从平面几何出发：形式化验证如何驱动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 推理的认知边界！