谷歌AI險失IMO金牌：19秒解題震驚評委，幾何能力超越人類

AlphaProof

AlphaProof 是一個能夠在 Lean 形式語言中證明數學命題的系統。它結合了預訓練的大型語言模型和 AlphaZero 強化學習算法。

為了克服機器學習在形式語言中由於人工編寫數據有限而產生的限制，研究人員通過以下方式彌合了自然語言和形式陳述之間的差距：

1. 微調 Gemini 模型以自動將自然語言問題陳述翻譯成形式陳述
2. 創建一個包含不同難度的形式化問題的大型庫

在解決問題時，AlphaProof 生成候選解決方案，並通過在 Lean 中搜索可能的證明步驟來證明或反駁它們。

AlphaGeometry 2

AlphaGeometry 2 是一個使用 Gemini 語言模型從頭開始訓練的神經符號混合系統。它可以解決比其前身更困難的幾何問題，包括涉及物體運動、角度、比例和距離方程的問題。

主要改進包括：

1. 在比之前版本大一個數量級的合成數據上進行訓練
2. 比以前快兩個數量級的符號引擎
3. 一種新穎的知識共享機制，允許不同搜索樹的高級組合來解決更複雜的問題

AlphaGeometry 2 展示了令人印象深刻的能力，解決了過去 25 年國際數學奧林匹克競賽（IMO）幾何問題的 83%，而其前身為 53%。在今年的 IMO 中，它在收到形式化問題後僅用 19 秒就解決了第 4 題。

AI 在 IMO 中的表現展示了數學推理能力的顯著進步，使 AI 在高等數學的問題解決能力上更接近人類水平。