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

Oren Sultan, Eitan Stern, Dafna Shahaf
The Hebrew University of Jerusalem
Paper Code arXiv

A short podcast about the paper

Abstract

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.

Problem Formulation

Website

We demonstrate our ideas in the domain of Euclidean geometry. Our input is a geometry problem, described in both natural language and via a formal representation. The description includes the geometric entities involved (e.g., lines, angles), their relationships (e.g., perpendicular, collinear), and measurements or algebraic expressions over them. We also receive a goal, some quantity to be determined (e.g., the length of a line). In addition, the model has access to a dictionary of theorems that may be used in the proof. The output is a formal proof that derives the goal from the given conditions and theorems, along with the final, numeric answer. The proof consists of steps, each applying a specific theorem from the dictionary.

Approach

Website

Our neuro-symbolic approach. Given a target problem from the FormalGeo-7k dataset, we first convert it into an abstract form by replacing entity names (e.g., lines, angles) and specific numeric values with placeholders. We then retrieve structurally similar problems from the abstracted dataset by computing Jaccard similarity over key formal components: construction (entities and geometric relations), conditions (e.g., angle equalities, segment lengths), and goal (the conclusion to be proven). This is based on the observation that structurally similar problems often share proof patterns. The retrieved problems, along with their corresponding formal proofs, are presented to an LLM as in-context examples, together with the available theorems from the Geometry Theorem Dictionary, to guide proof generation for the target problem. Finally, a symbolic verifier iteratively checks the generated proof and provides feedback until a correct proof is produced or a retry limit is reached.

Results Across Model Families

Model First run, no retries First run, w/ retries Multiple runs, w/ retries
base1,1ours1,1Δ base1,5ours1,5Δ base3,5ours3,5Δ
o110%48%+38%38%68%+30%52%80%+28%
GPT-544%64%+20%80%96%+16%88%96%+8%
Gemini-Flash-2.522%48%+26%58%74%+16%72%86%+14%
Claude Sonnet-4.628%60%+32%58%78%+20%78%86%+8%

Proof accuracy (%) of the base model and our analogy-based method across settings, on 50 FormalGeo-7k problems (10 per difficulty level, 1-5). basei,j denotes the base model (random few-shot examples and the full theorem dictionary) with up to i runs and j verifier-guided retries, while oursi,j denotes our method (retrieved analogies and an analogy-derived theorem dictionary). Δ indicates absolute improvement (percentage points). Our method consistently improves proof accuracy across all models and settings: our complete pipeline (ours3,5) achieves 68%-96% accuracy, compared with 10%-44% for LLM-only baselines (base1,1). Under matched inference budgets with verifier feedback (base3,5 vs. ours3,5), analogical guidance still improves accuracy for every model. At the same time, it substantially reduces the theorem dictionary size (e.g., from ~18K to ~2.5K tokens on average for o1), making the baseline roughly 3× more expensive.

Ablation: Analogy Retrieval and Theorem Dictionary

Setting Examples Dictionary Gemini-2.5-Flash Claude Sonnet 4.6
1 run1 run + retries3 runs + retries 1 run1 run + retries3 runs + retries
OursAnalogiesAnalogy-derived48%74%86%60%78%86%
(i)AnalogiesFull30%68%78%42%62%78%
(ii)RandomRandom-derived24%54%72%28%60%72%
(iii)AnalogiesRandom (size-matched)32%60%78%36%66%74%
BaselineRandomFull22%58%72%28%58%78%

Controlled ablation of analogy retrieval and theorem-dictionary construction on 50 problems using Gemini-2.5-Flash and Claude Sonnet 4.6. Our full method performs best across all inference settings. Settings (i) and (iii), which use retrieved analogies, outperform setting (ii), demonstrating the benefit of analogy retrieval, while our gains over (i) and (iii) demonstrate the additional benefit of analogy-derived theorem selection.

BibTeX

@article{sultan2025reliable,
  title={Reliable Proof Generation with LLMs via Analogical Retrieval and Symbolic Verification: A Case Study in Euclidean Geometry},
  author={Sultan, Oren and Stern, Eitan and Shahaf, Dafna},
  journal={arXiv preprint arXiv:2505.14479},
  year={2025}
}