Verifiable Geometry Problem Solving: Solver-Driven Autoformalization and Theorem Proposing
06:00 · June 29, 2026 · arXiv cs.AI RSS
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.
Summary
SD-GPS is a neuro-symbolic system for geometry problem solving that treats the symbolic solver as an execution oracle across both formalization and deduction stages. Existing approaches typically separate multimodal parsing from solver compatibility and rely on static theorem libraries, which produces formal representations that are semantically plausible yet often unexecutable and leaves solvers at deductive impasses when required lemmas fall outside the predefined rule set.
The framework replaces this decoupled pipeline with two solver-driven modules. Solver-Driven Autoformalization fine-tunes a QwenVL3-2B multimodal model through supervised language adaptation followed by solvability-guided reinforcement learning, so that executability rather than surface-level textual fidelity becomes the primary training objective. Verified Theorem Proposing adds an impasse-aware agent that generates candidate auxiliary lemmas from the current proof state; every proposal is submitted to the symbolic verifier and is retained only if it preserves soundness and advances the derivation.
Evaluations on the Geometry3K and PGPS9K benchmarks show consistent gains over prior multimodal large language models, purely neural baselines, and earlier neuro-symbolic systems under completion, multiple-choice, and cross-modal reference settings. The results indicate that grounding neural perception directly in solver feedback improves both the quality of formal representations and the reliability of geometric reasoning.
Why it matters
This research is highly relevant for Dutch AI researchers focusing on neuro-symbolic AI and verifiable reasoning, aligning with the EU's emphasis on trustworthy and explainable AI systems. It provides actionable methodologies for integrating multimodal LLMs with symbolic solvers.
