ProofNet++는 대규모 언어 모델(LLM)과 형식적 증명 검증 및 자기 수정 메커니즘을 결합하여 자동 정리 증명을 향상시키는 신경 기호 프레임워크입니다. 기존의 LLM 기반 시스템은 환각적인 논리적 단계와 검증할 수 없는 추론으로 어려움을 겪습니다. ProofNet++는 기호적 증명 트리 감독, 검증자를 보상 함수로 사용하는 강화 학습 루프, 그리고 반복적인 자기 수정 모듈을 통합하여 이러한 한계를 완화합니다. miniF2F, Lean의 mathlib, HOL Light에 대한 실험 결과, ProofNet++는 이전 모델에 비해 증명 정확도, 정확성 및 형식적 검증 가능성을 크게 향상시키는 것으로 나타났습니다. 본 연구는 검증자로 안내되는 강화 학습 프레임워크의 수렴 및 안정성에 대한 이론적 분석을 제공하며, 향후 연구를 위해 데이터 세트와 코드베이스를 공개합니다.
