aclanthology.orgSource publication:
Loading content…
When a general-purpose model writes a geometry proof, it first retrieves structurally similar solved problems as examples, and a symbolic verifier then points out errors round by round. On 50 SAT-level Euclidean geometry problems from FormalGeo-7k, the full pipeline reaches 68%–96% proof accuracy, against 10%–44% for baselines that use neither analogical retrieval nor verifier feedback. Under the same verifier feedback and inference budget, analogical guidance alone lifts GPT-5 from 88% to 96% and o1 from 52% to 80%.
A general-purpose model can write a new proof by drawing on structurally similar solved problems and their complete proofs, instead of searching theorems on its own. Earlier practice let the model generate a proof directly, with no formal guarantee of correctness; here analogical retrieval and a symbolic verifier are both wired into generation. On 50 problems sampled from FormalGeo-7k, the complete pipeline reaches 68%–96% accuracy, against 10%–44% for baselines using neither analogical retrieval nor verifier feedback.
Each problem is first rewritten in an abstract form that drops specific names and numbers, and similar solved problems are found from that form. Retrieval uses Jaccard similarity over construction, conditions and goal, and a three-layer neural network regresses the proof similarity of two problems. Among problem pairs with predicted similarity above 0.95, 71% have ground-truth proof similarity in the top two bins, while only 1.28% of all pairs exceed that threshold.
The verifier checks whether the proof itself holds and does not know the answer, so it judges whether the answer follows from the proof. It encodes proof steps and geometric constraints as logical formulas and algebraic expressions, checks consistency with the SMT solver Z3, and reports feedback in three tiers: syntax violation, missing premise, goal not reached. On o1, allowing verifier-guided retries raises the analogy method from 48% to 68% and the baseline from 10% to 38%.
Keeping only the theorems used in similar problems' proofs shrinks the theorem table in the prompt. The full dictionary holds about 196 theorems and averages roughly 18K tokens, so the baseline prompts are longer and need more retries. At k=100, similar problems cover all theorems needed for 96% of target proofs using 26.66 theorems on average, about 13.6% of the full dictionary; o1's average prompt drops from 18K to 2.5K tokens.
The results rest on SAT-level Euclidean geometry problems from FormalGeo-7k, with a main experiment of 50 problems (10 per difficulty level) and a Z3-based symbolic verifier; the authors plan to extend the approach beyond geometry and to explore stronger formal verification and analogy retrieval.
The authors note that the abstraction scheme only replaces entity names and numbers with placeholders and may miss deeper structural relations; Z3 does not support inverse trigonometric functions, so proofs that must derive an angle from a trigonometric value cannot be verified; the model sees no diagrams, and arc-related reasoning can go wrong; whether the results generalize beyond geometry still needs evaluation.