Verifiable Geometry Problem Solving: Solver-Driven Autoformalization and Theorem Proposing
arXiv:2606.27926v1 [cs.AI] 26 Jun 2026
Can Li
Ting Zhang Junbo Zhao Hua Huang Beijing Normal University
Abstract 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.
1
Introduction
Geometry Problem Solving (GPS) aims to derive mathematical solutions from a textual problem description and its corresponding diagram [Chen et al., 2022, Gelernter et al., 1960, Sachan and Xing, 2017, Wu, 1986, Wu et al., 2024, Peng et al., 2023]. To tackle the inherent complexity of geometry, many recent systems adopt the neuro-symbolic paradigm [Trinh et al., 2024, Chervonyi et al., 2025]. This dual-process approach utilizes neural networks as a "perceptual front-end" and symbolic engines as a "logical back-end" [Wu et al., 2022a]. Within this framework, the reasoning pipeline is driven by two core modules: (i) Autoformalization, which translates multimodal raw inputs into executable formal representations, and (ii) Theorem Prediction, which selects or proposes theorem instances that can be used by the solver to derive solutions. This modular architecture allows systems to leverage the intuitive recognition of deep learning alongside the deterministic rigor of formal logic. In the autoformalization stage, the objective is to transform multimodal inputs into solver-ready predicates. However, existing GPS frameworks typically adopt a “decoupled-and-rectified” paradigm [Lu et al., 2021, Zhao et al., 2025, Ping et al., 2026], in which isolated neural modules independently parse diagrams and formalize text, followed by a post-hoc rectification step to resolve referential ambiguities [Zhao et al., 2025, Ping et al., 2026]. Beyond this structural fragility, a more fundamental limitation lies in objective misalignment. Current approaches treat formalization as a static, one-way semantic translation task, optimizing against expensive human-annotated logical forms that emphasize linguistic fidelity rather than computational solvability. As a result, the formalization process is Preprint.
not aligned with the ultimate goal of solver-based problem solving, and high semantic accuracy does not necessarily translate into effective or executable representations for downstream reasoning. Even when provided with accurate formalization, the theorem prediction stage faces a second critical bottleneck: a fixed theorem library and finite search budget can leave the solver at a deductive impasse. State-of-the-art GPS frameworks [Ping et al., 2026, Zhang et al., 2024a] usually operate with a pre-defined library of geometric rules, so they may fail when a problem requires a rarely selected theorem instance, a small auxiliary construction, or an intermediate relation such as cyclicity, similarity, or proportionality. We therefore treat theorem proposing as a bounded, verifier-controlled proposal problem rather than as free-form axiom generation: a neural agent may suggest local auxiliary lemmas from the current proof state, but only the symbolic back-end can accept, reject, and use them.