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

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

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

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

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

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

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

研究介紹

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

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

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

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

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

菲爾茲獎(jiǎng)得主、IMO 金牌獲得者 Ng? B?o Chau（吳寶珠）表示：「現(xiàn)在我完全明白了，為什么 AI 研究者們會(huì)首先嘗試解決國際數(shù)學(xué)奧林匹克 (IMO) 的幾何題目，因?yàn)檎业剿鼈兊慕鉀Q方案有點(diǎn)像下棋，我們?cè)诿恳徊蕉加邢鄬?duì)較少的合理走法。但我仍然對(duì)他們能夠?qū)崿F(xiàn)這一點(diǎn)感到震驚。這是一項(xiàng)令人印象深刻的成就。」

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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