清華AIR團(tuán)隊 投稿
量子位 | 公眾號 QbitAI

當(dāng)AI不再只是解題機(jī)器，而能與人類并肩完成嚴(yán)謹(jǐn)?shù)目蒲凶C明，這意味著什么？

清華大學(xué)科研團(tuán)隊以自主研發(fā)的AI數(shù)學(xué)家系統(tǒng)（AIM）為協(xié)作伙伴，通過人機(jī)交互的模式成功解決了一項均勻化理論研究問題，形成約17頁數(shù)學(xué)證明。

該成果系統(tǒng)性驗證了AI從“數(shù)學(xué)解題工具”升級為“科研協(xié)作伙伴”的可行性，為復(fù)雜數(shù)學(xué)問題的突破提供了新路徑。

這一突破，也讓AI真正踏入了“原創(chuàng)科研”的核心地帶，為未來數(shù)學(xué)發(fā)現(xiàn)的方式打開了新的想象空間。

數(shù)學(xué)研究的“AI困境”

近年來，AI在數(shù)學(xué)領(lǐng)域的表現(xiàn)屢獲突破：

• Gemini憑借Deep Think技術(shù)達(dá)到國際數(shù)學(xué)奧林匹克（IMO 2025）金牌水平；
• o4-mini模型在專家級數(shù)學(xué)基準(zhǔn)測試FrontierMath中超越人類平均團(tuán)隊表現(xiàn)；
• GPT-5-Thinking協(xié)助研究者解決了量子計算領(lǐng)域的難題。

然而，這些成果多集中在“短時間、標(biāo)準(zhǔn)化”的競賽類任務(wù)中，與真實數(shù)學(xué)研究的需求存在巨大鴻溝。

當(dāng)前主流AI系統(tǒng)在數(shù)學(xué)研究中存在明顯局限：FunSearch、AlphaEvolve等依賴問題的程序化表述，僅適用于部分?jǐn)?shù)學(xué)領(lǐng)域；AlphaGeometry系列則聚焦幾何推理，難以覆蓋更廣泛的數(shù)學(xué)分支。

即便部分AI能提供碎片化見解，完整證明的構(gòu)建與驗證仍需依賴人類，難以真正融入研究全流程。

該研究的核心目標(biāo)正是打破這一困境，通過構(gòu)建“人類分析+AI推導(dǎo)”的協(xié)同范式，讓AI的推理能力與人類的邏輯分析能力、知識經(jīng)驗儲備形成互補(bǔ)，共同攻克單一主體難以突破的復(fù)雜數(shù)學(xué)難題。

五大模式為AI輔助數(shù)學(xué)研究提供“操作指南”

均勻化理論是連接材料科學(xué)、流體力學(xué)與數(shù)學(xué)的核心橋梁，其核心是分析異質(zhì)材料微觀結(jié)構(gòu)變化對宏觀力學(xué)行為的影響。

本研究聚焦的具體問題為：當(dāng)周期性分布的流體夾雜尺度趨近于零（ε→0）時，如何推導(dǎo)耦合Stokes-Lamé系統(tǒng)的極限均勻化方程，并嚴(yán)格證明原解與極限解的誤差估計。

該問題來源于真實數(shù)學(xué)研究，具有顯著挑戰(zhàn)性。

最終，團(tuán)隊通過人機(jī)協(xié)同不僅得出極限方程，更精確證明了誤差階數(shù) α=1/2，形成約17頁數(shù)學(xué)證明。

△Stokes-Lamé系統(tǒng)

具體來看，團(tuán)隊在人機(jī)協(xié)同模式下，通過對實驗結(jié)果的迭代分析，將原問題拆解為六個子問題（見下圖），通過系統(tǒng)性的人機(jī)協(xié)同工作對六個子問題進(jìn)行各個擊破，最終在此基礎(chǔ)上獲得原問題的完整證明。

AIM系統(tǒng)在幾個最困難子問題的證明過程中作出非平凡貢獻(xiàn)。

△子問題拆解及人機(jī)分工

在研究過程中，團(tuán)隊并非簡單“使用AI”，而是系統(tǒng)性總結(jié)出了五大高效人機(jī)交互模式，為數(shù)學(xué)家運(yùn)用AI開展研究提供了可復(fù)用、可推廣的實踐框架：

1、直接提示（Direct Prompting）

通過“定理提示”（提供關(guān)鍵定理及適用條件）、“概念引導(dǎo)”（明確證明框架與策略方向）、“細(xì)節(jié)優(yōu)化”（校準(zhǔn)符號定義與局部推導(dǎo)錯誤），引導(dǎo)AIM聚焦核心推理路徑，減少無效探索。

例如，在“Cell Problem”的分析中，人類專家向AIM提供了相關(guān)理論方法的輔助引理，使其推理錨定在嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)基礎(chǔ)上，避免邏輯偏離。

2、理論協(xié)同應(yīng)用（Theory-Coordinated Application）

將某一數(shù)學(xué)分支的完整理論體系（定義、引理、推理規(guī)則）打包為“知識包”提供給AIM，使其在預(yù)設(shè)理論框架內(nèi)開展多步驟連貫推導(dǎo)。

在證明“Cell Problem”的正則性時，人類專家提供了“Schauder Theory”的全套核心引理，AIM據(jù)此逐步推導(dǎo)，最終得出符合預(yù)期的結(jié)論，展現(xiàn)出對復(fù)雜理論體系的應(yīng)用能力。

3、交互式迭代優(yōu)化（Interactive Iterative Refinement）

遵循“AI輸出→人類診斷→反饋修正→AI再推理→…”的循環(huán)，逐步完善證明鏈條。

在誤差估計階段，人類專家發(fā)現(xiàn)AIM的證明存在邏輯缺口后，通過對問題本身和實驗結(jié)果的分析，拆分了多個中間問題，最終讓AIM自主修正證明結(jié)論，形成完整推理鏈。

4、明確運(yùn)用邊界（Applicability Boundary and Exclusive Domain）

針對AIM當(dāng)前難以勝任的任務(wù)（如復(fù)雜幾何構(gòu)型構(gòu)建、多尺度符號推理），由人類主導(dǎo)完成，避免資源浪費(fèi)。

例如，“雙尺度展開”需精準(zhǔn)處理x、y雙尺度變量的導(dǎo)數(shù)分解，AIM易出現(xiàn)符號混淆，人類專家通過手動推導(dǎo)確保這一基礎(chǔ)環(huán)節(jié)的正確性，為后續(xù)AI推導(dǎo)掃清障礙。

5、輔助優(yōu)化策略（Auxiliary Optimization）

通過多輪嘗試篩選最優(yōu)證明（如利用LLM的輸出隨機(jī)性）、提供目標(biāo)結(jié)論約束推理方向（如明確誤差估計的預(yù)期形式）、根據(jù)任務(wù)類型選擇適配模型（如o4-mini擅長框架構(gòu)建，DeepSeek-R1擅長細(xì)節(jié)推導(dǎo)），進(jìn)一步提升AI輸出的可靠性與效率。

舉例來看，在“Regularity of Cell Problem”這一子問題的證明過程中，人類專家明確引入了來自Schauder Theory的輔助引理，并將這些引理作為提示信息提供給AIM。

△人類專家將Schauder Theory的輔助引理提供給AIM

通過這種方式，人類專家引導(dǎo)AIM在推導(dǎo)后續(xù)結(jié)論時運(yùn)用這些引理，從而有效構(gòu)建并約束其推理過程，使其朝著得出有效且完整的論證方向推進(jìn)。

在該提示的引導(dǎo)下，AIM的輸出結(jié)果表明，其能主動且恰當(dāng)?shù)卣咸崾局邪男畔?，并?zhí)行正確的推導(dǎo)流程。

△AIM輸出結(jié)果

17頁證明背后的三重突破

本研究并非局限于單一問題的解決，更在理論范式、實踐驗證與方法指導(dǎo)三方面取得突破，為數(shù)學(xué)研究與AI的深度融合提供基礎(chǔ)。

價值一：驗證人機(jī)協(xié)同數(shù)學(xué)研究范式

團(tuán)隊深度驗證“人類引導(dǎo)+AI推理”的協(xié)同研究模式，將AI的推理能力與人類數(shù)學(xué)工作者的知識經(jīng)驗和邏輯推理系統(tǒng)性融合。

這種協(xié)作模式，拓寬了數(shù)學(xué)工作者的能力邊界，也進(jìn)一步提高了AI證明數(shù)學(xué)理論的實驗表現(xiàn)。

價值二：攻克均勻化理論難題

團(tuán)隊給出了這項均勻化問題的長達(dá)17頁的完整證明。

該證明的很大一部分內(nèi)容由AI生成，其在整個證明過程中做出了非平凡貢獻(xiàn)，充分體現(xiàn)了人機(jī)協(xié)同范式在解決復(fù)雜、研究級數(shù)學(xué)問題方面的潛力。

價值三：系統(tǒng)梳理交互模式

團(tuán)隊對人機(jī)交互模式進(jìn)行了系統(tǒng)化梳理，并提煉出具有實證價值的見解。

這些見解可為未來人工智能輔助數(shù)學(xué)研究框架的設(shè)計提供參考，同時也能為希望在自身研究中利用AI的數(shù)學(xué)家提供實際參考意見，幫助數(shù)學(xué)工作者快速掌握與AI的協(xié)作研究，加速AI與數(shù)學(xué)科研的融合落地。

從協(xié)同到自主：AI數(shù)學(xué)研究的下一階段目標(biāo)

AI在數(shù)學(xué)研究中的比較優(yōu)勢體現(xiàn)在基于現(xiàn)有理論的分析、搜索與適配方面，例如自動拆解問題、梳理文獻(xiàn)、優(yōu)化已知方法等。

與之相對，數(shù)學(xué)理論的核心突破當(dāng)前仍依賴于人類的原始直覺與抽象思維能力，如提出新概念、構(gòu)建新框架、設(shè)計新的證明范式等，以解決長期懸而未決的難題。

由于這類突破對嚴(yán)謹(jǐn)性要求極高，而當(dāng)前AI存在幻覺輸出（生成看似合理卻錯誤的內(nèi)容）與置信度誤判（對錯誤結(jié)論過度自信）等問題，因此完全自主的AI證明目前仍無法實現(xiàn)，分步的人工驗證仍是必不可少的環(huán)節(jié)。

基于現(xiàn)有研究發(fā)現(xiàn)，團(tuán)隊提出了未來研究的兩個重要方向：

深化并系統(tǒng)化人機(jī)交互模式

團(tuán)隊已提煉出一套能顯著加速數(shù)學(xué)理論進(jìn)展、拓展研究者能力邊界的交互模式。

下一步，團(tuán)隊將研究這些模式能否遷移到其他數(shù)學(xué)領(lǐng)域，以及能否針對特定領(lǐng)域需求設(shè)計更豐富、更高效的交互模式。

同時，團(tuán)隊將從多個維度對人機(jī)交互框架進(jìn)行系統(tǒng)化構(gòu)建，包括但不限于問題拆解、過程監(jiān)督、誤差修正、定理引用及依賴管理。

這需要基于大量實驗分析制定嚴(yán)格的分類標(biāo)準(zhǔn)，并明確交互模式效果等信息，以確保所構(gòu)建系統(tǒng)的嚴(yán)謹(jǐn)性。

基于交互反饋優(yōu)化AIM系統(tǒng)

團(tuán)隊的長期研究目標(biāo)是實現(xiàn)數(shù)學(xué)定理證明的自動化，因此AIM系統(tǒng)架構(gòu)的迭代優(yōu)化既關(guān)鍵又具內(nèi)在挑戰(zhàn)性。

通過人機(jī)協(xié)同的定理證明實驗，團(tuán)隊已明確智能體擅長的任務(wù)類型與存在困難的任務(wù)類型。這些積累的見解為系統(tǒng)設(shè)計的后續(xù)迭代提供了依據(jù)。

團(tuán)隊將以這些不足為出發(fā)點(diǎn)，嘗試提出訓(xùn)練方法以提升模型的推理能力，進(jìn)而改善實驗表現(xiàn)，從而增強(qiáng)大型語言模型在數(shù)學(xué)理論研究領(lǐng)域的能力。

論文鏈接：
https://arxiv.org/abs/2510.26380