從平面幾何出發(fā)：形式化驗證如何驅動MLLM的推理能力躍遷

在邁向通用人工智能（AGI）的征途中，多模態(tài)大語言模型（MLLMs）雖然在視覺理解與文本生成上展現(xiàn)了驚人的能力，卻始終面臨一道難以逾越的鴻溝：如何在復雜的數(shù)學與幾何推理中，克服固有的幻覺與邏輯斷層？ 現(xiàn)有的 “結果導向” 訓練往往掩蓋了推理過程的脆弱性，導致模型常常 “蒙對答案” 卻 “想錯過程”。這種 “黑盒” 式的學習方式，使得模型難以習得真正魯棒的推理能力。

面對這一挑戰(zhàn)，來自上海交通大學、復旦大學、香港中文大學（深圳）、上海人工智能實驗室等研究機構的團隊提出了一套全新的系統(tǒng)化解決方案：“Formal Enhance Informal Reasoning”（以形式化增強非形式化推理）。該方案的核心洞察在于：利用領域內（In-Domain）極度嚴謹、可驗證的形式化邏輯，可以作為一種強有力的監(jiān)督信號，去規(guī)范和引導模型在非形式化場景下的推理行為。 更進一步，研究發(fā)現(xiàn)這種在嚴謹數(shù)學環(huán)境中習得的邏輯素養(yǎng)，不僅僅局限于幾何題，更能作為一把通用的鑰匙，解鎖模型在通用數(shù)學乃至更廣泛推理任務上的分布外（OOD）泛化能力。

基于這一理念，團隊歷經(jīng)三個階段的探索，構建了從數(shù)據(jù)底層到模型頂層的完整閉環(huán)：

• TrustGeoGen（數(shù)據(jù)基石）：針對現(xiàn)有數(shù)據(jù)噪聲大、邏輯自洽性差的問題，構建了首個形式化驗證的幾何數(shù)據(jù)合成引擎。通過集成多模態(tài)對齊、全路徑形式化驗證及 GeoExplore 探索算法，生成了 GeoTrust 數(shù)據(jù)集，確保每一條數(shù)據(jù)的邏輯鏈條都經(jīng)過數(shù)學層面的嚴格驗算，為后續(xù)工作提供數(shù)據(jù)和驗證環(huán)境保障。
• GeoBench（深度診斷）：為了精準定位模型推理短板，提出了基于分層能力評估的基準測試。它將幾何推理拆解為視覺感知、目標規(guī)劃、定理應用、自我反思四個層級，并引入了 “無關條件過濾” 與 “邏輯糾錯” 等高階任務，揭示了推理模型在復雜任務中的邏輯局限性。
• SGVR（能力躍遷）：針對 “結果監(jiān)督” 的不足，提出了 Sub-Goal Verifiable Reward 訓練框架。該框架將抽象證明轉化為可執(zhí)行的數(shù)值子目標（Milestones），利用 Skeleton Rate 提供密集獎勵信號。實驗證明，這種訓練不僅在幾何領域提升顯著，更實現(xiàn)了向通用數(shù)學及邏輯推理任務的強力遷移。

相關論文：

• 論文標題：TrustGeoGen: Formal-Verified Data Engine for Trustworthy Multi-modal Geometric Problem Solving
• 論文鏈接：https://arxiv.org/abs/2504.15780

• 論文標題：GeoBench: Rethinking Multimodal Geometric Problem-Solving via Hierarchical Evaluation
• 論文鏈接：https://arxiv.org/abs/2512.24119

• 論文標題：Milestones over Outcome: Unlocking Geometric Reasoning with Sub-Goal Verifiable Reward
• 論文鏈接：https://arxiv.org/abs/2601.05073

如何構筑可信推理的基石？

TrustGeoGen：形式化驗證的幾何數(shù)據(jù)合成引擎

“如何使訓練數(shù)據(jù)沒有邏輯漏洞？”

連貫且準確的推理過程是可信推理的基礎，每一步推理都應該由明確的前置結論和定理推導出。如圖 1 所示，TrustGeoGen 用 constructor, reasoner, sampler 和 translator 四個模塊來構造問題、擴充推理圖譜、回溯推理路勁和轉譯自然表達。其中，形式化推理引擎 DDAR 被用來保證每一個結論都由預定義的定理規(guī)則得到，從而保證了推理鏈路的連貫性和可解釋性。

圖 1 TrustGeoGen 可信數(shù)據(jù)構造流程

然而，形式化引擎以遍歷的方式獲得每一個推理步驟，它可以保證推理步驟是正確的，但是無法解釋為什么應該這樣做。這樣的數(shù)據(jù)仿佛解題過程被省略的參考答案，只能讓大模型記住結果而無法真正掌握推理能力。如圖 2 所示，connection thinking 被用來幫助構造思考過程性數(shù)據(jù)。每個推理步驟前，connection thinking 都會顯式地、根據(jù)最終目標來分析當前已經(jīng)擁有的結論和下一步應該得到什么結論。將推理步驟以深度思考的方式連接到一起，讓模型真正掌握推理能力。

圖 2 過程性思考數(shù)據(jù)構造流程

最后，推理的魅力在于結合已有的信息向未知發(fā)起沖鋒。這個過程中可能存在錯誤，也需要進行多次的驗證。掌握更多的思維模板（而不是只會鏈式思考）可以幫助模型應對不同的情況。如圖 3 所示，在 sampler 階段采用不同的采樣方式，可以獲得具有不同思維模板的推理數(shù)據(jù)，豐富大模型的推理 “技能庫”。

圖 3 多解和回溯思維模板數(shù)據(jù)構造示意圖

TrustGeoGen 不僅以可驗證的方式生成大量的幾何推理數(shù)據(jù)，更關注到了自然語言推理與形式化推理的差異，從模型訓練的角度來生成連貫可信的推理數(shù)據(jù)，為提高多模態(tài)大語言模型的推理能力奠定了基礎。

推理短板究竟在哪里？

GeoBench：從感知到反思的分層診斷基準

“做對了幾何題，真的意味著模型‘懂’了幾何嗎？”

當我們?yōu)槎嗄B(tài)大模型在 GeoQA 等基準上超越人類的表現(xiàn)歡呼時，一個嚴峻的問題被掩蓋了：現(xiàn)有的評估往往只看最終答案，卻忽視了推理過程的嚴謹性。模型是真正掌握了空間邏輯，還是僅僅記住了教科書里的解題套路，甚至只是為了正確答案而在作 reasoning hacking？為了刺破這層迷霧，精準定位模型能力的邊界，我們提出了 GeoBench —— 一個基于 TrustGeoGen 數(shù)據(jù)引擎而構建的分層診斷基準。

GeoBench 不再滿足于單一的分數(shù)，而是將復雜的幾何推理能力拆解為四個層層遞進的維度：

1.視覺感知（Visual Perception）：模型能否從圖中精準提取數(shù)值與結構信息？

2.目標導向規(guī)劃（Goal-Oriented Planning）：模型能否將大問題拆解為可操作的子目標？

3.嚴謹定理應用（Rigorous Theorem Application）：模型能否在眾多定理中精準篩選出適用的那一條？

4.自我反思回溯（Self-Reflective Backtracking）：當推理誤入歧途時，模型能否及時發(fā)現(xiàn)并修正？

圖 4 GeoBench 概覽：利用 TrustGeoGen 引擎生成包含圖像、問題及推理圖的形式化驗證幾何題，并基于四個推理能力層級，系統(tǒng)化構建分層評測任務

基于 TrustGeoGen 引擎生成的 1021 個形式化驗證樣本，我們設計了六大核心任務對模型進行全方位評估。實驗結果不僅揭示了推理模型的短板，更帶來了一些全新的發(fā)現(xiàn)：

• 能力斷層：即使是 OpenAI-o3 這樣的頂尖推理模型，隨著任務復雜度的提升，性能也呈現(xiàn)顯著下降趨勢。
• 關鍵瓶頸：子目標分解（Sub-Goal Decomposition）無關條件過濾（Irrelevant Premise Filtering）是決定解題成敗的最關鍵因素。這意味著，比起單純的計算能力，模型更缺乏 “排除干擾、規(guī)劃路徑” 的大局觀。
• CoT 的反作用：思維鏈（Chain-of-Thought）并非萬能藥。在涉及 “錯誤定位” 的高階反思任務中，CoT 提示甚至會產(chǎn)生負面干擾，導致模型在錯誤的路徑上越走越遠。

表 1 模型在 GeoBench 的 6 個任務上的表現(xiàn)與求解出最終正確答案的相關性（spearman 系數(shù)）

GeoBench 的出現(xiàn)，不僅是一次評測標準的升級，更為未來的幾何推理系統(tǒng)指明了進化方向：從盲目追求答案正確率，轉向對推理全過程的精細化掌控。

結果監(jiān)督是否足夠？

SGVR：用可驗證的 “里程碑” 引導通用推理泛化

“平面幾何訓練場可以實現(xiàn)域外泛化嗎？”

GeoBench 的診斷揭示了傳統(tǒng)訓練的致命弱點：模型常因 “虛假相關性” 而 “蒙對結果”，中間過程卻充滿幻覺。為了打破這種 “黑盒”，我們提出 SGVR (Sub-Goal Verifiable Reward) 框架，主張 “里程碑重于結果”（Milestones over Outcome）。我們利用 TrustGeoGen 將抽象證明拆解為一連串可自動驗證的數(shù)值子目標，并引入Skeleton Rate (SR)作為核心指標 —— 它不再只看最終答案，而是計算推理鏈條中正確 “路標” 的比例。配合 GRPO 算法，這種密集的中間獎勵強迫模型 “步步為營”，只有每一步邏輯都經(jīng)得起驗證，才能獲得高分。

圖 5 SGVR 的核心機制：利用形式化引擎將復雜的幾何證明題分解為多個可驗證的數(shù)值子目標（Milestones）。通過引入 Skeleton Rate (SR)，模型在每完成一個中間路標時都能獲得即時的密集獎勵反饋，從而糾正邏輯幻覺，確保推理路徑的每一步都精準可信。

這種訓練帶來了意想不到的驚喜：幾何邏輯的 “溢出效應”。 SGVR 不僅讓模型在幾何推理任務上實現(xiàn)了9.7%的顯著提升，更展現(xiàn)出了強大的跨域泛化能力。在完全未見過的 通用數(shù)學（AMC, MATH-500） 和 通用邏輯推理 任務中，模型在零樣本（Zero-shot）條件下分別獲得了8.0%和2.8%的性能躍升。這有力地證明：在高度嚴謹?shù)膸缀苇h(huán)境中習得的 “驗證思維”，能夠轉化為通用的邏輯素養(yǎng)，成為解鎖復雜推理難題的關鍵鑰匙。

圖 6 SGVR 在顯著提升幾何推理能力的同時，展現(xiàn)了卓越的 “溢出效應”：在完全未接觸過的通用數(shù)學（AMC, MATH-500）和邏輯推理任務中，模型性能均實現(xiàn)了顯著躍升

在確定了 “過程監(jiān)督” 的有效性后，一個核心問題隨之而來：我們需要對推理鏈條進行多大程度的干預？在 SGVR 的消融實驗中，我們通過調節(jié)Mask Ratio（即隱藏子目標的比例）探索了驗證密度對模型能力的影響。

圖 6 驗證密度對推理性能的影響 —— 尋找監(jiān)督的 “黃金分割點”

圖 6 的實驗結果揭示了一個有趣的現(xiàn)象：驗證并非越密越好，而是存在一個 “黃金比例”。當我們將驗證顆粒度保持在適中水平時，模型不僅能獲得足夠的糾錯信號，還能保留一定的自主推理空間。一旦驗證過于稀疏，模型會退回到 “結果賭博” 的老路；而過度的干預則可能導致模型過擬合于特定的驗證路徑，喪失了處理復雜變體的靈活性。

形式化增強的未來：通往魯棒性推理的新范式

面對當前推理模型普遍存在的邏輯斷層與過程不可控問題，團隊通過構建從可信數(shù)據(jù)合成、分級能力診斷到過程監(jiān)督訓練的一整套系統(tǒng)化方案，構建了一個完整的邏輯閉環(huán)。該閉環(huán)的核心在于：利用形式化驗證的嚴謹性來約束與增強非形式化的推理過程，并通過在特定領域內的深度訓練，賦予模型跨越領域邊界的廣義泛化能力。

這一研究范式表明，平面幾何不僅僅是評估模型能力的試金石，更是訓練 AI 具備高階邏輯思維的最佳演練場。未來，團隊將致力于將這種 “形式化增強” 的范式拓展至通用數(shù)學、代碼生成、物理模擬等更廣泛的領域，旨在構建更可信、更魯棒且具備強大泛化能力的通用推理大模型。

關于 FrontierX Lab:

FrontierX Lab 由上海交通大學人工智能學院助理教授夏紉秋創(chuàng)立，致力于探索人工智能的前沿邊界，實驗室核心方向涵蓋形式化增強的推理大模型、多模態(tài)文檔理解以及 AI 驅動的自動化科學發(fā)現(xiàn)等。實驗室長期招募對符號 AI、多模態(tài)推理及前沿科學探索充滿熱情的博士 / 碩士研究生、科研助理及實習生，歡迎發(fā)送簡歷至 xiarenqiu@sjtu.edu.cn，共同拓展 AI 推理的認知邊界！