论文
可验证几何问题求解：求解器驱动的自动形式化与定理提出
Verifiable Geometry Problem Solving: Solver-Driven Autoformalization and Theorem Proposing
摘要
几何问题求解日益采用神经符号范式——组合神经直觉与符号严谨。但当前框架在两个核心阶段 suffer 严重瓶颈：自动形式化把多模态翻译当作与下游求解器兼容性解耦的静态任务——而定理预测中求解器常因固定规则库陷入演绎僵局。为解决——我们提出SD-GPS——求解器驱动框架——在形式化与演绎全程把符号求解器当作执行神谕。第一——求解器驱动自动形式化把监督形式语言适配与可解性引导的强化学习统一进建立在QwenVL3-2B上的单一模块——使可执行性成为核心训练信号。第二——经验证的定理提出引入僵局感知智能体——从当前证明状态提出局部辅助引理——经符号验证过滤全部提案以保证健全性。Geometry3K与PGPS9K上的实证评估表明SD-GPS在标准补全、多选与跨模态参照下持续超越既有MLLM、神经与神经符号方法——证明闭合多模态感知与符号执行间的循环显著改进几何推理——并为神经智能体如何被形式系统锚定以获得可验证问题解决能力提供深刻洞见。
