https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/ 一年一度的國際奧林匹克數學競賽（IMO）是最負盛名的高中數學競賽，每年的IMO會設有 6道代數、幾何、數論以及組合學方面的題目。 近來，IMO被認為是機器學習領域的重要 挑戰，可用於衡量人工智慧（AI）系統的高級數學推理能力，這種能力對實現通用人工智 慧（AGI）很重要。 Google的DeepMind公司在今年年初推出了AlphaGeometry，該模型擅 長解決幾何證明題，已逼近人類金牌選手的水平，但無法應對幾何之外的代數、數論等問 題。 7月25日， DeepMind宣布推出基於強化學習、可用於形式數學推理的AlphaProof， 以及改進的幾何證明模型AlphaGeometry 2。 這兩個系統共同解決了今年IMO6題目中的4 道，首次達到了人類銀牌選手的水準 。 相較於上一代AlphaGeometry，DeepMind基於Gemini重新訓練了AlphaGeometry 2用到的語 言模型，並優化了符號引擎，提升了它解決複雜幾何問題的能力和效率。 對於IMO 2024 的問題4，AlphaGeometry 2只用19秒便給了答案。 AlphaProof則結合了預先訓練的語言 模型與強化學習演算法AlphaZero（通用棋類AI），並接受了一種名為Lean的形式化語言 的訓練。 其中，Lean是一種互動式定理證明語言，可用來檢驗數學證明的可靠性。 因此 用它訓練的模型可以避免自然語言訓練常出現的看似合理但不正確的答案。 對於IMO 2024的題目，AlphaProof花了三天時間解決了兩道代數問題，和一道數論問題，包括比賽 中最難的、僅有5位參賽選手解決的問題，但無法解決其餘兩道組合問題。 最終，經過數 學家評分，AlphaProof和AlphaGeometry 2共獲得了28分（滿分42），與金牌線29分相差 僅有1分，首次達到了銀牌選手的水平。 --

※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 111.253.162.64 (臺灣) ※ 文章網址: https://webptt.com/m.aspx?n=bbs/Math/M.1721979825.A.1CB.html