
(本文閱讀時間:15分鐘)
編者按:儘管近年來人工智慧的能力迅速增強,但在複雜的推理任務中仍存在不足。微軟亞洲研究院的研究員們從多個角度對此展開研究,不斷探索提升大模型推理能力的新途徑。從利用蒙特卡洛樹搜尋模擬人類“深度思考”過程的 rStar-Math,到基於規則的強化學習方法 Logic-RL;從融合大語言模型數學直覺與符號方法的 LIPS,到提升自動形式化準確性的新框架;再到自動生成高質量、有監督數學資料的神經符號框架,以及統一推理框架 CoR 和關鍵計劃步驟學習 CPL 的提出,每一項研究都為提升大模型的推理能力提供了新的視角和方法。
人工智慧的快速發展,使其在眾多領域展現出強大的能力,同時也不斷催生出人們對其更高的期待,希望人工智慧能夠具備深度的思考和推理能力,幫助人類解決各種“燒腦”的現實複雜問題。
為了提升大模型的推理能力,微軟亞洲研究院的研究員們從三個方向開展研究:一是透過改進模型本身來增強其推理能力,使較小規模的模型也能具有強大的推理效能;二是深入學習數學推理的規則,以提高大語言模型的可靠性;三是增強推理的泛化能力,讓模型能夠在跨領域的任務中靈活應用,從而促進通用人工智慧的進步。

“基於世界知識訓練的大模型雖然擁有海量的知識儲備,但是現有模型並沒有充分發揮其所蘊含的全部潛力。不僅如此,現有的模型還缺乏持續學習的能力,這與人類不斷學習新知識、填補認知空白的能力形成鮮明對比。”微軟亞洲研究院首席研究員張麗說。卓越的推理能力往往依賴於大規模模型的支援,因此,一些科研人員也在探索如何讓類似的推理能力可以在規模較小的模型中實現。
在傳統的推理模式下,大模型面對複雜問題時常常採用簡單直接的“直覺式”推理來生成答案。這種方式雖然速度較快,但很容易出錯。相比之下,人類會對問題進行逐步分析,嘗試多種思路,權衡利弊後再給出答案。鑑於此,研究員們提出了 rStar-Math,其核心在於利用蒙特卡洛樹搜尋(MCTS),模擬人類的“深度思考”過程,讓小語言模型在推理能力方面達到更高的水準。
rStar-Math 透過三個步驟實現了自我進化:首先,將複雜的數學問題分解為多個推理步驟,使模型能夠逐步探索並驗證每一步的貢獻,確保小模型生成的推理軌跡由正確、高質量的中間步驟組成;其次,訓練一個作為過程偏好模型(PPM)的小模型,用於可靠地為每個數學推理步驟預測獎勵標籤,從而實現所需的過程獎勵建模以及可靠的標註;最後,透過一個四輪自我進化方案,從零開始逐步構建前沿的策略模型和 PPM,每一輪都使用最新的策略模型和 PPM 進行蒙特卡洛樹搜尋,進而逐步進化,訓練出更強的策略模型和 PPM。
實驗顯示,rStar-Math 在四個小語言模型(15億 – 70億引數)上驗證了自身的有效性。在美國數學奧林匹克競賽(AIME)中,rStar-Math 平均能夠解決53.3%(8/15)的問題,排名在前20%最優秀的高中數學學生之列。
rStar-Math: Small LLMs can master math reasoning with self-evolved deep thinking
論文連結:
https://arxiv.org/pdf/2501.04519

圖1:rStar-Math 示意圖
研究員們還提出了基於規則的強化學習方法 Logic-RL,透過合成邏輯謎題作為訓練資料來提高模型在複雜邏輯問題上的推理能力。Logic-RL 引入了一種實用系統提示和嚴格的格式獎勵函式,避免推理模型走捷徑。例如,模型在生成答案時,必須按照特定格式組織推理過程和答案,只有當推理過程和答案都符合要求時,才能獲得較高獎勵,以此確保推理過程的完整性和準確性。
經過 Logic-RL 訓練後的模型不僅在邏輯謎題上表現出色,在70億引數小模型的數學競賽基準測試(如 AIME和 AMC)中也展現出了強大的泛化能力,準確率分別提高了125%和38%。
Logic-RL: Unleashing LLM reasoning with rule-based reinforcement learning
論文連結:
https://arxiv.org/pdf/2502.14768

數學作為科學的基石,具有嚴密的邏輯性和高度的精確性。對於人工智慧而言,解決數學推理難題將大幅提升人工智慧的推理能力,也將促進模型在各個領域的廣泛應用。然而,僅僅依靠大模型的自然語言處理能力,往往難以滿足數學推理所需的嚴格標準。為此,研究員們運用形式化和符號化的研究方法,幫助模型學習人類已有的數學方法和工具,掌握數學規則,提升推理的效率與準確性。
“自然語言是人類的語言,並不是計算機或大模型的原生語言,它們並不能直接理解自然語言。我們希望將大語言模型的輸出轉換為程式碼形式,並將其對映到公理中,例如‘1+1=2’這樣不證自明的公理,從而驗證模型輸出的正確性。這類似於人類在交流時將聽到的話語轉換為自己的理解,而我們則是透過形式化流程將其轉換為計算機能夠理解的工具。”微軟亞洲研究院高階研究員張憲說。
數學語言涵蓋數學定理、不等式證明等,與大語言模型的語言體系存在顯著差異。要讓大模型理解數學問題,首先需要透過形式化和符號化的方法將數學題目轉化為程式碼形式,再對映為計算機可理解的公理。基於此,研究員們設計了基於大模型的符號推理不等式證明器(LLM-based inequality prover with symbolic reasoning)LIPS。它創造性地融合了大模型的數學直覺與符號方法所編碼的領域特定見解,以確定數學推理中哪些部分最適合大模型,哪些部分更適合採用符號方法。
透過分析人類解決此類問題的思路,LIPS 提煉出兩種策略:一是由符號方法處理的縮放(scaling);二是由大模型處理的重寫(rewriting)。在使用來自多個數學競賽的161個極具挑戰性的不等式對 LIPS 進行評估後,結果顯示 LIPS 展現出了目前最先進的效能,並且在無需額外訓練資料的情況下,大大優於現有的大模型和符號方法。
Proving Olympiad inequalities by synergizing LLMs and symbolic reasoning
論文連結:
https://openreview.net/pdf?id=FiyS0ecSm0

圖2:LIPS 符號推理不等式證明器
儘管形式化方法使大模型在多種數學推理任務中表現出巨大潛力,但大模型在自動形式化資料陳述上的成功率仍然較低。具體而言,在大模型的自動形式化中,一次透過率(排名第一的生成結果正確)和 k 次透過率(排名前 k 的生成結果中有一個正確)之間有明顯的差異。
為了縮小這一差距,研究員們引入了一種新框架,從兩個創新且互補的維度建立自動形式化的自一致性——符號等價性和語義一致性。符號等價性將傳統的比較(如最終答案和執行行為)進行擴充套件,以驗證自動形式化候選結果之間的邏輯等價性。語義一致性則透過測量重新非形式化(反向翻譯)結果與原始自然語言陳述之間的嵌入相似性,糾正符號等價性可能忽略的意外推理差異。這種方法確保了自動形式化過程能夠保留原始陳述的預期含義和連貫性。在 MATH 和 miniF2F 資料集上的實驗表明,該方法極大地提高了自動形式化的準確性,在各種大語言模型和基線方法上實現了高達0.22-1.35倍的相對改進。
Autoformalizing mathematical statements by symbolic equivalence and semantic consistency
論文連結:
https://openreview.net/pdf?id=8ihVBYpMV4

圖3:自動形式化框架
此外,研究員們認為,高質量數學資料集的極度匱乏也是限制大語言模型數學推理能力提升的關鍵因素之一。為了突破這一困境,研究員們提出了一種神經符號框架,用於自動生成高質量、有監督的數學資料。這一正規化結合了神經和符號的優勢,一方面,透過系統取樣在符號空間中生成多樣化的數學問題,並利用符號求解器保證問題的有效性;另一方面,大模型能夠有效地支援從符號空間到自然語言空間的轉換,確保新生成的形式化問題與其相應的自然語言版本保持一致。
Neuro-symbolic data generation for math reasoning
論文連結:
https://openreview.net/pdf?id=CIcMZGLyZW

圖4:神經符號框架

推理泛化能力是衡量人工智慧是否真正具備通用性的重要指標。具備強大泛化能力的模型,能夠跨越不同領域的知識邊界,做到“舉一反三”,進而拓展人工智慧的應用範圍和價值。研究員們發現,模型經過數學資料訓練後,其推理能力在科學、程式碼等多個領域都有顯著提升。這一發現為提升大模型的推理泛化能力提供了新的思路和方向。
透過將自然語言、程式碼和符號語言三種推理正規化融入同一條推理軌跡,研究員們提出了統一推理框架 CoR(Chain-of-Reasoning)。其中,自然語言有助於理解問題的背景和需求,程式碼語言擅長精確的計算和邏輯處理,符號語言能以簡潔、嚴謹的方式表達數學和邏輯關係。CoR 允許模型先基於某一正規化推理,再根據問題的不同階段和需求靈活切換正規化,在先前生成內容的基礎上繼續進行多正規化的協同推理,實現通用數學任務上的推理泛化。
另外,利用調整提示詞(prompt),模型還可以改變推理深度和使用的正規化數量,極大提高了其對不同任務的適應性。在5個數學推理資料集的測試中,CoR 均取得了大幅的提升效果,展現出令人驚喜的通用數學解題能力——既能解決數學計算問題,又能解決數學證明問題。
Chain-of-Reasoning: Towards unified mathematical reasoning in LLMs via a multi-paradigm perspective
論文連結:
https://arxiv.org/pdf/2501.11110

圖5:不同正規化下的推理過程
此外,現有的大模型主要側重於提升特定任務或特定領域(如數學或程式設計)的推理能力,並未充分解決模型在各種推理任務中的泛化能力問題。為了增強推理任務中的泛化能力,研究員們建議在高階抽象計劃的動作空間內進行搜尋,而不是侷限於通常會限制泛化能力的特定任務動作空間。
透過分析此前利用大模型生成推理計劃以及特定任務解決方案,來提升推理能力的相關研究,研究員們發現,特定任務的解決方案與特定任務的技能密切相關。相比之下,計劃代表了一種解決問題的抽象思維,如決定應用哪些知識或如何分解問題,這有助於模型培養更廣泛的、與任務無關的能力,進而提升泛化能力。
微軟亞洲研究院首席研究員韓雪婷表示,“人類在思考解決問題時,存在一些共性策略。例如,將複雜問題拆解為子問題,從眾多資訊中提取關鍵部分,以及根據特定資訊回憶、調取已有知識,像是數學中的定理或程式設計中的演算法等。透過學習這些解題策略,當遇到新問題時,大模型也會形成一種類似人類解題的思路,從而更有效地解決問題。”
基於此,研究員們提出了關鍵計劃步驟學習 CPL(Critical Plan Step Learning)方法,它由兩個關鍵部分組成:基於計劃的搜尋和透過步驟級優勢偏好最佳化(Step-APO),來學習關鍵計劃步驟。基於計劃的搜尋利用蒙特卡洛樹搜尋在多步推理任務中探索不同的計劃步驟,透過建立計劃樹,幫助模型獲得與任務無關的技能,提升模型在不同任務中的泛化能力。Step-APO 則整合了利用蒙特卡洛樹搜尋獲得的步驟級偏好對的優勢估計,使模型能夠學習步驟之間的細粒度偏好,識別關鍵計劃步驟,並弱化錯誤步驟的影響,從而增強模型的整體推理能力,提升模型在不同任務中的泛化能力。
CPL: Critical plan step learning boosts LLM generalization in reasoning tasks
論文連結:
https://arxiv.org/pdf/2409.08642

圖6:CPL 示意圖

從數學推理到提升模型推理的泛化能力,從直覺式的快速回答到經過深度思考的回答,微軟亞洲研究院的研究員們持續探索大模型推理效能的邊界。透過引入新的視角和方法,他們不僅推動了該領域的前沿發展,還帶動了更多相關研究取得新進展。隨著大語言模型效能和可靠性的提升,人工智慧在現實場景中的應用範圍也在不斷擴大,為智慧教育、智慧醫療、智慧科研等領域提供了強有力的技術支援。
然而,我們也必須認識到當前大模型仍面臨諸多挑戰,如生成內容時出現的幻覺問題以及推理過程不夠嚴謹等。這些問題在特定應用場景中可能會帶來嚴重後果。例如,在科學研究中,模型推理的偏差可能導致錯誤的研究方向,造成資源的巨大浪費;在醫療健康領域,不準確的資訊可能直接危及患者的生命安全。
除了前文所述的研究,微軟亞洲研究院的研究員們也在嘗試從更多不同的角度提升人工智慧的推理能力,包括使用 LLMs 為 Rust 程式碼自動生成正確性證明,設計與 Verus 驗證工具獨特功能相匹配的方法;提出 SAFE 框架,解決 Rust 程式碼形式化證明中資料稀缺的問題;推出 Alchemy 框架,透過變化符號構建形式化定理,緩解神經定理證明(NTP)中的資料不足問題,等等。這些成果為大語言模型的推理能力提升提供了更多可能性,也為未來的研究方向提供了豐富的思路。
其他相關研究:
-
AutoVerus: Automated proof generation for rust codehttps://arxiv.org/abs/2409.13082
-
Automated proof generation for rust code via self-evolutionhttps://arxiv.org/pdf/2410.15756v1
-
Alchemy: Amplifying theorem-proving capability through symbolic mutationhttps://arxiv.org/pdf/2410.15748
-
Mutual reasoning makes smaller LLMs stronger problem-solvershttps://arxiv.org/pdf/2408.06195
你也許還想看:
