6日，記者從北京大學(xué)北京國際數(shù)學(xué)研究中心了解到，該中心董彬教授課題組與合作者組建的AI4Math團(tuán)隊(duì)用自主構(gòu)建的自動化AI框架解決了交換代數(shù)中一個開放問題——安德森猜想，并在用于形式化驗(yàn)證數(shù)學(xué)定理正確性的編程語言和定理證明器——Lean中完成了約19000行的形式化驗(yàn)證。這是國內(nèi)首次以AI框架攻克交換代數(shù)開放問題并實(shí)現(xiàn)大規(guī)模形式化驗(yàn)證，開辟了數(shù)學(xué)與AI深度融合的更多可能。

　　安德森猜想由美國數(shù)學(xué)家安德森于2014年提出，它關(guān)注的是“準(zhǔn)完備局部環(huán)”的一類性質(zhì)——這類環(huán)旨在用代數(shù)工具刻畫幾何對象局部（如某點(diǎn)附近）的無窮小結(jié)構(gòu)與變形。該猜想提出后十余年始終無人突破。

　　此次解決安德森猜想，北京大學(xué)AI4Math團(tuán)隊(duì)搭建的雙智能體協(xié)作框架功不可沒。該框架由自然語言推理智能體Rethlas和形式化驗(yàn)證智能體Archon組成。

　　研究中，Rethlas通過團(tuán)隊(duì)自研的Matlas自然語言語義檢索系統(tǒng)，從上千萬條數(shù)學(xué)陳述中精準(zhǔn)定位到與猜想看似無關(guān)的整環(huán)完備化理論成果，以此構(gòu)造反例。隨后，Archon將證明轉(zhuǎn)化為約19000行Lean代碼，并在過程中自主發(fā)現(xiàn)初始方案存在隱含的邏輯漏洞，重新設(shè)計了形式化證明的整體技術(shù)路線，還在所需數(shù)學(xué)概念于Lean形式化數(shù)學(xué)庫中尚未收錄時，自主找到等價替代路徑，最終完成的代碼覆蓋6篇外部論文關(guān)鍵結(jié)果，完成同等規(guī)模形式化工作的效率較經(jīng)驗(yàn)豐富的Lean專家提升至少10倍。

　　該成果的背后是團(tuán)隊(duì)三年的技術(shù)積累與跨學(xué)科協(xié)作。2023年，北京大學(xué)AI4Math團(tuán)隊(duì)正式組建，它由一群對這個方向有共同判斷的人逐步自然匯聚而成，團(tuán)隊(duì)成員來自代數(shù)與數(shù)論、優(yōu)化、機(jī)器學(xué)習(xí)與人工智能等方向。

　　董彬告訴科技日報記者，團(tuán)隊(duì)認(rèn)為，讓AI做嚴(yán)肅數(shù)學(xué)推理，檢索最為關(guān)鍵。他們打造了雙引擎檢索架構(gòu)——LeanSearch和Matlas。LeanSearch用自然語言描述需求即可語義檢索出相關(guān)定理，現(xiàn)已被Lean官方社區(qū)廣泛使用。Matlas則覆蓋上千萬條數(shù)學(xué)陳述，支持命題級語義檢索。在這些基礎(chǔ)設(shè)施之上，他們搭建了前述兩個AI智能體。

　　北京大學(xué)數(shù)學(xué)科學(xué)學(xué)院院長、中國科學(xué)院院士劉若川指出，此次探索不僅解決了具體數(shù)學(xué)問題，更驗(yàn)證了AI與數(shù)學(xué)融合的新研究范式。中國科學(xué)院院士田剛由此呼吁，應(yīng)鼓勵和支持青年學(xué)者大膽創(chuàng)新，進(jìn)一步推動AI與數(shù)學(xué)的深度融合，并在國家急需解決的重大科技問題中發(fā)揮關(guān)鍵作用。（記者　張蓋倫）

　　轉(zhuǎn)自：科技日報

　　【版權(quán)及免責(zé)聲明】凡本網(wǎng)所屬版權(quán)作品，轉(zhuǎn)載時須獲得授權(quán)并注明來源“中國產(chǎn)業(yè)經(jīng)濟(jì)信息網(wǎng)”，違者本網(wǎng)將保留追究其相關(guān)法律責(zé)任的權(quán)力。凡轉(zhuǎn)載文章及企業(yè)宣傳資訊，僅代表作者個人觀點(diǎn)，不代表本網(wǎng)觀點(diǎn)和立場。版權(quán)事宜請聯(lián)系：010-65363056。

延伸閱讀