（本文閱讀時間：10分鐘）
數學貫穿人類歷史，被視為宇宙的語言。萬事萬物中都蘊含著數學理論，藉助數學思維，人們得以洞察事物的本質。如今，數學建模在氣候科學、醫學成像、疾病控制以及人工智慧等諸多領域，都發揮著重要作用。
在3月14日“國際數學日”，我們邀請到近年來專注於人工智慧數學推理研究的微軟亞洲研究院高階研究員張憲，深入探討了他和同事們在大語言模型數學推理領域的探索與突破。張憲表示，他們的研究並非從資料角度出發，而是更多地從規則角度入手，透過形式化和符號化的方法，讓大語言模型基於數學領域的知識學習內在規則，並實現自動化擴充套件和應用，推動數學推理能力的發展。
微軟亞洲研究院高階研究員張憲
張憲：首先，數學推理是人工智慧的必要組成部分。隨著數學推理能力的提升，大語言模型透過學習數學的方法、規則，能夠增強模型整體的推理效能。數學推理與邏輯規則緊密相連，這種能力的提升不僅能夠幫助大模型更好地理解和處理複雜任務，還能將數學推理方法泛化到其他領域，如程式碼最佳化、常識推理，甚至是語義理解等，展現出更高的效率和準確性。
另外，數學還是科學研究的基礎，尤其在當前備受關注的 AI for Science（科學智慧）領域，大模型數學能力的提升將直接促進人工智慧在科學計算、工程建模等科學研究中的應用，進一步推動科研程序，加速科學發現的探索步伐。
張憲：現階段，人工智慧在數學推理方面的能力很大程度上依賴於訓練資料的質量和數量。當訓練資料豐富且多樣時，模型能夠在某些數學領域表現出色，甚至能夠解決複雜的奧數題，並能舉一反三地解答變形題目。然而，當訓練資料不足或分佈不均時，即使是簡單的小學題目，模型也可能出錯。這是因為大語言模型本質上是對所學資料的擬合，一旦某領域的訓練資料不足，模型就容易出現“幻覺”，找不到合理的解題方法。
資料不足是當前人工智慧數學推理能力提升的主要阻礙之一。理論上，如果資料足夠豐富，那麼大模型在數學領域的推理能力將有可能達到頂級水平。這就像“題海戰術”與“天才戰術”的差異：透過大量練習，人們可以積累經驗並掌握解題技巧；而天才則能夠憑藉快速學習和理解能力迅速掌握複雜概念。儘管兩者之間的界限難以明確劃分，但一個成績優異的人通常見過許多場景，學過大量知識。因此，豐富的資料對於提升大語言模型的數學推理能力至關重要。需要特別指出的是，在單一任務上，目前的大語言模型需要遠大於人類個體接受的訓練資料量。
張憲：在數學推理這個方向上，我們主要從規則而非資料的角度進行研究，希望大語言模型能夠學習和理解數學領域的規則，並自主擴充套件和應用這些規則來進行泛化推理。
我們開展了形式化、符號化的研究，讓大語言模型可以將自然語言的數學問題轉化為形式化語言，類似於“翻譯”，從而使大語言模型能夠讀懂題目，理解數學問題的內在規律。例如，透過形式化方法，模型可以像計算器一樣處理各種數學運算，展現出強大的泛化能力。
Autoformalizing Mathematical Statements by Symbolic Equivalence and Semantic Consistency
論文連結：
https://openreview.net/pdf?id=8ihVBYpMV4
針對不等式證明方面，我們讓模型在奧林匹克競賽級別的複雜問題上進行了嚴格推理，驗證了形式化模型具備學習並應用數學規則的能力，為推理能力的進一步拓展奠定了基礎。同時，我們還嘗試將這些方法推廣到更廣泛的代數、幾何和數論領域，希望實現大語言模型在數學推理上的全面突破。
Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning
論文連結：
https://openreview.net/pdf?id=FiyS0ecSm0
為了解決大語言模型因訓練資料有限而導致的能力不足問題，我們還進行了數學資料合成方面的研究。透過形式化方法生成多樣化的數學問題與答案對，就像老師為了鍛鍊學生新編寫的變形題，從而為模型提供更豐富的訓練素材。這種方法不僅增加了模型訓練的資料量，還提升了資料的多樣性和質量，讓模型能夠在更多場景中學習和驗證推理能力。
Neuro-Symbolic Data Generation for Math Reasoning
論文連結：
https://openreview.net/pdf?id=CIcMZGLyZW
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation
論文連結：
https://arxiv.org/pdf/2410.15748
然而，對於提升人工智慧效能來說，單純依賴海量資料和計算資源的“規模法則（scaling law）”並非長久之計。因此，我們從生成數學題、理解題目、解答證明這三個方面入手，讓大語言模型能夠更全面地理解數學推理的規律，然後透過一種自動化且可擴充套件的方法來處理複雜的推理問題，而不是僅停留在表面的資料擬合上。
張憲：數學推理是透過運用數學知識以及明確的規則和方法來解決問題，具有較強的邏輯性與確定性。而常識推理則更多依賴於人類在日常生活中積累的經驗和對世界的認知，涉及對各種概念、場景的理解與判斷。
對於“執竿入城”這類問題，不僅需要數學計算能力，還需要對物理空間和物體運動的直觀理解。大語言模型是基於自然語言資料訓練的，缺乏對空間概念和常識的理解。模型本質上並不理解“竿”和“城”的具體概念，只是從文字表面去理解問題，對物體的形狀、運動等概念沒有認知，因此，在解決這類問題時大語言模型容易出錯。這種空間智慧的缺失是大語言模型亟待突破的難題。
張憲：目前來看，用一個大語言模型來處理初高中或本科階段的數學問題是可行的。這一階段的數學知識體系相對固定，問題型別和解題方法較為明確，透過對大量相關資料的學習和訓練，大模型能夠掌握其中的規律，從而進行有效的推理和解答。
但對於前沿的數學領域，業界還沒有明確的解決方案。數學是一個非常有趣且複雜的領域，例如哥德爾不完備定理指出，在特定的公理體系中，可能存在一些雖然正確但無法用當前公理體系證明的命題。當前的人工智慧模型在進行數學推理時，通常採用形式化方法，基於一套固定的公理體系，這使得模型在這套體系下必然會遇到某些難以證明的命題。
人類最偉大之處就在於不斷突破自我，突破底層固有的公理、系統，探索新的規律來解決問題。就像愛因斯坦發現相對論，打破了經典力學的侷限。雖然目前我們的方法在理論上沒有上限，但在涉足前沿數學研究時，確實可能遭遇現有體系無法證明某些命題的困境。這意味著，人工智慧也要跳出現有框架，構建更高級別的公理體系來相容那些無法證明的命題。
張憲：在進行數學推理時，人類會根據需要藉助各種工具，如計算器、查閱資料等，而不是一味地心算。對大語言模型而言，未來在推理時精準呼叫合適工具的能力至關重要。這種能力不僅對數學推理本身非常重要，對於程式碼編寫、常識判斷等領域也同樣具有重要意義。
人工智慧數學推理能力的提升將率先在教育領域發揮作用。具備強大推理能力的模型可以為學生提供更精準、高效的數學學習輔助，幫助他們更好地理解數學概念、掌握解題技巧，併為個性化學習提供支援。
從工業角度來看，當人工智慧在數學形式化推理方面表現出色時，結合其常識和知識儲備，將極大地推動程式碼形式化的發展。這對於工業界開發穩定、可靠的軟體十分關鍵，這也是當前眾多科研團隊積極探索的重要方向之一。
此外，在數學研究領域，儘管讓人工智慧解決所有數學問題不太現實，但它可以在未解決的數學難題上為人類提供新的思路和視角。已經有數學家透過藉助人工智慧的發散性“思維”，再結合自身的專業知識，來尋找解決難題的突破口了。這種人機協作的方式將為數學研究帶來新的發展機遇，也將為未來的科學研究開闢新的路徑。
你也許還想看：