國際數學奧林匹克競賽 (IMO) 可能是面向大學預科生的最負盛名的比賽。 每年，來自世界各地的學生爭奪其令人垂涎的銅牌、銀牌和金牌。 很快，人工智慧程式也可能與他們競爭。
今年 1 月，由 Google DeepMind 的 Trieu H. Trinh 和紐約大學領導的團隊在《自然》雜誌上釋出了一個名為 AlphaGeometry 的新人工智慧程式。 研究人員報告稱，該程式能夠解決過去 IMO 中的 30 道幾何題中的 25 道，成功率與人類金牌獲得者相似。 該人工智慧還找到了 2004 年 IMO 中一個更通用的解決方案，而該解決方案此前並未引起專家的注意。
在為期兩天的比賽中，參加 IMO 的學生必須解決來自不同數學領域的六個問題。 其中一些問題非常複雜，即使是專家也無法解決。 它們通常具有簡短而優雅的解決方案，但需要大量的創造力，這使得它們對人工智慧研究人員特別有吸引力。
支援科學新聞報道
如果您喜歡這篇文章，請考慮透過以下方式支援我們屢獲殊榮的新聞報道 訂閱。 透過購買訂閱，您正在幫助確保未來能夠繼續報道關於塑造我們當今世界的發現和想法的具有影響力的故事。
將數學證明翻譯成計算機能夠理解的程式語言是一項艱鉅的任務。 存在專門為幾何開發的正式程式語言，但它們很少使用來自其他數學領域的方法——因此，如果一個證明需要一個涉及複數等中間步驟，則無法使用專門用於幾何的程式語言。
為了解決這個問題，Trinh 和他的同事建立了一個數據集，該資料集不需要將人類生成的證明翻譯成正式語言。 他們首先讓演算法生成一組幾何“前提”或起點：例如，一個三角形，其中繪製了一些測量值，並在其邊上標記了額外的點。 然後，研究人員使用演繹演算法來推斷三角形的進一步屬性，例如哪些角匹配以及哪些線彼此垂直。 透過將前提與推匯出的屬性相結合，研究人員建立了一個由定理和相應證明組成的訓練資料集。 例如，一個問題可能涉及證明三角形的某個特徵——例如，它的兩個角相等。 相應的解決方案將包括演繹演算法得出該結論的步驟。
然而，為了解決 IMO 級別的問題，AlphaGeometry 需要更進一步。 “關鍵的缺失部分是生成新的證明項，”Trinh 和他的團隊在論文中寫道。 例如，為了證明關於三角形的某些東西，您可能需要引入問題中未提及的新點和線——而這正是大型語言模型 (LLM) 非常擅長做的事情。
LLM 透過計算一個詞跟隨另一個詞的機率來生成文字。 Trinh 和他的團隊能夠以類似的方式使用他們的資料庫來訓練 AlphaGeometry 關於定理和證明。 LLM 不會學習解決問題所涉及的演繹步驟； 這項工作仍然由其他專門的演算法完成。相反，人工智慧模型專注於尋找點、線和其他有用的輔助物件。
當 AlphaGeometry 收到一個問題時，演繹演算法首先推匯出一個關於該問題的陳述列表。 如果要證明的陳述未包含在該列表中，則人工智慧會介入。 例如，它可能會決定在三角形 ABC 中新增第四個點 X，以便ABCX表示一個平行四邊形——這是該程式從之前的訓練中學到的。 這樣做，人工智慧為演繹演算法提供了新的資訊來處理。 這個過程可以重複進行，直到人工智慧和演繹程式達到預期的結論。 “這種方法聽起來是合理的，並且在某些方面類似於國際數學奧林匹克競賽參與者的培訓，”菲爾茲獎章獲得者彼得·舒爾茨說道，他曾三次獲得 IMO 金牌。
為了測試 AlphaGeometry，科學家們選擇了自 2000 年以來 IMO 中出現的 30 道幾何題。 以前用於解決幾何問題的程式 Wu’s algorithm 僅正確解決了 10 道題，而 GPT-4 在所有問題上都失敗了，但 AlphaGeometry 解決了 25 道題。 研究人員表示，人工智慧的表現優於大多數 IMO 參與者，後者平均解決了 30 道題中的 15.2 道。（金牌獲得者平均正確解決了 25.9 道題。）
當研究人員檢視人工智慧生成的證明時，他們注意到，在解決一個問題的過程中，該程式並沒有使用所有提供的資訊——這意味著 AlphaGeometry 獨立自主地開始工作，並找到了一個相關但更通用的定理的解決方案。 同樣明顯的是，複雜的任務——IMO 參與者表現不佳的任務——通常需要人工智慧提供更長的證明。 似乎機器也面臨著與人類相同的挑戰。
AlphaGeometry 尚不能參加 IMO，因為幾何只是比賽的三分之一，但 Trinh 和他的同事強調，他們的方法可以應用於其他數學子學科，例如組合數學。 誰知道呢——也許幾年後，一位非人類的參與者將首次參加 IMO。 也許它甚至會贏得金牌。