面向欧几里得几何的神经符号可靠证明生成方法：一个案例研究
人工智能
2026-05-26 v9 计算与语言
摘要
大型语言模型（LLM）在需要严格逻辑推理和符号推理的形式领域（如数学证明生成）方面存在挑战。我们提出了一种神经符号方法，将LLM的生成优势与结构化组件相结合，以克服这一挑战。作为概念验证，我们聚焦于SAT水平的几何问题。我们的方法具有两个方面：(1) 检索类似问题并使用其证明来指导LLM，(2) 形式化验证器评估生成的证明并提供反馈，帮助模型纠正不正确的证明。我们的方法在 diverse 模型家族中显著提高了证明准确率，无论是OpenAI o1、GPT-5、Gemini-Flash-2.5还是Claude Sonnet 4.6，都取得了显著的提升。准确率从基础模型的10%提高到44%，通过我们的方法提高到68%至96%，无论是类似问题指导还是验证器反馈，都对这些改进作出了贡献。更广泛地说，转向能够生成可形式化正确结论的LLM，有望极大提高其可靠性、准确性和一致性，解锁需要可信度的复杂任务和关键实际应用。
引用
@article{arxiv.2505.14479,
title = {A Neuro-Symbolic Approach for Reliable Proof Generation with LLMs: A Case Study in Euclidean Geometry},
author = {Oren Sultan and Eitan Stern and Dafna Shahaf},
journal= {arXiv preprint arXiv:2505.14479},
year = {2026}
}
备注
long paper