VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving

Motivation

• Known: LLM 기반 formal prover는 tactic을 생성하는 언어모델과 증명 공간을 탐색하는 tree search(MCTS 등)를 결합해 miniF2F 같은 벤치마크에서 solve rate를 지속적으로 끌어올려 왔으며, 대표적으로 Best-of-N sampling이나 handcrafted portfolio 방식이 흔히 사용된다.
• Gap: 기존 파이프라인은 Lean 등 검증기가 제공하는 syntax error, type mismatch, partial goal progress 같은 풍부한 신호를 스칼라 reward나 binary pass/fail로 요약해 버려, 탐색이 검증기가 이미 알려준 정보를 다시 학습해야 하는 비효율이 존재하며, 특히 여러 단계에 걸친 dependent tactic이 필요한 증명에서 이 문제가 두드러진다.
• Why: 검증기의 구조화된 피드백을 생성 결정에 직접 연결하는 것이 단순히 샘플링 규모를 늘리는 것보다 LLM 성능을 더 크게 향상시킬 수 있음을 보여줌으로써, 향후 verifier-in-the-loop 탐색 설계에 일반 원칙을 제시한다.
• Approach: Strategist, Tactician, Critic, Retriever 네 개의 특화된 agent가 공유된 ProofState와 Lean의 4가지 구조화 신호(σA-σD)를 기반으로 협업하며, Phase 1(Best-of-N)이 실패한 정리에 한해 Phase 2(critic-guided MCTS, Phase 1 실패 tactic을 negative example로 주입)를 수행하는 2단계 프로토콜을 사용한다.

Achievement

Figure 2. Main results on miniF2F. (a) Solve rates with 95%

1. miniF2F 성능 향상: VERITAS는 40.6%(99/244)를 달성해 독립적으로 실행한 Best-of-5 Claude(36.9%)와 handcrafted Portfolio(26.2%)를 능가했다.
2. VERITAS-CombiBench 공개 및 검증: 55개의 author-verified Lean 4 조합론 정리로 구성된 신규 벤치마크를 공개했으며, 여기서 VERITAS는 7.3%를 달성해 Best-of-5(1.8%)와 Portfolio(3.6%)를 모두 크게 상회했다.
3. 비유도 샘플링의 한계 노출: CombiBench에서 Best-of-5(1.8%)가 Portfolio(3.6%)보다 낮게 나타나, 올바른 Mathlib lemma 이름을 반복적으로 verifier feedback에서 복구해야 하는 상황에서는 unguided sampling이 오히려 성능을 해친다는 것을 보였다.
4. Phase별 기여도 분석: miniF2F에서 flat-sampling budget으로는 도달할 수 없는 11개 정리를 MCTS만으로 해결 가능함을 phase-wise decomposition으로 규명했다.
5. 검증 비용 절감: batched Lean validation 기법으로 expansion당 검증 비용을 O(K)에서 O(1)로 줄여 약 10배의 verification 비용 절감을 달성했다.

How

Figure 1. VERITAS two-phase protocol. Phase 1: Best-of-N dispatch; failures feed corpus F1. Phase 2: Critic-guided MCTS

• ProofState s = (T, g, H, τ1:t, σA, σB, σC, σD)를 모든 agent가 공유하며 Lean의 syntax validity(σA), type correctness(σB), goal progress(σC), completion(σD) 신호를 명시적으로 전달
• Strategist가 direct/induction/contradiction/cases/rewrite/apply_lemma 6가지 전략과 depth estimate를 선택해 탐색 공간을 축소
• Tactician(Claude Sonnet 4.6, temp 0.8)이 전략, retrieved premise, Critic guidance, 그리고 이전에 실패한 tactic 목록(Lean error message 포함, negative example로 시스템 프롬프트에 주입)을 조건으로 K개의 tactic 후보 생성
• Critic(Claude Haiku 4.5, temp 0.3)이 V(s)∈[0,1] value, 추천 tactic, pruning 권고를 반환하여 MCTS의 random rollout을 대체
• Retriever가 goal token, lemma 이름, 타입 시그니처에 대한 weighted keyword overlap으로 top-5 Mathlib premise 검색
• Critic-guided MCTS의 selection은 UCB에 Critic value와 strategy alignment 항을 추가한 점수로 수행하고, simulation은 V(s) = Vcritic(s) + α1σA + α2σB + α3σC + β/(1+N(s)) 로 구조화 신호를 반영, backpropagation은 binary win/loss 대신 A-B-C-D 신호를 그대로 전파
• Phase 1(Best-of-N)이 실패한 정리에 대해서만 Phase 2(critic-guided MCTS)를 실행하는 2단계 프로토콜로 monotonicity guarantee(S(T) ⊇ S1(T))를 증명
• K개의 tactic 후보를 하나의 .lean 파일에 private theorem으로 묶어 단일 lake env lean 호출로 검증하는 batched Lean validation 적용

Originality

• 검증기의 4가지 구조화 신호(syntax/type/progress/completion)를 binary pass/fail로 뭉개지 않고 생성 및 탐색의 모든 단계에 명시적으로 되먹임하는 최초의 zero-shot 프레임워크 설계
• Phase 1 실패 tactic과 Lean error message를 Tactician의 negative example로 명시적으로 주입해 MCTS 탐색을 유도하는 방식
• Best-of-N 이후에만 MCTS를 실행하는 2단계 프로토콜을 통해 내부 monotonicity guarantee(Phase 1 solve set이 항상 보존됨)를 형식적으로 증명하여 Phase 2의 기여도를 귀속 가능하게 만든 설계
• 조합론 정리에 특화된 VERITAS-CombiBench라는 새로운 벤치마크를 공개해 lemma name 복구가 어려운 상황에서 unguided sampling의 실패를 드러낸 점
• K개 tactic 후보를 단일 batched Lean 호출로 검증하는 실용적 엔지니어링 트릭

Limitation & Further Study

• Best-of-5 baseline이 독립적으로 실행된 stochastic run이라 VERITAS의 solve set과 subset 관계가 보장되지 않으며, 두 방법 간 직접적인 공정 비교에 한계가 있음
• Strategist가 제안하는 6가지 고정 전략 vocabulary가 특정 유형(예: 조합론의 복잡한 존재성 증명)에는 부족할 수 있어, 전략 다양성 확장이 필요
• Critic과 Tactician에 서로 다른 상용 LLM(Claude Sonnet/Haiku)을 사용하므로 오픈소스 모델이나 타 검증기(Coq, Isabelle 등)로의 일반화 가능성이 본문에서 충분히 검증되지 않음
• miniF2F 40.6%, CombiBench 7.3%로 여전히 최신 SOTA(80% 이상) 대비 낮은 절대 성능이며, 후속 연구로 실패 모드 taxonomy를 기반으로 한 verifier-in-the-loop 탐색의 추가 개선이 필요

Evaluation

총평: 검증기의 구조화된 피드백을 생성 및 탐색 전 과정에 되먹임한다는 간단하지만 효과적인 설계 원칙을 명확한 monotonicity guarantee와 함께 제시하고, 새로운 벤치마크까지 공개해 실증적으로 뒷받침한 점에서 실용적 기여가 큰 연구이다.