# Reliable Proof Generation with LLMs via Analogical Retrieval and Symbolic Verification: A Case Study in Euclidean Geometry

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

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 24 of its 46 references that are in the map.
- First posted on arXiv 20 May 2025.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

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

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [MathVerse: Does Your Multi-modal LLM Truly See the Diagrams in Visual Math Problems?](https://mlsanity.com/paper/2403.14624/) (2024)
- [MAmmoTH: Building Math Generalist Models through Hybrid Instruction Tuning](https://mlsanity.com/paper/2309.05653/) (2023)
- [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://mlsanity.com/paper/2012.13048/) (2020)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [Large Language Models as Analogical Reasoners](https://mlsanity.com/paper/2310.01714/) (2023)
- [Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2](https://mlsanity.com/paper/2502.03544/) (2025)
- [NaturalProver: Grounded Mathematical Proof Generation with Language Models](https://mlsanity.com/paper/2205.12910/) (2022)
- [LAMBADA: Backward Chaining for Automated Reasoning in Natural Language](https://mlsanity.com/paper/2212.13894/) (2022)
- [FormalGeo: An Extensible Formalized Framework for Olympiad Geometric Problem Solving](https://mlsanity.com/paper/2310.18021/) (2023)
- [Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification](https://mlsanity.com/paper/2412.14063/) (2024)
- [PerfCodeGen: Improving Performance of LLM Generated Code with Execution Feedback](https://mlsanity.com/paper/2412.03578/) (2024)
- [Beyond Final Answers: Evaluating Large Language Models for Math Tutoring](https://mlsanity.com/paper/2503.16460/) (2025)
- [LEMMA: Learning from Errors for MatheMatical Advancement in LLMs](https://mlsanity.com/paper/2503.17439/) (2025)
- [Exposing the Achilles' Heel: Evaluating LLMs Ability to Handle Mistakes in Mathematical Reasoning](https://mlsanity.com/paper/2406.10834/) (2024)
- [MCP-Solver: Integrating Language Models with Constraint Programming Systems](https://mlsanity.com/paper/2501.00539/) (2024)
- [ParallelPARC: A Scalable Pipeline for Generating Natural-Language Analogies](https://mlsanity.com/paper/2403.01139/) (2024)
- [Combining Constraint Programming Reasoning with Large Language Model Predictions](https://mlsanity.com/paper/2407.13490/) (2024)
- [Lemmanaid: Neuro-Symbolic Lemma Conjecturing](https://mlsanity.com/paper/2504.04942/) (2025)
- [Using a Feedback Loop for LLM-based Infrastructure as Code Generation](https://mlsanity.com/paper/2411.19043/) (2024)
- [Can LLMs plan paths with extra hints from solvers?](https://mlsanity.com/paper/2410.05045/) (2024)

## Built on by (most cited first, 7 of 7)

- [Geometrically-Constrained Agent for Spatial Reasoning](https://mlsanity.com/paper/2511.22659/) (2025)
- [Unlocking LLM Creativity in Science through Analogical Reasoning](https://mlsanity.com/paper/2605.11258/) (2026)
- [LLMs versus the Halting Problem: Characterizing Program Termination Reasoning](https://mlsanity.com/paper/2601.18987/) (2026)
- [LLMs with in-context learning for Algorithmic Theoretical Physics](https://mlsanity.com/paper/2605.08212/) (2026)
- [Generative Logic: A New Computer Architecture for Deterministic Reasoning and Knowledge Generation](https://mlsanity.com/paper/2508.00017/) (2025)
- [SymDiag: Explainable Diagnosis for LLM Reasoning via Neuro-Symbolic Verification](https://mlsanity.com/paper/2608.08786/) (2026)
- [Diagnosing Sampled LLM Reasoning in Formal Geometry: Coverage, Realization, and Validity Evidence](https://mlsanity.com/paper/2609.32924/) (2026)

## Abstract (arXiv)

Large language models (LLMs) struggle with formal domains that require rigorous logical deduction and symbolic reasoning, such as mathematical proof generation. We propose a neuro-symbolic approach centered on the hypothesis that structurally analogous problems often admit similar proofs. As a proof-of-concept, we focus on SAT-level geometry problems. Our approach is two-fold: (1) We retrieve analogous problems and use their proofs to guide the LLM, and (2) a formal verifier evaluates the generated proofs and provides feedback, helping the model fix incorrect proofs. Our complete pipeline substantially improves proof accuracy across model families, achieving 68%-96% accuracy compared with 10%-44% for LLM-only baselines that use neither analogy retrieval nor verifier feedback. When comparing against models with the same verifier feedback and inference budget, analogical guidance improves accuracy from 88% to 96% for GPT-5, 78% to 86% for Claude Sonnet 4.6, 72% to 86% for Gemini-Flash-2.5, and 52% to 80% for OpenAI o1. More broadly, shifting to LLMs that generate provably correct conclusions has the potential to dramatically improve their reliability, accuracy and consistency, unlocking complex tasks and critical real-world applications that require trustworthiness.