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

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.

@article{ambati2025_2505.24230,
  title={ ProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correction },
  author={ Murari Ambati },
  journal={arXiv preprint arXiv:2505.24230},
  year={ 2025 }
}