Towards Reliable Proof Generation with LLMs: A Neuro-Symbolic Approach
This addresses the challenge of improving reliability and trustworthiness in LLMs for critical real-world applications requiring formal reasoning, though it is incremental as it builds on existing neuro-symbolic methods.
The paper tackles the problem of LLMs struggling with rigorous logical deduction in formal domains like mathematical proof generation by proposing a neuro-symbolic approach that combines LLMs with structured components, resulting in a 58%-70% improvement in proof accuracy for geometry problems.
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 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 could dramatically improve their reliability, accuracy and consistency, unlocking complex tasks and critical real-world applications that require trustworthiness.