Enhancing Neural Theorem Proving via High-Quality Proof Selection and Verifier Feedback

Motivation

• Known: LLM을 활용한 neural theorem proving은 Lean 4와 Isabelle 같은 interactive theorem prover에서 proof-step generation과 whole-proof generation 방식으로 발전해왔으며, 일반 NLP 영역에서는 data-centric 접근이 대규모 raw corpus보다 소규모 curated dataset으로 더 나은 성능을 낼 수 있음이 입증되었다(MoDS, self-guided data selection 등).
• Gap: 기존 Isabelle NTP 연구는 검색 전략 최적화나 불균형한 raw proof corpus에 대한 supervised training에 의존하며, 일반 목적 data selection 방법은 Isabelle proof의 특수한 구조적·논리적 의존성을 반영하지 못해 그대로 적용하기 어렵다는 한계가 있다.
• Why: seL4, 검증된 컴파일러 등 실제 소프트웨어/하드웨어 검증에 널리 쓰이는 성숙한 정리 증명기인 Isabelle에서 LLM 기반 증명 자동화 성능을 향상시키는 것은 formal verification의 실용적 확장성에 직접적으로 기여하는 중요한 문제이다.
• Approach: 약 200,000개의 theorem-proof pair로 구성된 raw corpus에서 PSR(Proof complexity, Semantic coverage, Reasoning diversity) 기준으로 4k개의 고품질 데이터를 선별해 파인튜닝하고, 추론 시 Isabelle verifier의 피드백을 반복적으로 프롬프트에 반영하는 Dynamic Feedback-Based Prompt Optimization을 결합한다.

Achievement

Figure 4. Pass@k performance on miniF2F-test for models fine-

1. PSR 기반 고품질 데이터셋 구축: raw corpus에서 PSR 기준으로 선별한 4k 규모의 Isabelle 학습 데이터셋을 구축하고 공개했다.
2. 데이터만으로 큰 성능 향상: PSR-selected 데이터만으로 파인튜닝했을 때 miniF2F-test에서 84.8% Pass@64를 달성했다.
3. State-of-the-art 달성: Dynamic Feedback-Based Prompt Optimization을 결합한 전체 프레임워크는 90.6% Pass@64를 기록하며 기존 ProofAug 등을 능가하는 Isabelle NTP 최고 성능을 달성했다.
4. 재현 가능 자원 공개: PSR-selected 데이터셋과 fine-tuned LoRA adapter를 공개하여 후속 연구를 지원한다.

How

Figure 2. Template for Dynamic Feedback-Based Prompt Optimization (round r). The prompt is composed of the problem state

• Raw corpus(약 200k개 theorem-proof pair)에 대한 경험적 분석을 통해 supervised fine-tuning 효과를 제한하는 세 가지 데이터 이슈를 식별
• Proof complexity(명확한 구조와 적정 난이도), Semantic coverage(정리 영역과 문제 유형에 대한 넓은 커버리지), Reasoning diversity(다양한 증명 전략과 추론 패턴) 세 차원을 PSR 기준으로 통합
• PSR 점수를 기반으로 raw corpus를 스코어링하여 compact하고 고품질인 학습 subset(4k)을 구성하는 High-Quality Data Selection pipeline 설계
• 훈련된 모델을 추론 시 Isabelle verifier로부터 받은 피드백을 데이터 신호로 활용해 라운드마다 프롬프트를 반복적으로 갱신하는 Dynamic Feedback-Based Prompt Optimization 도입 (검증 성공 시 종료, 실패 시 피드백을 반영해 재생성)
• miniF2F-test에서 Pass@k 지표로 PSR 데이터 단독 파인튜닝과 verifier feedback 결합 프레임워크의 성능을 종합 평가

Originality

• 일반 NLP data selection 기법을 formal theorem proving 도메인, 특히 Isabelle의 구조적·논리적 특성에 맞게 재설계한 PSR 기준을 새롭게 제안
• 학습 단계의 데이터 선별과 추론 단계의 verifier feedback을 하나의 data-centric 프레임워크로 통합하여 training-time과 inference-time 모두에서 데이터 신호를 활용
• Isabelle이라는 상대적으로 연구가 덜 이루어진 declarative ITP에 특화된 접근으로, Lean 4 중심의 기존 NTP 연구와 차별화

Limitation & Further Study

• PSR 기준의 세 차원(complexity, coverage, diversity)을 정량화하는 구체적 스코어링 방법과 하이퍼파라미터 민감도에 대한 상세 분석이 발췌 내용만으로는 충분히 드러나지 않음
• 4k 규모 데이터셋이 Isabelle/HOL과 AFP raw corpus 특성에 맞춰졌기 때문에 다른 ITP(Lean, Coq 등)로의 일반화 가능성에 대한 검증이 필요
• Dynamic Feedback-Based Prompt Optimization의 반복 횟수 증가에 따른 계산 비용과 실제 배포 시의 효율성 트레이드오프에 대한 논의가 추가로 필요
• 후속 연구로 PSR 기준을 다른 ITP나 더 큰 규모의 corpus에 확장 적용하는 연구가 유망함

Evaluation

총평: 데이터 품질과 verifier feedback을 결합한 data-centric 접근으로 Isabelle NTP에서 뚜렷한 성능 향상과 새로운 state-of-the-art를 달성했다는 점에서 실용적 가치가 크며, 공개된 데이터셋과 어댑터는 후속 연구에 유용한 자원이 될 것으로 보인다.