用自纠错机制提升大模型证明正确性，让机器证明更可信。
ProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correction
- 结合符号验证与强化学习，让模型自我修正逻辑错误
- 在miniF2F等数据集上证明准确率显著高于以往模型
- 适合形式化验证、AI数学推理研究者使用
我们提出ProofNet++，一种神经符号框架，通过将大语言模型（LLMs）与形式化证明验证及自纠错机制结合，提升自动定理证明能力。现有基于LLM的系统存在幻觉逻辑步骤和不可验证推理的问题。ProofNet++通过引入符号证明树监督、以验证器为奖励函数的强化学习循环，以及迭代自纠错模块，缓解这些缺陷。在miniF2F、Lean的mathlib和HOL Light上的实验表明，ProofNet++在证明准确率、正确性和形式可验证性方面均显著优于先前模型。我们还对验证器引导的强化学习框架的收敛性与稳定性进行了理论分析，并公开了数据集和代码库以促进后续研究。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。