ProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correction
This addresses the problem of unreliable automated theorem proving for formal verification and mathematical reasoning, though it appears incremental as an enhancement to existing neuro-symbolic approaches.
The authors tackled the problem of hallucinated logical steps and unverifiable reasoning in LLM-based automated theorem proving by developing ProofNet++, a neuro-symbolic framework that integrates symbolic proof tree supervision, verifier-guided reinforcement learning, and self-correction. The result was significant improvements in proof accuracy, correctness, and formal verifiability on benchmarks like miniF2F, Lean's mathlib, and HOL Light.
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.