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

Researchers propose SD-GPS, a solver-driven framework for geometry problem solving that addresses bottlenecks in autoformalization and theorem prediction by treating the symbolic solver as an execution oracle. This approach unifies supervised formal-language adaptation with solvability-guided reinforcement learning to ensure executability during formalization.

• The framework utilizes QwenVL3-2B to unify supervised formal-language adaptation and solvability-guided reinforcement learning into a single module.
• Verified Theorem Proposing introduces an impasse-aware agent that proposes local auxiliary lemmas from current proof states.
• All proposed theorems are filtered through symbolic verification to ensure soundness.
• Empirical evaluations on Geometry3K and PGPS9K show SD-GPS outperforms existing MLLM, neural, and neuro-symbolic methods across standard completion, multiple-choice, and cross-modal reference regimes.

Closing the loop between multimodal perception and symbolic execution significantly improves geometric reasoning, offering insights into how neural agents can be grounded by formal systems to achieve verifiable problem-solving capabilities.