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

TL;DR

ProofNet++ is a neuro-symbolic system that combines large language models with formal proof verification and self-correction to improve automated theorem proving accuracy and reliability.

Contribution

It introduces a novel neuro-symbolic framework with verifier-guided reinforcement learning and self-correction, advancing the state-of-the-art in formal proof verification.

Findings

Significantly improves proof accuracy and correctness

Enhances formal verifiability over prior models

Demonstrates stability and convergence of the RL framework

Abstract

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.