Verifiable Geometry Problem Solving: Solver-Driven Autoformalization and Theorem Proposing
作者: Can Li, Ting Zhang, Junbo Zhao, Hua Huang
分类: cs.AI, cs.CL, cs.CV
发布日期: 2026-06-26
💡 一句话要点
提出SD-GPS框架以解决几何问题求解中的瓶颈
🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 几何问题求解 神经符号范式 自动形式化 定理预测 强化学习 符号验证 多模态翻译
📋 核心要点
- 现有几何问题求解方法在自动形式化和定理预测阶段面临严重瓶颈，导致推理效率低下。
- 本文提出的SD-GPS框架通过将符号求解器视为执行神谕，优化了形式化和推理过程。
- 实验证明，SD-GPS在Geometry3K和PGPS9K数据集上表现优异，超越了现有的多种方法，提升了几何推理能力。
📝 摘要（中文）
几何问题求解逐渐采用神经符号范式，结合神经直觉与符号严谨性。然而，现有框架在自动形式化和定理预测两个核心阶段存在严重瓶颈。为此，本文提出了SD-GPS框架，将符号求解器视为执行神谕，贯穿形式化和推理过程。首先，Solver-Driven Autoformalization将监督形式语言适应与可解性引导的强化学习统一为一个模块，以可执行性作为核心训练信号。其次，Verified Theorem Proposing引入了一个感知停滞的代理，从当前证明状态中提出局部辅助引理，通过符号验证确保其正确性。实验证明，SD-GPS在多个标准任务上均优于现有方法，显著提升几何推理能力。
🔬 方法详解
问题定义：本文旨在解决现有几何问题求解方法在自动形式化和定理预测阶段的瓶颈，导致推理效率低下和准确性不足。
核心思路：提出SD-GPS框架，将符号求解器视为执行神谕，贯穿形式化和推理过程，优化了多模态翻译与求解器的兼容性。
技术框架：SD-GPS框架包括两个主要模块：Solver-Driven Autoformalization和Verified Theorem Proposing。前者结合监督学习与强化学习，后者通过引入感知停滞的代理进行定理提出。
关键创新：最重要的创新在于将求解器的执行能力作为核心训练信号，并通过符号验证确保提出的引理的正确性，这与现有方法的静态规则库形成鲜明对比。
关键设计：在Solver-Driven Autoformalization中，使用QwenVL3-2B模型进行训练，损失函数设计为以可执行性为中心，确保模型在推理过程中能够有效执行。
🖼️ 关键图片
📊 实验亮点
实验结果显示，SD-GPS在Geometry3K和PGPS9K数据集上均优于现有的多模态大语言模型、神经网络和神经符号方法，特别是在标准完成、选择题和跨模态参考任务中，性能提升幅度显著，证明了其在几何推理中的有效性。
🎯 应用场景
该研究的潜在应用领域包括教育、自动化定理证明、机器人导航等。通过提升几何推理能力，SD-GPS能够为复杂问题的自动求解提供更为可靠的支持，未来可能在智能教育和自动化系统中发挥重要作用。
📄 摘要（原文）
Geometry Problem Solving have increasingly adopt the neuro-symbolic paradigm, combining neural intuition with symbolic rigor. However, current frameworks suffer from severe bottlenecks in two core stages: autoformalization, which treats multimodal translation as a static task decoupled from downstream solver compatibility, and theorem prediction, where solvers frequently hit a deductive impasse due to fixed rule libraries. To address these, we propose SD-GPS, a solver-driven framework that treats the symbolic solver as an execution oracle throughout both formalization and deduction. First, Solver-Driven Autoformalization unifies supervised formal-language adaptation and solvability-guided reinforcement learning into a single module built on QwenVL3-2B, making executability the central training signal. Second, Verified Theorem Proposing introduces an impasse-aware agent that proposes local auxiliary lemmas from current proof states, ensuring soundness by filtering all proposals through symbolic verification. Empirical evaluations on Geometry3K and PGPS9K demonstrate that SD-GPS consistently outperforms existing MLLM, neural, and neuro-symbolic methods across standard completion, multiple-choice, and cross-modal reference regimes, proving that closing the loop between multimodal perception and symbolic execution significantly improves geometric reasoning, offering profound insights into how neural agents can be grounded by formal systems to achieve verifiable problem-solving capabilities.