# Verifiable Geometry Problem Solving: Solver-Driven Autoformalization and Theorem Proposing

arXiv: https://arxiv.org/abs/2606.27926 · HTML: https://mlsanity.com/paper/2606.27926/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 18 of its 31 references that are in the map.
- First posted on arXiv 26 Jun 2026.

## Builds on (most cited first, 18 of 18)

- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [InternVL: Scaling up Vision Foundation Models and Aligning for Generic Visual-Linguistic Tasks](https://mlsanity.com/paper/2312.14238/) (2023)
- [InternVL3: Exploring Advanced Training and Test-Time Recipes for Open-Source Multimodal Models](https://mlsanity.com/paper/2504.10479/) (2025)
- [Vision-R1: Incentivizing Reasoning Capability in Multimodal Large Language Models](https://mlsanity.com/paper/2503.06749/) (2025)
- [Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning](https://mlsanity.com/paper/2105.04165/) (2021)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [GeoQA: A Geometric Question Answering Benchmark Towards Multimodal Numerical Reasoning](https://mlsanity.com/paper/2105.14517/) (2021)
- [G-LLaVA: Solving Geometric Problem with Multi-Modal Large Language Model](https://mlsanity.com/paper/2312.11370/) (2023)
- [A Multi-Modal Neural Geometric Solver with Textual Clauses Parsed from Diagram](https://mlsanity.com/paper/2302.11097/) (2023)
- [FormalGeo: An Extensible Formalized Framework for Olympiad Geometric Problem Solving](https://mlsanity.com/paper/2310.18021/) (2023)
- [LANS: A Layout-Aware Neural Solver for Plane Geometry Problem](https://mlsanity.com/paper/2311.16476/) (2023)
- [A Symbolic Character-Aware Model for Solving Geometry Problems](https://mlsanity.com/paper/2308.02823/) (2023)
- [PGDP5K: A Diagram Parsing Dataset for Plane Geometry Problems](https://mlsanity.com/paper/2205.09947/) (2022)
- [AutoGPS: Automated Geometry Problem Solving via Multimodal Formalization and Deductive Reasoning](https://mlsanity.com/paper/2505.23381/) (2025)
- [Fuse, Reason and Verify: Geometry Problem Solving with Parsed Clauses from Diagram](https://mlsanity.com/paper/2407.07327/) (2024)
- [MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?](https://mlsanity.com/paper/2506.06034/) (2025)
- [Diagram Formalization Enhanced Multi-Modal Geometry Problem Solver](https://mlsanity.com/paper/2409.04214/) (2024)
- [Pi-GPS: Enhancing Geometry Problem Solving by Unleashing the Power of Diagrammatic Information](https://mlsanity.com/paper/2503.05543/) (2025)

## Abstract (arXiv)

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.