核心发现
方法论
该方法融合监督学习与强化学习，基于QwenVL3-2B模型实现多模态自动形式化，利用符号求解器作为执行神谕。引理提议模块通过符号验证筛选，解决推理中的死胡同问题。系统在Geometry3K和PGPS9K数据集上表现优异，超越现有神经符号和深度学习模型。
关键结果
- 在Geometry3K上，SD-GPS达到86.4%的完成率和90.4%的选择题准确率，超越最优基线3.5和3.2个百分点。
- 在PGPS9K上，分别取得79.8%和84.5%的成绩，优于现有方法4.4和3.0个百分点。
- 引理提议结合符号验证，有效缓解推理死胡同，显著提升推理成功率和可解释性。
研究意义
该研究突破了几何问题自动推理的瓶颈，将神经感知与符号推理紧密结合，为可验证的几何推理提供新思路。其创新的自动形式化与引理提议机制，为未来符号AI在复杂推理任务中的应用奠定基础，推动AI向更高的可解释性和可靠性迈进。
技术贡献
提出以求解器为执行神谕的框架，融合监督与强化学习，提升形式化的可执行性。引入死胡同感知引理提议器，确保符号验证的严谨性。系统在多模态输入下实现端到端训练，显著优于传统解码或单一模型，提供理论保证和工程创新。
新颖性
首次将求解器作为连续的执行神谕，贯穿自动形式化与推理过程。引理提议模块结合符号验证，解决固定规则库的限制，推动神经符号系统的动态扩展，体现出在符号推理中的新颖应用。
局限性
- 依赖高质量的符号求解器，复杂问题中仍可能受限于规则库和搜索空间。
- 模型训练成本较高，需大量标注和符号验证数据。
- 对极端复杂或模糊问题的泛化能力仍需提升。
未来方向
未来将结合更强大的符号引擎，优化引理提议策略，增强模型的泛化能力。此外，将探索多模态输入的自适应融合机制，提升在实际场景中的应用鲁棒性，推动符号AI向更广泛的推理任务扩展。
AI 总览摘要
几何问题的自动推理一直是人工智能中的难题。传统方法依赖规则库，难以应对复杂或模糊场景。近年来，神经符号融合成为研究热点，但多模态输入的自动形式化和推理死胡同问题仍未根本解决。
本文提出SD-GPS框架，创新性地将符号求解器作为连续的执行神谕，贯穿自动形式化与推理全过程。核心在于基于QwenVL3-2B模型的多模态自动形式化，将原始图像和文本联合转化为可执行的符号表达，同时利用求解器反馈优化模型。引理提议模块通过符号验证筛选，动态生成辅助引理，有效缓解推理死胡同，提升推理成功率。
在Geometry3K和PGPS9K两个公开数据集上，SD-GPS显著优于现有神经符号和深度学习方法，完成率分别达到86.4%和79.8%，超越最优基线3-4个百分点。这表明闭环式的多模态感知与符号执行结合，极大改善了几何推理的准确性和可解释性。
该研究不仅推动了符号AI的理论发展，也为实际应用提供了可行路径。未来，将结合更强的符号引擎和自适应多模态融合技术，进一步提升系统的鲁棒性和泛化能力，推动AI在复杂推理任务中的广泛应用。
深度分析
研究背景
几何推理作为数学教育和科学研究的重要组成部分，经历了从符号演算到深度学习的演变。早期符号方法如Wu’s Method和Groebner基底，强调数学严谨性，但难以处理模态多样的非结构化输入。近年来，神经符号融合系统如Inter-GPS、AutoGPS等，试图结合深度学习的感知能力与符号推理的严密性，但多依赖于独立模块，信息传递不畅，限制了复杂空间关系的理解。多模态自动形式化成为突破口，但受制于符号表达的准确性和一致性问题，仍面临推理死胡同和规则库限制。符号验证的引入为提升推理可靠性提供了新思路，但如何实现端到端的联合优化仍是挑战。
核心问题
核心问题在于多模态输入的自动形式化与符号推理的紧密结合。现有系统多采用分离式架构，导致信息丢失和推理死胡同。自动形式化的目标是将图像和文本转化为符号表达，但受限于模型的表达能力和规则库的刚性，难以应对复杂空间关系。引理提议和符号验证的结合虽能缓解死胡同，但缺乏动态适应能力，难以应对多样化问题场景。如何实现端到端、可扩展且高效的多模态自动形式化，成为亟待解决的难题。
核心创新
本研究的创新点包括：1）提出以求解器为执行神谕的端到端多模态自动形式化框架，打破传统的模块化限制；2）引入死胡同感知的引理提议器，结合符号验证筛选，动态生成辅助引理，增强推理的灵活性；3）融合监督学习与强化学习，优化形式化质量和推理效率。该方法不同于以往仅依赖静态规则或单一模型的方案，强调符号验证的严谨性和模型的适应性，为神经符号系统的动态扩展提供了新路径。
方法详解
- �� 输入：原始几何图像和文本描述。
- �� 多模态联合编码：利用QwenVL3-2B模型，将图像和文本联合编码为符号表达。
- �� 监督训练：在标注数据上优化模型，使其输出符合目标符号语言。
- �� 强化优化：通过求解器反馈，奖励可执行、符号验证通过的形式化结果。
- �� 引理提议：在推理死胡同时，利用符号状态提议局部引理，经过验证后加入推理链。
- �� 端到端训练：结合监督和强化信号，优化模型参数，实现多模态到符号的无缝转换。
实验设计
采用Geometry3K和PGPS9K两个公开数据集，比较多种基线模型，包括纯深度学习、神经符号和符号方法。评估指标包括完成率和选择题准确率。通过消融实验验证引理提议、符号验证和强化学习的贡献。参数设置包括QwenVL3-2B模型、不同的奖励权重和搜索策略，确保模型在多场景下的鲁棒性。
结果分析
SD-GPS在Geometry3K上达86.4%的完成率和90.4%的选择题准确率，优于AutoGPS、PGPSNet等方法3-4个百分点。在PGPS9K上，分别达到79.8%和84.5%，超越最优基线。引理提议和符号验证显著提升推理成功率，验证了闭环机制的有效性。消融实验显示强化学习和修复策略对性能提升至关重要。
应用场景
该方法适用于自动化几何推理、数学教育、科学研究等场景，能自动理解复杂空间关系，提供可验证的推理过程。未来还可扩展到物理、化学等多模态科学推理任务，推动AI在科学探索中的应用。
局限与展望
目前模型依赖高质量符号求解器，复杂或模糊问题仍存在推理死胡同。训练成本高，需大量标注数据和符号验证。对极端复杂场景的泛化能力有限，未来需优化模型结构和推理策略。
通俗解读 非专业人士也能看懂
想象你在一家工厂工作，工厂里有很多不同的机器和流程。每个机器都需要按照一定的步骤操作，才能完成一件产品。以前，工厂只用一套固定的操作手册，遇到新问题就很难解决。现在，这个新系统像是给工厂配备了一个聪明的助手，它能看懂工厂里的各种机器和流程，知道怎么用最合适的方法解决问题。这个助手不仅能理解工厂里的图片和说明，还能自己提出新的解决方案，确保每一步都符合工厂的规则。这样，工厂的生产效率大大提高，问题也能更快解决。这个系统就像让工厂变得更聪明、更可靠的一双“慧眼”。
简单解释 像给14岁少年讲一样
想象你在学校里参加一个科学比赛，题目是用纸和尺子画出各种几何图形。以前，你需要自己想办法画出正确的形状，有时候会画错，还得反复检查。现在，有个聪明的机器人助手，它能看懂你的描述和图片，帮你把图形变成可以用计算机理解的符号。它还能自己提出一些小建议，比如“试试用这个角度”或者“加个辅助线”，帮助你更快完成任务。这个机器人还会检查每一步，确保没有错误，最后帮你得到正确的答案。就像有个聪明的朋友一直在你身边，帮你解决难题，让你更快更准地完成比赛。
原文摘要
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.