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

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

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

基于這一理念，團隊歷經三個階段的探索，構建了從數據底層到模型頂層的完整閉環：

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

相關論文：

• 論文標題：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：形式化驗證的幾何數據合成引擎

“如何使訓練數據沒有邏輯漏洞？”

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

圖 1 TrustGeoGen 可信數據構造流程

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

圖 2 過程性思考數據構造流程

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

圖 3 多解和回溯思維模板數據構造示意圖

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

推理短板究竟在哪里？

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

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

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

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

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

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

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

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

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

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

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

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

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

結果監督是否足夠？

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

“平面幾何訓練場可以實現域外泛化嗎？”

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

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

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

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

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

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

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

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

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

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

關于 FrontierX Lab:

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