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

# 可验证的几何问题求解：求解器驱动的自动形式化与定理提出
来源：https://arxiv.org/html/2606.27926
###### 摘要

几何问题求解（Geometry Problem Solving）正日益采用神经符号范式，将神经直觉与符号严谨性相结合。然而，当前的框架在两个核心阶段面临严重瓶颈：自动形式化（autoformalization）将多模态翻译视为一个与下游求解器兼容性解耦的静态任务，以及定理预测（theorem prediction）中求解器常因固定规则库而陷入推理僵局。为解决这些问题，我们提出 SD-GPS，一个以求解器为驱动的框架，在形式化和演绎两个阶段均将符号求解器视为执行预言机。首先，求解器驱动的自动形式化将监督式形式语言适应与可解性引导的强化学习统一到基于 QwenVL3-2B 的单一模块中，使可执行性成为核心训练信号。其次，可验证的定理提出引入了一个僵局感知代理，该代理从当前证明状态中提出局部辅助引理，并通过符号验证过滤所有提议以确保正确性。在 Geometry3K 和 PGPS9K 上的实验评估表明，SD-GPS 在标准完成、多项选择和跨模态引用场景中持续优于现有的多模态大语言模型、神经和神经符号方法，证明了多模态感知与符号执行之间闭环的构建能显著提升几何推理能力，并为神经代理如何通过形式系统落地以实现可验证的问题求解能力提供了深刻见解。

## 1 引言

几何问题求解（GPS）旨在从文本问题描述及其对应图形中推导出数学解（Chen 等, 2022 (https://arxiv.org/html/2606.27926#bib.bib35); Gelernter 等, 1960 (https://arxiv.org/html/2606.27926#bib.bib41); Sachan 和 Xing, 2017 (https://arxiv.org/html/2606.27926#bib.bib42); Wu, 1986 (https://arxiv.org/html/2606.27926#bib.bib43); Wu 等, 2024 (https://arxiv.org/html/2606.27926#bib.bib2); Peng 等, 2023 (https://arxiv.org/html/2606.27926#bib.bib5)）。为应对几何固有的复杂性，许多近期系统采用神经符号范式（Trinh 等, 2024 (https://arxiv.org/html/2606.27926#bib.bib22); Chervonyi 等, 2025 (https://arxiv.org/html/2606.27926#bib.bib39)）。这种双过程方法利用神经网络作为“感知前端”，符号引擎作为“逻辑后端”（Wu 等, 2022a (https://arxiv.org/html/2606.27926#bib.bib28)）。在该框架中，推理流程由两个核心模块驱动：(i) 自动形式化，将多模态原始输入转换为可执行的正式表示；(ii) 定理预测，选择或提出可用于求解器推导解的定理实例。这种模块化架构使系统能够同时利用深度学习的直觉识别和形式逻辑的确定性严谨性。

在自动形式化阶段，目标是将多模态输入转换为求解器可读的谓词。然而，现有的 GPS 框架通常采用“解耦而后纠正”的范式（Lu 等, 2021 (https://arxiv.org/html/2606.27926#bib.bib1); Zhao 等, 2025 (https://arxiv.org/html/2606.27926#bib.bib9); Ping 等, 2026 (https://arxiv.org/html/2606.27926#bib.bib10)），其中独立的神经模块分别解析图形和形式化文本，随后通过事后纠正步骤解决指代歧义（Zhao 等, 2025 (https://arxiv.org/html/2606.27926#bib.bib9); Ping 等, 2026 (https://arxiv.org/html/2606.27926#bib.bib10)）。除了这种结构上的脆弱性之外，更根本的限制在于目标错位。当前方法将形式化视为一个静态的单向语义翻译任务，优化昂贵的人工标注逻辑形式，强调语言忠实度而非计算可解性。因此，形式化过程与基于求解器的问题求解最终目标不一致，高语义准确性并不一定能转化为下游推理的有效或可执行表示。

即使提供了准确的形式化，定理预测阶段仍面临第二个关键瓶颈：固定的定理库和有限的搜索预算可能使求解器陷入推理僵局。最先进的 GPS 框架（Ping 等, 2026 (https://arxiv.org/html/2606.27926#bib.bib10); Zhang 等, 2024b (https://arxiv.org/html/2606.27926#bib.bib49)）通常使用预定义的几何规则库，因此当问题需要罕见的定理实例、小的辅助构造或循环性、相似性、比例性等中间关系时，它们可能失败。因此，我们将定理提出视为一个有界、验证器控制的提议问题，而非自由形式的公理生成：神经代理可以从当前证明状态中建议局部辅助引理，但只有符号后端可以接受、拒绝和使用它们。

请参阅图注

图 1：现有方法的性能比较。

为解决这些错位问题，我们提出 SD-GPS，这是一个求解器驱动的框架，在形式化和演绎两个阶段都将符号求解器视为执行预言机。首先，求解器驱动的自动形式化将解耦流程替换为基于 QwenVL3-2B 的统一多模态形式化器。它联合读取原始图形和问题文本，通过监督适应学习目标形式语言，并通过求解器的可解性引导反馈进一步优化。这使得可执行性（而非表面文本相似度）成为核心训练信号。其次，求解器驱动的定理提出旨在解决求解器侧的僵局。神经代理不是允许添加未检查的公理，而是从当前证明状态中提出有界的辅助引理或定理实例，每个被接受的提议必须通过符号验证才能驱动推导。

在 Geometry3K（Lu 等, 2021 (https://arxiv.org/html/2606.27926#bib.bib1)）和 PGPS9K（Zhang 等, 2023 (https://arxiv.org/html/2606.27926#bib.bib3)）上的实验评估显示，相对于多模态大语言模型、神经和神经符号基线，SD-GPS 取得了一致的改进。如图 1 (https://arxiv.org/html/2606.27926#S1.F1) 总结所示，SD-GPS 在两个基准测试中的完成准确率均超过了先前最强的系统。结果表明，多模态感知与符号执行之间的闭环能够同时改善求解器就绪的形式化和最终的几何推理。

综上所述，我们的贡献主要有三个方面：

- **求解器驱动的自动形式化**：我们将监督式形式语言适应与可解性引导的强化学习统一到一个自动形式化模块中，该模块从原始图形-文本输入中产生求解器可执行的谓词。
- **可验证的定理提出**：我们引入了一个僵局感知的定理提出代理，可从求解器状态中提出辅助引理，同时仅接受经符号后端验证的提议来保持正确性。
- **系统性评估**：我们在标准的完成和选择设置、跨模态点引用场景以及OCR导致的失败模式下进行评估，在 Geometry3K 和 PGPS9K 上展示了稳健的提升。

## 2 相关工作

**几何问题求解。** GPS 领域已从经典的基于规则引擎演变为现代的神经符号混合体。早期的符号方法，如 Wu 方法（Wu, 1978 (https://arxiv.org/html/2606.27926#bib.bib50)）和 Gröbner 基（Buchberger, 1976 (https://arxiv.org/html/2606.27926#bib.bib36)），奠定了数学严谨性的基础，但根本受限于它们无法解释非正式的多模态输入。为弥合这一差距，现代框架（Wu 等, 2024 (https://arxiv.org/html/2606.27926#bib.bib2); Peng 等, 2023 (https://arxiv.org/html/2606.27926#bib.bib5)），如 Inter-GPS（Lu 等, 2021 (https://arxiv.org/html/2606.27926#bib.bib1)）和 UniGeo（Cheng 等, 2025 (https://arxiv.org/html/2606.27926#bib.bib37)），将深度学习解析器与符号求解器集成。然而，这些系统主要依赖解耦范式，其中文本和图形由独立的神经模块处理。最近的进展，特别是 Pi-GPS（Zhao 等, 2025 (https://arxiv.org/html/2606.27926#bib.bib9)）和 AutoGPS（Ping 等, 2026 (https://arxiv.org/html/2606.27926#bib.bib10)），试图通过引入专门的事后纠正阶段或图形式启发法来解决这种隔离，以消除指代歧义。尽管做出了这些努力，此类系统仍然受限于初始独立解析结果的质量。这种结构分离常常导致级联信息损失，因为形式化过程缺乏统一的表示来解决模态间的依赖关系，特别是在面对文本或图形中未明确定义的复杂空间关系时。

**多模态自动形式化。** 自动形式化桥接了非正式的人类直觉与机器可验证逻辑之间的差距（Wu 等, 2022b (https://arxiv.org/html/2606.27926#bib.bib45)）。在几何中，这项任务尤为艰巨，因为语言描述在没有视觉基础的情况下常常在逻辑上是不明确的。MATP-BENCH（He 等, 2025 (https://arxiv.org/html/2606.27926#bib.bib21)）强调了该领域的重要性，指出形式化验证的多模态数学仍是前沿多模态大语言模型面临的重大挑战。最近的框架，如 AutoGPS（Ping 等, 2026 (https://arxiv.org/html/2606.27926#bib.bib10)）和 Pi-GPS（Zhao 等, 2025 (https://arxiv.org/html/2606.27926#bib.bib9)），试图通过将图形翻译成谓词来解决这个问题。然而，它们主要依赖解耦范式，使用专门的、非Transformer的解析器如PGDP（Hao 等, 2022 (https://arxiv.org/html/2606.27926#bib.bib4)），需要事后启发式方法来解决模态间的不一致性。类似地，DFE-GPS（Zhang 等, 2024c (https://arxiv.org/html/2606.27926#bib.bib44)）仅将图形形式化视为辅助信号而非主要目标。虽然最近的 MMFORMALIZER（Xiong 等, 2026 (https://arxiv.org/html/2606.27926#bib.bib26)）通过递归基础和 PhysLean 中的规则搜索将自动形式化扩展到物理领域，但它侧重于高级公理演绎。相比之下，我们的框架在统一的LMM表示中实现了联合图形-文本对齐。通过在单次推理过程中实现双向消歧，我们直接从原始像素中解决低级拓扑歧义，为可验证的多模态推理提供了更集成和可扩展的路径。

**可验证强化学习。** 强化学习也在几何推理中得到了探索，例如 GeoDRL 将演绎推理表述为在几何逻辑图上的序列决策（Peng 等, 2023 (https://arxiv.org/html/2606.27926#bib.bib5)）。最近，LLM 推理转向了*可验证*奖励（DeepSeek-AI, 2025 (https://arxiv.org/html/2606.27926#bib.bib51)），其中正确性可以从数学或代码输出中自动计算，而不是依赖人工偏好标签。DeepSeekMath 通过 GRPO（Shao 等, 2024 (https://arxiv.org/html/2606.27926#bib.bib23)）在数学推理中普及了这一范式，而 GSPO 后来通过序列级策略优化改进了训练稳定性和效率（Zheng 等, 2025 (https://arxiv.org/html/2606.27926#bib.bib24)）。相比之下，我们的工作将优化锚定在形式表示的求解器就绪性上。我们将 GSPO 适应到多模态自动形式化，奖励基于解析有效性、可执行求解器状态以及答案级可解性。当黄金形式标注可用时，我们将其用于监督适应和分析；强化学习阶段本身可以由解析器和求解器执行反馈驱动，使目标更接近下游符号任务。

## 3 方法

### 3.1 框架概述

给定一个由图形 \(I\)、文本问题 \(T\) 和目标答案 \(a^*\) 组成的几何问题，SD-GPS 旨在生成一个可由符号求解器 \(\mathcal{S}\) 消费的形式表示 \(\hat{\Lambda}\)。该系统围绕两个求解器耦合的循环组织。第一个循环学习多模态形式化器 \(F_\theta\)：

\[
\hat{\Lambda} = F_\theta(I, T),
\]
(1)

其中 \(\hat{\Lambda}\) 包含基于图形和文本的正式谓词。第二个循环通过一个定理提出代理来增强符号演绎。当 \(\mathcal{S}(\hat{\Lambda})\) 无法推导出目标答案时，代理观察中间证明状态并提出一个定理假设 \(\hat{\tau}\)，随后求解器验证 \(\hat{\tau}\) 是否适用且对继续证明有用。这种设计确保所有被接受的形式化和定理提议都基于符号执行。

图 2 (https://arxiv.org/html/2606.27926#S3.F2) 展示了 SD-GPS 的整体工作流程，包括多模态形式化、求解器反馈、修复和定理提出。

请参阅图注

图 2：所提出的 SD-GPS 框架概览。原始图形-文本输入被转换为求解器可执行的正式谓词，由符号求解器检查，必要时通过求解器引导的修复进行优化，并在求解器遇到演绎僵局时通过验证的辅助定理提议进行增强。

### 3.2 形式化数据：精选与合成来源

为了使形式化器能够接触真实的教科书措辞、多样化的图形样式和标注噪声，我们构建了一个混合形式化语料库，包含精选的真实世界示例和可控的合成实例。真实世界部分由 Geometry3K-Train、PGPS9K 的训练分割和 PGDP 训练集构建而成。由于这些数据集在标注约定上有所不同，且最初并非设计为统一严格的形式语言基准，我们对符号表达式、实体名称和图形-文本基础格式进行了规范化。Geometry3K 的标注经过校对和标准化，以减少不一致的谓词使用和模糊的实体引用。对于 PGPS9K，图形侧的形式语言被转换为 Inter-GPS 格式，在预处理过程中进行消歧，然后通过解析器和求解器执行进行过滤。转换后的谓词若无法解析、实体基础或求解器验证，则被移除。

合成部分由几何模板生成，这些模板指定了图形构建程序、谓词级形式化和目标查询。模板参数控制点的布局、标签可见性、辅助标记、代数值和歧义类型。我们使用求解器拒绝不一致的构造，仅保留谓词可执行且目标答案被唯一确定的示例。这为形式化器提供了在真实数据中代表性不足的情形（例如省略标签、图形提供的点、密集的角度标记和视觉上相似的点名）的额外监督。

最终的训练数据以元组 \((I, T, \Lambda^*, a^*, m)\) 形式存在，其中 \(I\) 表示图形，\(T\) 表示问题文本，\(\Lambda^*\) 表示目标形式表示，\(a^*\) 表示黄金答案，\(m\) 存储关于实体基础、歧义类型、标注来源和求解器状态的元数据。