计算机科学 > 人工智能
[提交于 2025年5月30日
]
标题: ProofNet++:一种具有自纠正功能的形式化证明验证的神经符号系统
标题: ProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correction
摘要: 我们提出了ProofNet++,这是一种神经符号框架,通过结合大型语言模型(LLMs)与形式化证明验证和自我校正机制来增强自动定理证明。 当前基于LLM的系统存在幻觉逻辑步骤和无法验证推理的问题。 ProofNet++通过集成符号证明树监督、使用验证器作为奖励函数的强化学习循环以及迭代自我校正模块来缓解这些局限性。 我们在miniF2F、Lean的mathlib和HOL Light上的实验表明,ProofNet++显著提高了证明的准确性、正确性和形式可验证性,超过了先前的模型。 我们提供了引导验证器的RL框架的收敛性和稳定性理论分析,并发布了数据集和代码库以供未来研究。
文献和引用工具
与本文相关的代码,数据和媒体
alphaXiv (什么是 alphaXiv?)
CatalyzeX 代码查找器 (什么是 CatalyzeX?)
DagsHub (什么是 DagsHub?)
Gotit.pub (什么是 GotitPub?)
Hugging Face (什么是 Huggingface?)
带有代码的论文 (什么是带有代码的论文?)
ScienceCast (什么是 ScienceCast?)
演示
推荐器和搜索工具
arXivLabs:与社区合作伙伴的实验项目
arXivLabs 是一个框架,允许合作伙伴直接在我们的网站上开发和分享新的 arXiv 特性。
与 arXivLabs 合作的个人和组织都接受了我们的价值观,即开放、社区、卓越和用户数据隐私。arXiv 承诺这些价值观,并且只与遵守这些价值观的合作伙伴合作。
有一个为 arXiv 社区增加价值的项目想法吗? 了解更多关于 arXivLabs 的信息.