從平面幾何出發(fā)：形式化驗(yàn)證如何驅(qū)動(dòng)MLLM的推理能力躍遷

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

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

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

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

相關(guān)論文：

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

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

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

如何構(gòu)筑可信推理的基石？

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

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

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

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

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

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

最后，推理的魅力在于結(jié)合已有的信息向未知發(fā)起沖鋒。這個(gè)過(guò)程中可能存在錯(cuò)誤，也需要進(jìn)行多次的驗(yàn)證。掌握更多的思維模板（而不是只會(huì)鏈?zhǔn)剿伎迹┛梢詭椭Ｐ蛻?yīng)對(duì)不同的情況。如圖 3 所示，在 sampler 階段采用不同的采樣方式，可以獲得具有不同思維模板的推理數(shù)據(jù)，豐富大模型的推理 “技能庫(kù)”。

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

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

推理短板究竟在哪里？

GeoBench：從感知到反思的分層診斷基準(zhǔn)

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

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

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

1.視覺(jué)感知（Visual Perception）：模型能否從圖中精準(zhǔn)提取數(shù)值與結(jié)構(gòu)信息？

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

3.嚴(yán)謹(jǐn)定理應(yīng)用（Rigorous Theorem Application）：模型能否在眾多定理中精準(zhǔn)篩選出適用的那一條？

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

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

基于 TrustGeoGen 引擎生成的 1021 個(gè)形式化驗(yàn)證樣本，我們?cè)O(shè)計(jì)了六大核心任務(wù)對(duì)模型進(jìn)行全方位評(píng)估。實(shí)驗(yàn)結(jié)果不僅揭示了推理模型的短板，更帶來(lái)了一些全新的發(fā)現(xiàn)：

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

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

GeoBench 的出現(xiàn)，不僅是一次評(píng)測(cè)標(biāo)準(zhǔn)的升級(jí)，更為未來(lái)的幾何推理系統(tǒng)指明了進(jìn)化方向：從盲目追求答案正確率，轉(zhuǎn)向?qū)ν评砣^(guò)程的精細(xì)化掌控。

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

SGVR：用可驗(yàn)證的 “里程碑” 引導(dǎo)通用推理泛化

“平面幾何訓(xùn)練場(chǎng)可以實(shí)現(xiàn)域外泛化嗎？”

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

圖 5 SGVR 的核心機(jī)制：利用形式化引擎將復(fù)雜的幾何證明題分解為多個(gè)可驗(yàn)證的數(shù)值子目標(biāo)（Milestones）。通過(guò)引入 Skeleton Rate (SR)，模型在每完成一個(gè)中間路標(biāo)時(shí)都能獲得即時(shí)的密集獎(jiǎng)勵(lì)反饋，從而糾正邏輯幻覺(jué)，確保推理路徑的每一步都精準(zhǔn)可信。

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

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

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

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

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

形式化增強(qiáng)的未來(lái)：通往魯棒性推理的新范式

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

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

關(guān)于 FrontierX Lab:

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