AI數學家,這次不只是來刷題的。
此前,清華大學智能產業研究院(AIR)院長劉洋教授團隊,發布了一個面向數學研究的智能體系統——
AIM。
![]()
與以往不少專注于解題的agent不同,AIM不只回答數學題,也試圖參與更早一步的科研工作:
它能夠幫助研究者發散思路、組織定理、生成證明草稿,并把這些內容交給人類繼續審查。
而最近,圍繞AIM,AIR-求真書院聯培學生王彥橋、求真書院劉錦鵬助理教授,完成了一項由AI深度參與的前沿量子算法研究——
Sign Embedding Quantum Algorithms for Matrix Equations and Matrix Functions。
![]()
這項研究從一個模糊直覺開始:有理逼近,能不能成為一種量子算法設計原則?
在研究過程中,AI先幫人類研究者把候選路線鋪開,再由人類篩選方向、審計假設、修復推導。AIM則在后續階段參與定理組織、證明草稿生成和復雜度分析。
最終,研究團隊提出了符號嵌入量子算法(Sign Embedding Quantum Algorithms),形成了一篇84頁的量子算法論文。
可以說,相比此前主要解決研究者給定的開放數學問題,這一次,AIM開始參與研究問題的提出與方向探索。
這是怎么做到的?
AI數學能力正在從“解題”走向“研究”
近年來,AI在數學推理、算法搜索、猜想檢驗和證明輔助等方向持續取得進展。
許多已有的案例主要面向相對明確的任務:給定一個待證明或待反駁的命題、一個需要優化的目標函數,或一個可以由程序執行并打分的搜索空間。
但在真實的前沿數學研究中,重要進展常常發生在定理正式出現之前。
研究者可能先擁有一個模糊直覺、一個跨領域類比或一種尚未定型的技術偏好,隨后才逐步判斷它應當轉化為什么問題、采用哪些假設、沿哪條路線推進,以及最終形成什么樣的定理族。
這一階段往往很難用標準答案或單一數值指標評價,卻直接影響研究的價值和方向。
圍繞“AI能否協助問題形成”這一問題,研究提供了一個較完整的觀察樣本:
AI與AIM被置于由人類研究者把關的研究閉環中,既參與探索與推導,也接受持續的審計、修訂和整合。
![]()
從一個元想法到可審計的定理族
值得一提的是,研究并不是從一個已經精確定義的量子算法定理開始,而是源自一個人類研究者提出的宏觀直覺:
有理逼近在處理階躍型函數,尤其是符號函數時具有優勢,這一思想是否可以作為量子算法設計原則?
在早期探索中,研究者通過與通用AI模型的交互,將這一直覺擴展為一組候選研究方向和比較維度。
隨后,人類研究者依據數學品味、技術可行性和潛在貢獻進行篩選,逐步聚焦到“符號嵌入”( Sign-Embedding)路線。
AIM在后續階段作為人機協同研究系統的一部分,幫助將已選路線組織為可審計的定理目標和推導材料。
最終形成的量子算法論文共84頁,下圖展示了AI/AIM在該論文形成過程中所起的作用。
![]()
需要說明的是,早期依賴通用AI對話完成的路線發散、候選方向組織和比較功能,已經在后續AIM v2中進一步沉淀為系統化能力。
也就是說,該案例不僅展示了一次具體研究過程,也反映了AIM從交互式輔助走向更完整科研工作流支持的演進。
人機協同工作流:人類價值門控下的AI高通量探索
從AI研究角度看,這篇研究的重點不在于展示“全自動數學發現”,而在于呈現一個可追蹤、可審計、可復用的人機協同流程。
整個流程可以概括為五個環節。
發散性路線擴展(Divergent Route Expansion):人類研究者提供核心元想法或宏觀科研直覺,AI將其擴展為多個候選問題、技術路線和跨領域連接,幫助研究者更快看到周邊研究空間。
人類價值把關(Human Value Gate):面對 AI 生成的候選分支,人類研究者依據學術判斷、問題價值和技術可行性進行篩選與聚焦,決定哪些方向值得繼續投入。
定理形成與推導(Theorem Formation and Derivation):主干路線確定后,AIM幫助把高層思路轉化為定理陳述、引理分解、證明草稿和復雜度表達式等可審計材料。
復雜度審計與修復(Complexity Audit and Repair):在量子算法研究中,證明正確并不自動意味著算法貢獻充分;假設是否自然、訪問模型是否合理、復雜度是否過松,都需要反復檢查。修復、優化或重構過程仍可繼續借助AI/AIM的推導、對照和重寫能力完成,但關鍵判斷和最終確認必須由人類研究者承擔。
驗證與整合(Validation and Integration):所有數學陳述、證明、假設、復雜度估計和貢獻表述,最終都需要經過人類研究者核查、取舍、改寫和整合,才能進入公開論文。
![]()
連接發現、推導生成與審慎審查
總的來說,AIM的意義并不是取代人類數學家獨立完成研究,而是在一個人類把關的循環中提升探索密度和推導效率。
AI/AIM可以快速擴展候選路線,組織相關概念之間的連接,并生成可供審查的證明與復雜度草稿;
人類研究者則負責決定哪些路線有研究價值、哪些假設可以接受、哪些推導需要修復。
這種協同模式使研究過程更接近“高通量候選生成+人類價值門控+AI輔助審計修復+人類最終整合”。
它的優勢不在于讓AI輸出直接成為最終結論,而在于把原本難以窮盡的路線探索、連接組織和局部推導轉化為可檢查、可比較、可逐步修訂的中間材料。
對于AI4Math和AI Scientist研究,這也提示:理論研究中的反饋信號往往不是實驗分數,而是數學判斷。
系統需要支持長程記憶、路線管理、假設記錄、復雜度審計和反駁性檢查,使人類研究者能夠更有效地控制方向、發現錯誤并穩定最終成果。
符號嵌入量子算法
作為該協同過程形成的技術成果,王彥橋和劉錦鵬提出的“符號嵌入量子算法”面向一類矩陣方程和矩陣函數問題,包括Sylvester、Lyapunov、Riccati方程,以及矩陣平方根、逆平方根和幾何平均等對象。
這些問題在數值線性代數、控制理論、動力系統和科學計算中具有基礎地位。
對非量子方向讀者而言,可以把該論文的核心思路理解為:先將多類結構化矩陣問題壓縮到某個擴張矩陣的符號函數或符號投影中,
再通過有理逼近和移位逆等量子算法原語實現相應對象。這樣的“先嵌入、再逼近”路線,為多個看似不同的問題提供了統一組織方式。
該量子論文的技術貢獻包括:在非正規、不可對角化等更一般輸入條件下建立可用的假設與復雜度表述;
將輸出從單個向量態推進到可供下游量子線路調用的矩陣塊編碼;并通過對移位逆實現層的縮放、重平衡和復雜度審計,形成較系統的算子輸出量子線性代數框架。
理論研究中的人類判斷與AI生產力
總的來說,研究呈現了AI參與數學研究的一種較為現實的方式:
AI可以幫助研究者更快地拓展路線、整理關聯、草擬證明和進行初步復雜度分析,從而降低理論研究中部分基礎推導與局部探索的顯性成本。
但與此同時,研究方向是否值得深入、假設是否自然合理、結果是否具有足夠的理論價值,仍然依賴研究者的專業判斷與持續審查。
隨著智能體能夠快速生成大量候選路線、證明草稿和技術表述,理論科學家的工作重心也可能發生變化。
繁瑣推導的部分成本被壓縮后,研究者可以將更多精力投入到方向選擇、問題定義、假設把關和結果審計之中。
換言之,判斷“什么問題真正值得研究”,以及識別那些表面合理但存在隱藏條件、技術漏洞或貢獻不足的路線,將成為更加關鍵的能力。
這一點也為AIM的后續發展提供了重要啟示。未來值得進一步加強的,不只是單點證明或局部推導能力,也包括支撐科研全過程的系統能力:
例如記錄和比較不同研究路線,顯式管理關鍵假設,保留可審計的推導痕跡,發現隱藏條件和復雜度漏洞,并在AI輔助下支持研究者完成后續修復、優化與重構。
這一案例表明,AI在前沿理論研究中的價值,正在從局部任務輔助逐步延伸到更完整的研究流程之中。
AIM將路線拓展、關聯發現、證明草擬和審計反饋等能力組織起來,使AI的生成與推導能力能夠更好地服務于人類研究者的方向判斷和數學把關。
這樣的協同方式,為提高理論研究效率、拓展研究視野提供了新的可能。
AIM系統應用報告:From Meta Idea to Advanced Mathematical Discovery: Human-AI Co-Discovery of Sign-Embedding Quantum Algorithms(https://arxiv.org/abs/2606.24899)
量子算法論文:Sign Embedding Quantum Algorithms for Matrix Equations and Matrix Functions (http://arxiv.org/abs/2604.25333)
AIM repo:https://github.com/TheoryFoundry/AIMv2AIM
blog:https://ai-mathematician.net
文章來源:量子位。
特別聲明:以上內容(如有圖片或視頻亦包括在內)為自媒體平臺“網易號”用戶上傳并發布,本平臺僅提供信息存儲服務。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.