Peano Player: Interactive Theorem Proving as a Constrained MDP

Motivation

• Known: 기존 RLVR 기반 신경망 정리 증명 연구들은 완성된 proof 전체에 대한 단일 binary verification reward만으로 학습하는 whole-proof(bandit-style) 접근을 주로 사용하며, 일부 연구(Kim & Yun, 2026)는 post-hoc하게 첫 실패 tactic을 찾아 역전파하는 process supervision을 도입했다.
• Gap: 기존 방법들은 tactic 실패를 사소한 penalty로만 취급하고 실패 이후에도 생성을 계속 허용하며, 여전히 proof 전체를 생성한 뒤에야 verifier 피드백을 받는 bandit 구조를 벗어나지 못해, 매 단계 verifier가 실제로 제공하는 proof state와 즉각적인 tactic 실패 신호를 학습에 온전히 활용하지 못한다.
• Why: 모든 tactic-level proof assistant는 매 스텝마다 proof state 갱신과 실패 여부라는 동일한 신호를 제공하므로, 이 신호를 constraint로 명시적으로 정식화해 학습에 반영하는 방법은 다양한 정리 증명 시스템에 일반적으로 적용 가능한 원리를 제시한다는 점에서 중요하다.
• Approach: tactic 적용의 유효성을 목표(reward)가 아닌 제약(constraint)으로 취급하여, proof 종료 시 sparse binary reward를 부여하고 tactic 실패 시 동일 크기의 terminal cost를 부과하는 CMDP로 정리 증명을 정식화하고, Peano numbers 위의 confluent하고 terminating한 rewrite 시스템 기반 통제된 equational-theory 환경에서 이를 검증한다.

Achievement

Figure 1. Held-out solve rate by theorem difficulty. Curves show

1. CMDP 정식화: tactic-level 정리 증명을 proof closure를 reward로, tactic failure를 별도의 cost로 분리하는 constrained MDP로 최초로 정식화했다.
2. 통제된 평가 환경 구축: confluent·terminating한 rewrite 시스템을 이용해 난이도가 통제되고 증명 가능성이 보장된(construction에 의해 증명되는) 정리를 무한히 생성하는 Peano numbers 기반 equational-theory 환경을 구축했다.
3. 성능 개선 입증: proof-state 관찰과 tactic-failure cost 각각이 독립적으로 solve rate를 향상시키며, 둘을 결합하면 가장 강한 baseline 대비 전체 solve rate가 4배 이상, 최고 난이도에서는 10배 향상됨을 실험적으로 보였다.

How

Figure 3. Tactic failure rate by theorem difficulty. Curves show

• CMDP를 (S, A, P, R, C, γ, α) 튜플로 정의하고, Lagrangian relaxation을 통해 penalized reward r̂(s,a) = R(s,a) − λC(s,a) (λ=1 고정)로 변환하여 unconstrained objective로 학습
• proof state 관찰 여부와 tactic-failure cost 부과 여부를 각각 독립 변수로 하는 ablation 설계 (proof-state 관찰 O/X × tactic-failure cost O/X)
• Peano numbers 위 4개의 deterministic rewrite tactic으로 구성된 환경에서 normal form을 샘플링하고 reducibility를 보존하는 expansion을 적용해 proof search 없이 by-construction으로 증명 가능한 정리를 생성
• GRPO(Group Relative Policy Optimization) 기반 bandit-style whole-proof baseline 및 Kim & Yun(2026)의 post-hoc per-tactic feedback 방식과 비교
• 난이도별 held-out solve rate, on-policy 학습 중 solve rate, 난이도별 tactic failure rate를 측정하여 비교 평가

Originality

• 정리 증명을 multi-step MDP로 전환하고 tactic 유효성을 constraint로, proof closure를 reward로 분리하는 CMDP 프레임워크를 정리 증명 도메인에 처음으로 적용
• 로보틱스·안전 RL에서 확립된 reward/cost 분리 원칙(Altman, 1999; Tessler et al., 2019)을 tactic-level 정리 증명에 유비적으로 적용한 점
• proof search나 비용이 큰 데이터셋 구축 없이 confluent·terminating rewrite 시스템을 이용해 무한한 난이도-통제 정리를 by-construction으로 생성하는 절차적 환경 설계

Limitation & Further Study

• 실험이 Peano numbers 위의 4개 deterministic rewrite tactic으로 이루어진 소규모 합성 equational-theory 환경에 국한되어, Lean과 같은 실제 대규모 proof assistant 및 MiniF2F, ProofNet 등 표준 벤치마크로의 일반화 가능성은 검증되지 않음
• Lagrange multiplier λ를 1로 고정하고 튜닝하지 않아, RCPO 등 λ를 적응적으로 조정하는 기법과의 비교나 최적 λ 탐색이 이루어지지 않음
• context 기반 verifier 피드백(에러 메시지를 reasoning chain에 포함하는 방식)과의 상호보완성을 언급했으나 실제 결합 실험은 수행하지 않음
• 후속 연구로 실제 Lean/Coq 등 산업 규모 proof assistant 환경에서의 검증, λ 적응적 조정 기법 적용, context 기반 피드백과의 결합 실험이 필요함

Evaluation

총평: tactic-level 정리 증명을 CMDP로 정식화하여 proof state 관찰과 tactic 실패 신호를 통합적으로 활용하는 아이디어는 간결하면서도 설득력 있고, 통제된 실험을 통해 solve rate의 큰 향상을 입증했으나 소규모 합성 환경에 국한된 검증이라는 점에서 실제 proof assistant로의 확장성 검증이 후속 과제로 남는다.