Skip to main content
CenXiv.org
此网站处于试运行阶段,支持我们!
我们衷心感谢所有贡献者的支持。
贡献
赞助
cenxiv logo > cs > arXiv:2505.24230

帮助 | 高级搜索

计算机科学 > 人工智能

arXiv:2505.24230 (cs)
[提交于 2025年5月30日 ]

标题: ProofNet++:一种具有自纠正功能的形式化证明验证的神经符号系统

标题: ProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correction

Authors:Murari Ambati
摘要: 我们提出了ProofNet++,这是一种神经符号框架,通过结合大型语言模型(LLMs)与形式化证明验证和自我校正机制来增强自动定理证明。 当前基于LLM的系统存在幻觉逻辑步骤和无法验证推理的问题。 ProofNet++通过集成符号证明树监督、使用验证器作为奖励函数的强化学习循环以及迭代自我校正模块来缓解这些局限性。 我们在miniF2F、Lean的mathlib和HOL Light上的实验表明,ProofNet++显著提高了证明的准确性、正确性和形式可验证性,超过了先前的模型。 我们提供了引导验证器的RL框架的收敛性和稳定性理论分析,并发布了数据集和代码库以供未来研究。
摘要: We propose ProofNet++, a neuro-symbolic framework that enhances automated theorem proving by combining large language models (LLMs) with formal proof verification and self-correction mechanisms. Current LLM-based systems suffer from hallucinated logical steps and unverifiable reasoning. ProofNet++ mitigates these limitations by integrating symbolic proof tree supervision, a reinforcement learning loop using verifiers as reward functions, and an iterative self-correction module. Our experiments on miniF2F, Lean's mathlib, and HOL Light show that ProofNet++ significantly improves proof accuracy, correctness, and formal verifiability over prior models. We provide theoretical analysis of the convergence and stability of the verifier-guided RL framework and release our datasets and codebase for future research.
评论: 6页,2个图
主题: 人工智能 (cs.AI)
引用方式: arXiv:2505.24230 [cs.AI]
  (或者 arXiv:2505.24230v1 [cs.AI] 对于此版本)
  https://doi.org/10.48550/arXiv.2505.24230
通过 DataCite 发表的 arXiv DOI

提交历史

来自: Murari Ambati [查看电子邮件]
[v1] 星期五, 2025 年 5 月 30 日 05:44:34 UTC (79 KB)
全文链接:

获取论文:

    查看标题为《》的 PDF
  • 查看中文 PDF
  • 查看 PDF
  • HTML(实验性)
  • TeX 源代码
  • 其他格式
许可图标 查看许可
当前浏览上下文:
cs.AI
< 上一篇   |   下一篇 >
新的 | 最近的 | 2025-05
切换浏览方式为:
cs

参考文献与引用

  • NASA ADS
  • 谷歌学术搜索
  • 语义学者
a 导出 BibTeX 引用 加载中...

BibTeX 格式的引用

×
数据由提供:

收藏

BibSonomy logo Reddit logo

文献和引用工具

文献资源探索 (什么是资源探索?)
连接的论文 (什么是连接的论文?)
Litmaps (什么是 Litmaps?)
scite 智能引用 (什么是智能引用?)

与本文相关的代码,数据和媒体

alphaXiv (什么是 alphaXiv?)
CatalyzeX 代码查找器 (什么是 CatalyzeX?)
DagsHub (什么是 DagsHub?)
Gotit.pub (什么是 GotitPub?)
Hugging Face (什么是 Huggingface?)
带有代码的论文 (什么是带有代码的论文?)
ScienceCast (什么是 ScienceCast?)

演示

复制 (什么是复制?)
Hugging Face Spaces (什么是 Spaces?)
TXYZ.AI (什么是 TXYZ.AI?)

推荐器和搜索工具

影响之花 (什么是影响之花?)
核心推荐器 (什么是核心?)
IArxiv 推荐器 (什么是 IArxiv?)
  • 作者
  • 地点
  • 机构
  • 主题

arXivLabs:与社区合作伙伴的实验项目

arXivLabs 是一个框架,允许合作伙伴直接在我们的网站上开发和分享新的 arXiv 特性。

与 arXivLabs 合作的个人和组织都接受了我们的价值观,即开放、社区、卓越和用户数据隐私。arXiv 承诺这些价值观,并且只与遵守这些价值观的合作伙伴合作。

有一个为 arXiv 社区增加价值的项目想法吗? 了解更多关于 arXivLabs 的信息.

这篇论文的哪些作者是支持者? | Disable MathJax (什么是 MathJax?)
  • 关于
  • 帮助
  • contact arXivClick here to contact arXiv 联系
  • 订阅 arXiv 邮件列表点击这里订阅 订阅
  • 版权
  • 隐私政策
  • 网络无障碍帮助
  • arXiv 运营状态
    通过...获取状态通知 email 或者 slack

京ICP备2025123034号