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

• URL: http://arxiv.org/abs/2606.27926v1
• Date: Fri, 26 Jun 2026 10:20:09 GMT
• Title: Verifiable Geometry Problem Solving: Solver-Driven Autoformalization and Theorem Proposing
• Abstract summary: We propose SD-GPS, a solver-driven framework that treats the symbolic solver as an execution oracle throughout both formalization and deduction.<n>We show that SD-GPS consistently outperforms existing MLLM, neural, and neuro-symbolic methods across standard completion, multiple-choice, and cross-modal reference regimes.
• Score: 27.961458371130018
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• BiNSGPS: Geometry Problem Solving via Bidirectional Neuro-Symbolic Interaction [45.32907555157728]
  BiNSGPS is a framework that establishes Bidirectional Neuro-Symbolic Interaction between a MLLM Adviser and a solver.<n> MLLM Adviser actively incorporates feedback from the symbolic solver to dynamically rectify inconsistent formal representations.
  arXiv  Detail & Related papers  (2026-06-03T09:18:37Z)
• Branched Signature Kernel Solvers for ODEs with rough Single-Trajectory signals [2.94985644773306]
  We develop a branched signature kernel solver for ordinary differential equations driven by a single trajectory.<n>A emphcount-sampling construction turns the single observation into a hierarchical family of $N+1$ nested training paths.<n>A kernel-collocation framework places the ansatz either on the highest-order derivative of the solution or on the solution itself.
  arXiv  Detail & Related papers  (2026-05-25T13:22:07Z)
• Heuristic Classification of Thoughts Prompting (HCoT): Integrating Expert System Heuristics for Structured Reasoning into Large Language Models [9.545957160908115]
  Heuristic- Classification-of-Thoughts prompting schema (HCoT)<n>Heuristic- Classification-of-Thoughts prompting schema (HCoT)<n>Heuristic- Classification-of-Thoughts prompting schema (HCoT)
  arXiv  Detail & Related papers  (2026-04-14T07:24:08Z)
• A Survey of Reasoning in Autonomous Driving Systems: Open Challenges and Emerging Paradigms [49.66022971508878]
  We argue that reasoning should be elevated from a modular component to the system's cognitive core.<n>We derive and systematize seven core reasoning challenges, such as the responsiveness-reasoning trade-off and social-game reasoning.<n>We identify a fundamental and unresolved tension between the high-latency, deliberative nature of LLM-based reasoning and the millisecond-scale, safety-critical demands of vehicle control.
  arXiv  Detail & Related papers  (2026-03-11T07:40:53Z)
• VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning [4.3414302048068745]
  We present a neurosymbolic framework that combines Large Language Models with SMT solvers to produce verification-guided answers.<n>We introduce three key innovations: (1) multi-model consensus via formal semantic equivalence checking, (2) semantic routing that directs different claim types to appropriate verification strategies, and (3) precise logical error localization via Minimal Correction Subsets.<n>With the GPT-OSS-120B model, VERGE demonstrates an average performance uplift of 18.7% at convergence across a set of reasoning benchmarks compared to single-pass approaches.
  arXiv  Detail & Related papers  (2026-01-27T20:59:11Z)
• Matrix Factorization Framework for Community Detection under the Degree-Corrected Block Model [48.989531198582704]
  We show that DCBM inference can be reformulated as a constrained nonnegative matrix factorization problem.<n>Our approach is to any specific network structure and applies to graphs with any structure representable by a DCBM.<n> Experiments on synthetic and real benchmark networks show that our method detects communities comparable to those found by DCBM inference.
  arXiv  Detail & Related papers  (2026-01-09T19:16:29Z)
• AutoGPS: Automated Geometry Problem Solving via Multimodal Formalization and Deductive Reasoning [14.44742282076576]
  AutoGPS is a neuro-symbolic collaborative framework that solves geometry problems with concise, reliable, and human-interpretable reasoning processes.<n>The MPF utilizes neural cross-modal comprehension to translate geometry problems into structured formal language representations.<n>The DSR takes the formalization as input and formulates geometry problem solving as a hypergraph expansion task.
  arXiv  Detail & Related papers  (2025-05-29T12:01:20Z)
• Fuse, Reason and Verify: Geometry Problem Solving with Parsed Clauses from Diagram [78.79651421493058]
  We propose a neural-symbolic model for plane geometry problem solving (PGPS) with three key steps: modal fusion, reasoning process and knowledge verification. For reasoning, we design an explicable solution program to describe the geometric reasoning process, and employ a self-limited decoder to generate solution program autoregressively. We also construct a large-scale geometry problem dataset called PGPS9K, containing fine-grained annotations of textual clauses, solution program and involved knowledge solvers.
  arXiv  Detail & Related papers  (2024-07-10T02:45:22Z)
• Task-Oriented Sensing, Computation, and Communication Integration for Multi-Device Edge AI [108.08079323459822]
  This paper studies a new multi-intelligent edge artificial-latency (AI) system, which jointly exploits the AI model split inference and integrated sensing and communication (ISAC) We measure the inference accuracy by adopting an approximate but tractable metric, namely discriminant gain.
  arXiv  Detail & Related papers  (2022-07-03T06:57:07Z)
• Message Passing Neural PDE Solvers [60.77761603258397]
  We build a neural message passing solver, replacing allally designed components in the graph with backprop-optimized neural function approximators. We show that neural message passing solvers representationally contain some classical methods, such as finite differences, finite volumes, and WENO schemes. We validate our method on various fluid-like flow problems, demonstrating fast, stable, and accurate performance across different domain topologies, equation parameters, discretizations, etc., in 1D and 2D.
  arXiv  Detail & Related papers  (2022-02-07T17:47:46Z)
• Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning [123.06420835072225]
  We construct a new large-scale benchmark, Geometry3K, consisting of 3,002 geometry problems with dense annotation in formal language. We propose a novel geometry solving approach with formal language and symbolic reasoning, called Interpretable Geometry Problem solver (Inter-GPS) Inter-GPS incorporates theorem knowledge as conditional rules and performs symbolic reasoning step by step.
  arXiv  Detail & Related papers  (2021-05-10T07:46:55Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.