這一次，人工智能算法在數(shù)學(xué)奧林匹克競賽（IMO）上取得了重大成績突破。

在今天發(fā)表的國際權(quán)威期刊《自然》雜志最新一期上，論文《Solving olympiad geometry without human demonstrations》向世人介紹了 AlphaGeometry，專家表示，這是人工智能朝著具有人類推理能力方向邁進(jìn)的重要一步。

論文鏈接：https://www.nature.com/articles/s41586-023-06747-5

DeepMind 也在論文發(fā)表的第一時間將代碼和模型開源，GitHub：https://github.com/google-deepmind/alphageometry

這是一種人工智能系統(tǒng)，來自 Google DeepMind 研究者之手，它能夠以接近人類奧賽金牌得主的水平解決復(fù)雜的幾何問題。

在對 30 道奧數(shù)幾何題的基準(zhǔn)測試中，AlphaGeometry 在標(biāo)準(zhǔn)奧數(shù)時限內(nèi)解決了 25 道。相比之下，之前最先進(jìn)的系統(tǒng)解決了其中 10 個幾何問題，而人類金牌得主平均解決了 25.9 個問題。

定理證明對于基于學(xué)習(xí)的 AI 模型來說困難程度很高，因為在大多數(shù)數(shù)學(xué)領(lǐng)域中，翻譯成機器可驗證語言的人類證明的訓(xùn)練數(shù)據(jù)都很少。DeepMind 提出了一種使用合成數(shù)據(jù)進(jìn)行定理證明的替代方法，基于該解決方案的通用的指導(dǎo)框架 AlphaGeometry 具有對很多領(lǐng)域的適用性。

研究介紹

AlphaGeometry 將語言模型與「符號引擎」相結(jié)合，借助符號和邏輯規(guī)則進(jìn)行數(shù)學(xué)推論。在這其中，語言模型擅長識別、預(yù)測流程的后續(xù)步驟，但缺乏數(shù)學(xué)推理所需的嚴(yán)謹(jǐn)性；另一方面，符號引擎純粹基于形式邏輯和嚴(yán)格的規(guī)則，這使得它能夠引導(dǎo)語言模型走向理性決策。

在 AlphaGeometry 的研究上，DeepMind 從跨越 2000 年到 2022 年之間的 30 個奧林匹克幾何問題（IMO-AG-30）的基準(zhǔn)測試集中進(jìn)行了測試，結(jié)果表明，AlphaGeometry 在比賽時間限制下能夠解決 25 個問題。而之前最先進(jìn)的方法（Wu’s method）只能解決 10 個。

眾所周知，由于缺乏推理技能和訓(xùn)練數(shù)據(jù)，AI 系統(tǒng)經(jīng)常難以解決幾何和數(shù)學(xué)方面的復(fù)雜問題。AlphaGeometry 系統(tǒng)將神經(jīng)語言模型的預(yù)測能力與規(guī)則約束推理引擎相結(jié)合，兩者協(xié)同工作以找到了新的解決方案。

此外，為了解決數(shù)據(jù)難題，該研究生成了大量的合成訓(xùn)練數(shù)據(jù)，即 1 億個示例，其中許多定理的證明步驟超過 200 步，比數(shù)學(xué)奧林匹克競賽定理的平均證明長度長 4 倍。

AlphaGeometry 展示了 AI 不斷增長的邏輯推理能力以及發(fā)現(xiàn)和驗證新知識的能力。解決奧林匹克級別的幾何問題是 AI 在邁向更先進(jìn)和通用人工智能系統(tǒng)道路上的一個重要里程碑。 

菲爾茲獎得主、IMO 金牌獲得者 Ng? B?o Chau（吳寶珠）表示：「現(xiàn)在我完全明白了，為什么 AI 研究者們會首先嘗試解決國際數(shù)學(xué)奧林匹克 (IMO) 的幾何題目，因為找到它們的解決方案有點像下棋，我們在每一步都有相對較少的合理走法。但我仍然對他們能夠?qū)崿F(xiàn)這一點感到震驚。這是一項令人印象深刻的成就。」

吳寶珠，2010 年菲爾茲獎得主，現(xiàn)任芝加哥大學(xué)教授。

AlphaGeometry 是一個神經(jīng)符號系統(tǒng)，由神經(jīng)語言模型和符號推演引擎組成，它們共同尋找復(fù)雜幾何定理的證明。一個系統(tǒng)提供快速、直觀的想法，而另一種則提供更加深思熟慮、理性的決策。

由于語言模型擅長識別數(shù)據(jù)中的一般模式和關(guān)系，因此它們可以快速預(yù)測潛在有用的結(jié)構(gòu)，但通常缺乏嚴(yán)格推理或做出解釋。另一方面，符號推演引擎基于形式邏輯并使用明確的規(guī)則來得出結(jié)論，兩者相互配合，共同構(gòu)成了 AlphaGeometry。

AlphaGeometry 的語言模型引導(dǎo)其符號推演引擎尋找?guī)缀螁栴}的可能解決方案。一般的奧林匹克幾何問題基于圖表，需要添加新的幾何結(jié)構(gòu)才能解決，例如點、線或圓。AlphaGeometry 的語言模型可以從無數(shù)種可能性中預(yù)測添加哪些新結(jié)構(gòu)最有用。這些線索有助于填補空白，并允許符號引擎對圖表進(jìn)行進(jìn)一步推論并接近解決方案。

舉例來說，下圖（上）為 AlphaGeometry 解答簡單題的過程，題目為「設(shè) ABC 為 AB = AC 的任意三角形。證明∠ABC = ∠BCA?！?/span>

AlphaGeometry 證明過程是這樣的：AlphaGeometry 通過運行符號推演引擎（symbolic deduction  engine）啟動證明搜索。這個引擎會從定理的前提出發(fā)，詳盡地推導(dǎo)出新的陳述，直到定理得到證明或者新的陳述被耗盡。假如符號引擎未能找到證明，語言模型會構(gòu)造一個輔助點，在符號引擎重新開始之前增加可證明的條件。這個循環(huán)一直持續(xù)到找到解決方案為止。對于簡單的例子，循環(huán)在第一個輔助結(jié)構(gòu)「 BC 的中點添加 D 點」之后終止。

下圖（下）為 AlphaGeometry 解決 IMO 的解題思路?！缸C明三角形 FKM 和 KQH 的外接圓 (O1) 和 (O2) 彼此相切……」，這么復(fù)雜的問題，AlphaGeometry 同樣也能證明，證明過程還給出了輔助點等。出于說明目的，證明過程被大大縮短和編輯。

生成 1 億數(shù)學(xué)推理訓(xùn)練數(shù)據(jù)

人類可以在紙上進(jìn)行勾畫來學(xué)習(xí)幾何、檢查圖表并使用現(xiàn)有知識來發(fā)現(xiàn)新的、更復(fù)雜的幾何屬性和關(guān)系。該研究生成合成數(shù)據(jù)的方法大規(guī)模模擬了這種知識構(gòu)建過程。其中生成合成數(shù)據(jù)的方法如圖 3 所示。

使用高度并行計算，系統(tǒng)首先生成 5 億個幾何對象的隨機圖，并詳盡地導(dǎo)出每個圖中點和線之間的所有關(guān)系。AlphaGeometry 找到每個圖中包含的所有證明，然后逆向推導(dǎo)，找出需要哪些額外的結(jié)構(gòu)（如果有的話）來獲得這些證明。這一過程為「符號推演與回溯」。

由 AlphaGeometry 生成的合成數(shù)據(jù)的可視化表示

之后，這個巨大的數(shù)據(jù)池被過濾以排除類似的示例，從而產(chǎn)生了 1 億個訓(xùn)練數(shù)據(jù)集。

開創(chuàng)性的人工智能推理能力

AlphaGeometry 提供的每一道奧數(shù)題的解法都經(jīng)過計算機檢查和驗證。研究人員還將其結(jié)果與之前的人工智能方法以及人類在奧林匹克競賽中的表現(xiàn)進(jìn)行了比較。此外，數(shù)學(xué)教練、前奧賽金牌得主 Evan Chen（陳誼廷）為我們評估了 AlphaGeometry 的一系列解決方案。

陳誼廷，MIT 數(shù)學(xué)在讀博士，曾獲得 IMO 2014 年金牌。

Evan Chen 表示：「AlphaGeometry 的輸出令人印象深刻，因為它既可驗證又干凈。過去針對基于證明的競爭問題的人工智能解決方案有時是碰巧的（輸出有時是正確的，需要人工檢查），而 AlphaGeometry 沒有這個弱點：它的解決方案具有機器可驗證的結(jié)構(gòu)。另一方面，它的輸出仍然是人類可讀的。人們可以想象一個通過強力坐標(biāo)系解決幾何問題的計算機程序：想想一頁又一頁繁瑣的代數(shù)計算，AlphaGeometry 不是這樣做的，它像人類學(xué)生一樣使用帶有角度和相似三角形的經(jīng)典幾何規(guī)則。」

最近一段時間，金融科技公司 XTX Markets 設(shè)立了人工智能奧林匹克數(shù)學(xué)獎（AI-MO Prize），旨在鼓勵能夠進(jìn)行數(shù)學(xué)推理的人工智能模型的開發(fā)。由于每個奧林匹克競賽都有六個問題，其中只有兩個通常集中在幾何上，因此 AlphaGeometry 只能應(yīng)用于給定奧林匹克競賽中的三分之一問題。

盡管如此，AlphaGeometry 僅靠自己的幾何解題能力就成為了世界上第一個能夠在 2000 年和 2015 年通過 IMO 銅牌門檻的人工智能模型。

DeepMind 已在著手推進(jìn)下一代人工智能系統(tǒng)的推理。研究人員認(rèn)為，鑒于利用大規(guī)模合成數(shù)據(jù)從頭開始訓(xùn)練人工智能系統(tǒng)的廣泛潛力，這種方法可能會影響未來人工智能系統(tǒng)發(fā)現(xiàn)數(shù)學(xué)及其他領(lǐng)域新知識的方向。

AlphaGeometry 開創(chuàng)了人工智能數(shù)學(xué)推理的先河 —— 從探索純數(shù)學(xué)之美到使用語言模型解決數(shù)學(xué)和科學(xué)問題。人們希望這種技術(shù)能夠繼續(xù)提升，進(jìn)而解決更高級、抽象的數(shù)學(xué)問題。

而在數(shù)學(xué)之外，AlphaGeometry 的影響或許還可以覆蓋到包含幾何問題的更多領(lǐng)域，如計算機視覺、建筑，甚至理論物理學(xué)等。