Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models

Motivation

• Known: 기존 증명론과 복잡도 이론은 형식적 증명의 존재 여부(Γ ⊢K φ)와 최악의 경우 탐색 난이도만을 다루며, LLM 기반 agentic theorem prover가 실제 워크로드에서 왜, 어떤 요소 덕분에 유한 예산 내 성공하는지는 설명하지 못했다.
• Gap: 실제 정리 증명 워크로드는 라이브러리 정리, 벤치마크군, 재사용 정의, 반복되는 증명 패턴에 편향되어 있음에도, 검증기 피드백·검색(retrieval)·표현 기하학·증명 단축(proof-shortening) 메커니즘이 유한 예산 성공확률에 미치는 영향을 구성요소별로 분리해 설명하는 통계적 이론이 부재했다.
• Why: agentic theorem prover의 각 구성요소(retrieval, verifier feedback, representation learning, proof-shortening)가 성공률 향상에 기여하는 메커니즘을 수학적으로 분리해 설명함으로써, 시스템 설계 선택을 이론적으로 정당화하고 최악 경우 난해성(worst-case hardness)과 모순 없이 실용적 성능 향상을 설명할 수 있다는 점에서 중요하다.
• Approach: 증명 탐색을 결정론적 검증기 동역학을 갖는 finite-horizon reachability MDP로 공식화하고, 충실한 상태 추상화(faithful state abstraction) 하에서 최적 성공확률이 통사적 provability와 일치함을 보인 뒤, depth-wise offline action-value regression과 greedy test-time proving으로 구성된 파이프라인의 provability gap을 이론적으로 분석한다.

Achievement

1. Statistical Provability 개념 정립: 문제 스트림 q0, 검증기 호출 예산 B, prover 정책 π에 대해 유한 예산 내 검증된 증명 도달 확률을 정의하여, 논리적 provability와 알고리즘적 성공확률을 구분하는 새로운 분석 대상을 제시했다.
2. MDP-Provability 동치성 증명: 충실한 proof-state 추상화 하에서 reachability MDP의 최적 성공확률이 예산 B 내 통사적 provability(Prov_B)와 정확히 일치함을 보여, 논리적 엄밀성을 훼손하지 않으면서 가치 기반(value-based) 분석을 가능하게 했다.
3. Provability Gap 상한 정리: 학습된 prover와 최적 prover 간 provability 격차를 occupancy-weighted uniform action-value error의 합으로 상한 지었으며, 균등 오차 가정 하에서 핵심 승수가 학습된 prover의 평균 truncated proof length임을 규명했다.
4. 오차 분해 및 fast rate 조건: 오차를 근사 오차, 학습 분포의 기하학적 coverage, Monte Carlo 라벨 노이즈로 분해하고, action-gap margin 조건 하에서 더 빠른 수렴률(fast rate)을 얻음을 보였다.

How

• 형식적 증명 시스템 K와 검증기를 결정론적 finite-horizon reachability MDP로 추상화 (state=proof obligation+context, action=tactic/inference rule, transition=검증기의 결정론적 업데이트 F)
• Lean, Rocq, Isabelle 등 backward tactic 기반 및 forward natural deduction 기반 증명 탐색 모두를 동일한 verifier-interface 추상화로 포괄 (Proposition 2.1)
• 예산 B 내 도달 가능성을 나타내는 Prov_B(x)를 정의하고, MDP 최적 성공확률과의 동치성을 증명
• depth-wise offline action-value regression(오프라인 rollout으로부터 깊이별 action-value 함수 학습) + greedy test-time proving 파이프라인을 설정
• 학습된 prover의 provability gap을 occupancy-weighted action-value error 합으로 bound하는 주요 정리 도출, 이를 근사오차/coverage/Monte Carlo 노이즈로 분해
• action-gap margin 조건 하 fast rate 개선을 증명

Originality

• 증명론적 provability(논리적 존재)와 통계적 provability(알고리즘적 유한예산 성공확률)를 명확히 구분하고 양자를 MDP 프레임워크로 연결한 최초의 통합적 시도
• 순수 최악 경우(worst-case) 복잡도 이론과 모순 없이, 편향된 실제 워크로드에서의 경험적 성공을 설명하는 통계적 이론을 제시
• retrieval, verifier feedback, representation geometry, proof-shortening 같은 실무적 설계 요소들을 단일 이론적 bound의 항(approximation error, coverage, margin, average proof length)으로 해석하는 component-sensitive account 제공
• 강화학습의 offline action-value regression 이론을 자동 정리 증명(automated theorem proving) 도메인에 특화하여 적용

Limitation & Further Study

• 분석은 검증기 전이가 결정론적(deterministic)이라는 가정에 의존하며, 확률적 verifier나 부분관측(POMDP) 환경으로의 확장은 다루지 않음
• 이론이 "faithful state abstraction"이라는 이상화된 가정에 의존하는데, 실제 시스템에서 이 추상화가 얼마나 충실한지에 대한 실증적 검증이 부족함
• 제시된 bound는 주로 uniform-error reading 하에서 해석되며, 실제 학습된 action-value function의 오차 분포가 이 가정을 만족하는지에 대한 실험적 검증이 본문 발췌에는 제시되지 않음
• 후속 연구로는 실제 Lean/Rocq 기반 agentic prover에서의 실증적 검증, 확률적 verifier로의 확장, search(beam search 등) 알고리즘까지 포괄하는 이론 확장이 필요함

Evaluation

총평: agentic theorem prover의 경험적 성공을 MDP 및 통계적 학습 이론의 언어로 정교하게 설명하는 이론적 기여가 돋보이며, 실무적 설계 선택(retrieval, verifier feedback 등)에 대한 해석적 통찰을 제공하는 점에서 가치가 크나, 실증적 검증과 결정론적 가정의 일반화 가능성에 대한 추가 논의가 필요하다.