A Neuro-Symbolic Approach for Reliable Proof Generation with LLMs: A Case Study in Euclidean Geometry

TL;DR

This paper introduces a neuro-symbolic method combining LLMs with structured verification to enhance proof accuracy in geometric problems, significantly improving reliability and correctness.

Contribution

It presents a novel neuro-symbolic framework that retrieves similar problems and uses formal verification to guide LLMs in generating accurate proofs.

Findings

Proof accuracy improved by 58%-70% with the method

Both problem retrieval and verifier feedback contribute to performance gains

Method enhances LLM reliability for formal reasoning tasks

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 that combines LLMs' generative strengths with structured components to overcome this challenge. 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. We demonstrate that our method significantly improves proof accuracy for OpenAI's o1 model (58%-70% improvement); both analogous problems and the verifier's feedback contribute to these gains. 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.