清華AI數(shù)學(xué)家：獨(dú)立完成理論難題，自動(dòng)調(diào)用基本定理構(gòu)建證明思路

白交 2025-06-05 10:17:40 來源：量子位

清華AIM團(tuán)隊(duì) 投稿

量子位 | 公眾號(hào) QbitAI

AI數(shù)學(xué)家來了！清華團(tuán)隊(duì)出品——

他們推出AI Mathematician（AIM）框架，推理模型也能求解前沿理論研究，并且證明完成度很高。

比如一道吸收邊界條件問題。這是分析中涉及方程的經(jīng)典理論問題，通過構(gòu)造人工邊界得到較為精確的近似解。

AIM部分求解過程如下：

AIM給出了方程的能量估計(jì)，這是求解這個(gè)問題的關(guān)鍵的中間結(jié)論。它不僅正確推導(dǎo)了這個(gè)結(jié)論，在后續(xù)證明中加以運(yùn)用。

這是AIM對(duì)于方程的近似解的構(gòu)造和存在唯一性的證明過程。盡管部分運(yùn)算細(xì)節(jié)并沒有展示出來，但是這里的證明思路和定理運(yùn)用都是正確的，也得到了整個(gè)問題中的關(guān)鍵結(jié)論。

本次成果的作者包括劉遠(yuǎn)航、黃硯星、王彥橋、李鵬、劉洋，其中劉遠(yuǎn)航、黃硯星、王彥橋?yàn)檎撐墓餐谝蛔髡摺?/p>

AIM數(shù)學(xué)家智能體

傳統(tǒng)大語(yǔ)言模型在數(shù)學(xué)領(lǐng)域的突破長(zhǎng)期局限于競(jìng)賽級(jí)問題，LRMs快速發(fā)展的數(shù)學(xué)推理能力也讓人類數(shù)學(xué)工作者期待可以使用大模型進(jìn)行前沿?cái)?shù)學(xué)研究。

當(dāng)前數(shù)學(xué)理論的研究主要有以下兩大挑戰(zhàn)：

• 問題復(fù)雜度
• 數(shù)學(xué)理論的推導(dǎo)和證明往往需要復(fù)雜的思考過程和推導(dǎo)細(xì)節(jié)，需要引理證明和跨領(lǐng)域的知識(shí)整合。這樣的復(fù)雜度遠(yuǎn)超競(jìng)賽題的求解模式。

• 證明嚴(yán)謹(jǐn)性
• 數(shù)學(xué)研究的證明內(nèi)容需要經(jīng)過嚴(yán)格驗(yàn)證和精確的分析，而自然語(yǔ)言證明的評(píng)估一直缺乏有效方法。

基于此，AIM框架首次將LRMs的推理能力引導(dǎo)延伸至前沿?cái)?shù)學(xué)研究，在人工智能探索數(shù)學(xué)理論的道路上邁出了關(guān)鍵的一步。

技術(shù)架構(gòu)上，主要包括三大模塊協(xié)作驅(qū)動(dòng)自動(dòng)理論研究。

1、探索模塊：通過開放推理，生成猜想和引理，構(gòu)建問題的多種探索思路；

2、驗(yàn)證模塊：基于悲觀驗(yàn)證機(jī)制，對(duì)證明過程進(jìn)行多角度并行評(píng)估，確保證明嚴(yán)謹(jǐn)性準(zhǔn)確性；

3、修正模塊：根據(jù)驗(yàn)證反饋優(yōu)化證明結(jié)構(gòu)，并且可以接收人為修正意見，確保輸出結(jié)論的正確性。

人類工作者首先提供探究課題的一些問題設(shè)定和求解結(jié)論，也可以包含方法信息，例如術(shù)語(yǔ)的定義，或者一些初步結(jié)論。這些內(nèi)容將視為系統(tǒng)提示傳遞給三個(gè)模塊。在這之后，會(huì)將數(shù)學(xué)研究需要求解的問題傳遞給這個(gè)智能體。AIM將嘗試一步一步地解決這個(gè)問題，并輸出其所有中間過程和結(jié)論。

為了應(yīng)對(duì)數(shù)學(xué)理論的挑戰(zhàn)，更好的激發(fā)LRMs在數(shù)學(xué)研究的推理能力，提高證明的完成度，AIM通過以下兩大核心策略攻克難題：

1、“探索+記憶”機(jī)制
智能體圍繞研究命題自由探索可行的方向。通過驗(yàn)證，逐步生成中間猜想完成理論的推導(dǎo)證明。如此可以有效拆解過長(zhǎng)思維路徑，通過多輪遞進(jìn)自動(dòng)形成研究思路。

2、“檢驗(yàn)與修正”機(jī)制
檢驗(yàn)?zāi)K中，有多重LRM并行評(píng)審證明過程，取最嚴(yán)苛意見拒絕不嚴(yán)謹(jǐn)證明。再將評(píng)估意見迭代反饋給修正模塊，自動(dòng)修正完善每一處證明細(xì)節(jié)。

在這樣的迭代反饋機(jī)制下，AIM會(huì)仔細(xì)思考每一種證明思路，完善中間結(jié)論的證明，最后給出整個(gè)問題的逐步證明過程。

實(shí)驗(yàn)驗(yàn)證：求解四個(gè)理論問題

AIM嘗試求解了四個(gè)數(shù)學(xué)上具有挑戰(zhàn)性的研究問題，三個(gè)已證明的定理和一個(gè)開放的問題。

將單個(gè)LRM直接應(yīng)用于這些問題不會(huì)得到正確的數(shù)學(xué)推理結(jié)果，并且不能構(gòu)成數(shù)學(xué)理論中的有效證明過程。而AIM在其中自主構(gòu)造關(guān)鍵引理，給出證明過程或者提供不平凡的新結(jié)論。

量子算法問題

LCHS方法是科學(xué)計(jì)算中的一種高效計(jì)算方法。Black-Scholes-Merton模型是金融學(xué)中用于歐式期權(quán)定價(jià)的基本數(shù)學(xué)框架。這個(gè)問題就是利用LCHS來模擬BSM模型，并設(shè)計(jì)相應(yīng)的量子算法。實(shí)驗(yàn)表明，AIM可以給出比較詳細(xì)的證明，基本解決這個(gè)問題。

吸收邊界條件

這是分析中涉及方程的經(jīng)典理論問題，通過構(gòu)造人工邊界得到較為精確的近似解。給出合理的思路后，AIM可以正確運(yùn)用提到的方法與技術(shù)。最后給出了一個(gè)完成度很高的證明。

高對(duì)比度極限

這是一個(gè)關(guān)于Lame-Stokes系統(tǒng)參數(shù)極限的誤差分析問題，是方程分析理論中的一個(gè)復(fù)雜問題，也是實(shí)際應(yīng)用中的一個(gè)重要特例。雖然推導(dǎo)中存在一些不嚴(yán)謹(jǐn)之處，但是AIM給出了核心結(jié)論的主要證明過程和推導(dǎo)細(xì)節(jié)，并且還探索出了一些新的正確的結(jié)論。

均勻化問題

均勻化理論是方程分析和應(yīng)用數(shù)學(xué)的一個(gè)重要研究領(lǐng)域，專注于推導(dǎo)具有多尺度結(jié)構(gòu)的材料或系統(tǒng)的等效宏觀性質(zhì)，如周期性或隨機(jī)特征。在探索這一問題的過程中，AIM給出了一些正確的結(jié)論和思路，對(duì)數(shù)學(xué)家完成這一研究具有指導(dǎo)意義。

實(shí)驗(yàn)表明，AIM 生成的證明雖仍需數(shù)學(xué)工作者進(jìn)行局部調(diào)整，但已能合理運(yùn)用數(shù)學(xué)技術(shù)，覆蓋核心邏輯鏈，甚至在部分問題中洞察非平凡結(jié)論，顯著加速研究進(jìn)展。

總結(jié)

AIM在數(shù)學(xué)研究中展現(xiàn)了基本的數(shù)學(xué)研究能力。它可以在證明過程中調(diào)用基本定理，并應(yīng)用這些定理完成證明過程。它還展示了識(shí)別和實(shí)現(xiàn)人工提供的指導(dǎo)和提示的能力，最終按照指示完成證明過程。

AIM可以嘗試完成各種數(shù)學(xué)理論的證明。它可以運(yùn)用正確的證明思路，提供關(guān)鍵的中間過程和核心結(jié)論。在數(shù)學(xué)理論研究中，數(shù)學(xué)家們經(jīng)常會(huì)產(chǎn)生多個(gè)證明思路和猜想。這些潛在的方法可以系統(tǒng)地輸入到AIM中，用于自動(dòng)生成證明嘗試。然后，數(shù)學(xué)家可以分析輸出結(jié)果，以確定方法的可行性，從而推進(jìn)理論證明。后續(xù)也可以進(jìn)一步根據(jù)實(shí)驗(yàn)結(jié)果，嘗試更多的方法和思路，繼續(xù)使用AIM來探索數(shù)學(xué)理論的證明與結(jié)論。

不過，AIM數(shù)學(xué)家智能體仍處于非常早期的階段。目前出現(xiàn)的問題包括重復(fù)探索，對(duì)特定的數(shù)學(xué)設(shè)定理解能力不夠強(qiáng)以及缺乏部分證明細(xì)節(jié)等問題。當(dāng)然最核心的是當(dāng)前的LLM的推理能力還并不夠強(qiáng)大，因此在很多較為前沿的復(fù)雜數(shù)學(xué)理論的研究中還是略顯稚嫩。

未來將通過記憶反思機(jī)制、多智能體協(xié)作和強(qiáng)化學(xué)習(xí)優(yōu)化等途徑進(jìn)一步提升能力。隨著算法與算力的迭代，人工智能有望成為數(shù)學(xué)研究的核心驅(qū)動(dòng)力，推動(dòng)人類向更深遠(yuǎn)的科學(xué)未知發(fā)起挑戰(zhàn)。

論文地址：?https://arxiv.org/abs/2505.22451