기술 요약: VERITAS: 제로샷 형식 정리 증명을 위한 검증기 유도형 증명 탐색

문제 정의

현재의 대규모 언어 모델(LLM) 기반 형식 정리 증명 도구들은 형식 검증기(Lean 4와 같은)로부터 오는 풍부하고 구조화된 신호를 단순히 이진적인 통과/실패(pass/fail) 결과로 축소시키는 경頃향이 있습니다. 검증기는 구문 오류, 타입 불일치, 부분적인 목표 진행 상태, 증명 완료 상태를 포함한 세밀한 피드백을 제공합니다. 그러나 표준 파이프라인은 이러한 중간 산출물들을 무시하고 이를 스칼라 보상으로 요약하거나 완전히 버립니다. 이는 검색 알고리즘이 검증기가 이미 명시적으로 제공한 정보를 다시 "재학습"하게 만들며, 각 단계의 정당성이 이전 단계가 목표에 미친 효과에 달려 있는 의존적 전술(tactic) 체인이 필요한 증명에서는 특히 비용이 많이 드는 한계가 됩니다.

방법론: VERITAS 프레임워크

VERITAS는 모든 검증기 신호를 증명 생성 과정으로 다시 라우팅하도록 설계된 제로샷 프레임워크입니다. 이는 공유된 증명 상태와 2단계 검색 프로토콜을 통해 조정되는 4개 에이전트 아키텍처를 채택합니다.

1. 네 가지 특화된 에이전트

모 모든 에이전트는 정리, 현재 목표, 가설, 전술 이력 및 Lean으로부터 오는 4가지 구조화된 신호를 포함하는 공유 ProofState 상에서 작동합니다.

• 전략가 (Strategist): 증명 상태를 6가지 고수준 전략(직접, 귀납, 모순, 케이스 분류, 재작성, lemma_apply) 중 하나로 매핑하고, 탐색 범위를 제한하기 위해 깊이를 추정합니다.
• 검색기 (Retriever): 키워드 중첩도를 목표 토큰, 렘마 이름 및 시그니처와 비교하여 점수를 매겨 관련 Mathlib 전제(premises)를 찾아냅니다.
• 비평가 (Critic): 부분적인 증명 상태를 점수화하고 다음 전술을 제안하며 가지치기(pruning) 권고를 수행하는 경량 모델입니다. 이는 MCTS의 무작위 롤아웃을 Lean의 4방향 피드백이 통합된 가치 추정치로 대체합니다.
• 전술가 (Tactician): 전략, 검색된 전제, 비평가의 가이드, 그리고 결정적으로 이전에 실패한 전술 목록과 그에 따른 특정 Lean 에러 메시지를 부정적 예시(negative examples)로 주입받아 조건화된 $K$개의 전술 후보를 생성합니다.

2. 단조성 보장을 갖춘 2단계 프로토콜

프레임워크는 피드백 기반 탐색에 의한 이득을 명확히 입증하기 위해 보수적인 2단계 프로토콜을 사용합니다.

• 1단계 (Best-of-N): 표준 Best-of-N 스윕(예: $N=5$)을 통해 단일 배치로 전술을 생성합니다. 만약 하나라도 성공하면 즉시 정리가 해결됩니다.
• 2단계 (Critic-Guided MCTS): 1단계가 실패했을 때만 활성화됩니다. 1단계의 실패 집합(전술 및 해당 에러)은 전술가의 시스템 프롬프트에 부정적 예시로 주입됩니다. 비평가는 다음과 같이 구성된 몬테카를로 트리 탐색(MCTS)을 가이드합니다:
  • 선택 (Selection): 비평가의 가치와 전략 일치성을 통합한 확장된 UCB 공식을 사용합니다.
  • 확장 (Expansion): 에이전트들이 순차적으로 실행되며, 후보들은 배치형 Lean 검증(Batched Lean Validation) 기법을 통해 검증됩니다.
  • 시뮬레이션 (Simulation): 무작위 롤아웃을 구조화된 신호($\sigma_A$ 구문, $\sigma_B$ 타입, $\sigma_C$ 진행, $\sigma_D$ 완료)로 보강된 비평가의 가치로 대체합니다.
  • 역전파 (Backpropagation): 이진 승패로 축소하지 않고 구조화된 신호를 상위로 전달하여 부분적인 진행에 대한 크레딧을 보존합니다.

배치형 Lean 검증: 확장을 위해 Lean을 $K$번 호출하는 대신, 후보들을 하나의 .lean 파일 내의 프라이빗 정리로 컴파일하여 단 한 번의 호출로 검방합니다. 이는 검증 비용을 $O(K)$에서 $O(1)$로 줄여 약 $10\times$의 속도 향상을 가져옵니다.

단조성 (Monotonicity): 이 프로토콜은 최종 해결된 정리의 집합이 1단계만으로 해결된 집합의 상위 집합($S \supseteq S_1$)임을 보장합니다. 이를 통해 2단계의 기여도를 격리하여, 추가적인 해결 사례가 엄격하게 피드백 기반 탐색 덕분임을 보장합니다.

주요 기여

1. 제로샷 4-에이전트 프레임워크: 별도의 미세 조정 없이 구조화된 Lean 피드백(구문, 타입, 진행, 완료)을 모든 생성 결정에 라우팅하는 시스템입니다.
2. 2단계 프로토콜: Best-of-N $\to$ Critic-MCTS 설계와 내부 단조성 보장을 통해 탐색 기여도를 명확히 규명할 수 있게 합니다.
3. 효율성 최적화: 검증 오버헤드를 약 $10\times$ 감소시키는 배치형 Lean 검증 기법을 제공합니다.
4. VERITAS-CombiBench: 가이드 없는 샘플링의 한계를 드러내기 위해 공개된, 저자가 직접 검증한 55개의 어려운 조합론 정리로 구성된 새로운 벤치마크입니다.
5. 기여 분석: 평면 샘플링(flat sampling)으로는 도달할 수 없었던 11개의 miniF2F 정리가 MCTS 단계에 의해 유일하게 해결되었음을 보여주는 실증적 근거를 제시합니다.

실험 결과

실험은 miniF2F(244개 정리)와 VERITAS-CombiBench(55개 정리)에서 수행되었습니다.

• miniF2F 성능: VERITAS는 **40.6%**의 해결률(99/244)을 달성하여, 독립적인 Best-of-5 베이스라인(36.9%)과 핸드크래프트된 포트폴리오(26.2%)를 능가했습니다.
  • 2단계는 평면 샘플링이 도달할 수 없었던 11개의 고유한 해결 사례를 기여했으며, 이는 주로 2~4개의 의존적 전술이 필요한 문제들에서 나타났습니다.
  • "hard" non-sorry 문제에서 VERITAS는 Best-of-5의 25.9% 대비 28.9%를 기록했습니다.
• VERITAS-CombiBench 성능: 이 벤치마크는 가이드 없는 샘플링의 실패를 극명히 보여주었습니다. Best-of-5는 LLM이 잘못된 Mathlib 렘마 이름을 환각(hallucination)했기 때문에 **1.8%**에 그쳐 포트폴리오(3.6%)보다 낮은 성적을 냈습니다. VERITAS는 Lean의 에러 피드백을 사용하여 이러한 이름들을 반복적으로 수정함으로써 **7.3%**에 도달했습니다.
• 효율성: VERITAS는 추론 전용 방법론 중 파레토 최적선(Pareto frontier)을 점유하며, 정리당 약 27회의 Lean 호출과 약 $150의 API 비용로 40.6%의 해결률을 달성했습니다.
• 실패 모드: 분석 결과, 실패의 32%는 구문 수준(이름 환각), 17%는 타입은 맞지만 틀린 경우, 10%는 비평가가 높은 가치 가이드를 제공할 수 있었던 "근접 실패(near-misses, 부분적 목표 진행)"인 것으로 나타났습니다.

의의 및 주장

본 논문은 일반적인 설계 원칙을 제시합니다: 결정론적 검증기가 구조화된 중간 신호를 방출할 때, 이를 생성 과정에 다시 결합하는 것은 단순한 추가 샘플링보다 LLM을 훨씬 더 크게 증폭시킨다.

VERITAS는 다음을 입증합니다:

1. 상태로서의 검증기 신호: 결정론적 검증기 신호는 단순한 최종 체크가 아니라 추론 시점의 상태(state) 역할을 할 수 있습니다.
2. 구성 요소 간의 시너지: 검증기와 생성을 긴밀하게 결합하는 것이 LLM이나 검색 구성 요소 중 하나만을 개별적으로 확장하는 것보다 더 효과적입니다.
3. 반복적 교정: 정밀한 렘마 추출이 필요한 도메인(예: 조합론)에서는, 평면 샘플링이 어휘적으로 틀린 이름을 환각하는 경향이 있는 반면, 검증기 에러를 통한 반복적 교정이 더 우월합니다.

저자들은 VERITAS가 IMO 수준의 창의성이나 대화형 지연 시간을 해결하는 해결책은 아니지만, 핵심 기여는 라우팅에 있다고 결론짓습니다. 즉, 1단계에서 쉬운 증명들을 효율적으로 수집하고, 검증 실패가 다음 전술을 가이드할 수 있는 곳에만 2단계에서 계산 자원을 집중하는 것입니다. 향후 과제로 검색 능력 개선, 더 저렴한 비평기 생성, 그리고 이 원칙을 남은 어려운 문제들에 적용하기 위한 2단계 트레이스(trace) 증류 등이 제시되었습니다.