用相似题启发+符号验证，让大模型更可靠地证明几何题。
Reliable Proof Generation with LLMs via Analogical Retrieval and Symbolic Verification: A Case Study in Euclidean Geometry
- 通过找结构相似的题目及其证明来引导大模型推理。
- 结合形式化验证反馈，使证明准确率提升至68%-96%。
- 适合需要高可信度推理的数学、教育或AI安全场景。
大语言模型在需严格逻辑推导的领域（如数学证明生成）表现不佳。本文提出一种神经符号方法，核心假设是结构相似的问题常有相似证明。以SAT级几何题为案例，方法包含两步：（1）检索结构相似问题并利用其证明指导LLM；（2）使用形式化验证器评估生成的证明并提供反馈，帮助修正错误。完整流程显著提升多类模型的证明准确率，达68%-96%，远超仅用LLM的基线（10%-44%）。在相同验证反馈与推理预算下，引入类比引导使GPT-5准确率从88%升至96%，Claude Sonnet 4.6从78%升至86%，Gemini-Flash-2.5从72%升至86%，OpenAI o1从52%升至80%。转向能生成可验证结论的LLM，有望大幅提升其可靠性、准确性和一致性，推动复杂任务及高可信应用落地。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。