可验证几何问题求解：求解器驱动的自动形式化与定理提出

背景

几何问题求解（Geometry Problem Solving, GPS）近年来日益采用神经符号范式（neuro-symbolic paradigm），旨在结合神经网络的直觉能力与符号逻辑的严谨性。然而，现有的框架在两个核心阶段面临严重的瓶颈：

1. 自动形式化（Autoformalization）：目前的方法通常将多模态翻译视为一个静态任务，将其与下游求解器的兼容性脱钩。这意味着视觉信息转化为符号语言的过程往往是孤立的，未能充分考虑后续逻辑推导的需求。
2. 定理预测（Theorem Prediction）：在推理过程中，求解器经常因为固定的规则库限制而陷入演绎僵局（deductive impasse），导致无法继续推进证明过程。

为了解决上述问题，研究人员提出了一种新的框架，旨在通过闭环反馈机制，将多模态感知与符号执行紧密结合，从而实现可验证的问题求解能力。

核心内容

本文提出了 SD-GPS（Solver-Driven Geometry Problem Solving，求解器驱动的几何问题求解）框架。该框架的核心创新在于将符号求解器（symbolic solver）视为整个形式化过程和演绎过程中的“执行预言机”（execution oracle）。SD-GPS 主要包含两个关键模块：

1. 求解器驱动的自动形式化（Solver-Driven Autoformalization）

传统的自动形式化往往缺乏对“可执行性”的关注。SD-GPS 通过以下统一模块解决了这一问题：

• 基础模型：基于 QwenVL3-2B 模型构建。
• 训练信号：将“可执行性”（executability）作为核心训练信号。
• 方法融合：将监督式的形式语言适应（supervised formal-language adaptation）与可解性引导的强化学习（solvability-guided reinforcement learning）统一到一个模块中。
• 目标：确保生成的符号表示不仅语义正确，而且能够被下游的符号求解器成功执行和推理。

2. 验证定理提出（Verified Theorem Proposing）

针对求解器在固定规则库下容易陷入僵局的问题，SD-GPS 引入了一个“僵局感知代理”（impasse-aware agent）：

• 动态引理生成：该代理能够根据当前的证明状态（current proof states），动态地提出局部辅助引理（local auxiliary lemmas）。
• 符号验证过滤：为了确保推导的正确性（soundness），所有提出的引理都必须通过符号验证（symbolic verification）的过滤。只有经过验证的引理才会被纳入证明过程。
• 打破僵局：通过这种方式，系统能够突破固定规则库的限制，自主发现并引入新的推理步骤，从而走出演绎僵局。

关键要点

• 闭环反馈机制：SD-GPS 的核心思想是“求解器驱动”。它不再将形式化和推理视为线性、独立的步骤，而是利用求解器的反馈来指导形式化的生成和定理的提出，形成了“感知-形式化-执行-反馈”的闭环。
• 可执行性优先：在自动形式化阶段，不再仅仅追求从图像到文本的翻译准确率，而是追求生成的符号语言能否被求解器“执行”。这通过结合监督学习和强化学习来实现。
• 动态定理发现：传统的神经符号方法依赖预定义的规则库，容易遇到瓶颈。SD-GPS 通过引入僵局感知代理，能够根据证明进度动态生成并验证新的辅助引理，极大地扩展了推理能力。
• 模型基础：该框架建立在 QwenVL3-2B 这一多模态大语言模型之上，利用其强大的多模态理解能力进行初始的形式化翻译。
• 验证机制：所有由 AI 提出的新定理或引理，都必须经过严格的符号逻辑验证，确保了最终结果的可验证性和可靠性，避免了纯神经网络方法常见的“幻觉”问题。

意义与影响

在 Geometry3K 和 PGPS9K 这两个标准几何问题求解数据集上的实证评估表明，SD-GPS 在标准完成（standard completion）、多项选择（multiple-choice）以及跨模态参考（cross-modal reference）设置下，均一致地优于现有的多模态大语言模型（MLLM）、纯神经网络方法以及现有的神经符号方法。

这一成果证明了以下观点：

1. 闭环的重要性：在多模态感知与符号执行之间建立闭环，能够显著提升几何推理的能力。
2. 神经代理的根基：为神经智能体（neural agents）如何被形式化系统（formal systems）所“接地”（grounded）提供了深刻的见解。通过形式化系统的约束和验证，神经网络可以克服其固有的不确定性，实现真正可验证的问题求解能力。
3. 范式转变：从静态的多模态翻译转向动态的、求解器驱动的形式化与定理生成，代表了神经符号 AI 在几何推理领域的一个重要进步。