Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers

Motivation

• Known: LLM과 Lean 4 같은 interactive theorem prover(ITP)를 결합하여 tactic을 생성하고 컴파일러 검증을 통해 RL로 학습하는 방식(GPT-f, HyperTree Proof Search, AlphaProof 등)은 이미 formal theorem proving에서 활발히 연구되어 왔다.
• Gap: 기존 접근법들은 학습 시 RL이 초기 성능 향상 후 정체되는 performance plateau 문제를 겪고, 추론 시에는 tree search가 전역적 planning 없이 proof depth에 따라 지수적으로 커지는 탐색 공간과 각 탐색 궤적 간 정보 공유 부재라는 한계를 갖는다.
• Why: 학습 시간과 추론 시간의 이중 스케일링 문제를 동시에 해결하는 것은 LLM 기반 reasoning agent 전반, 특히 장기적(long-horizon) multi-turn reasoning과 복잡한 탐색이 필요한 도메인에 일반적으로 적용 가능한 원리를 제공한다는 점에서 중요하다.
• Approach: AlphaZero에서 영감을 받은 multi-stage expert iteration 기반 off-policy RL 프레임워크로 학습 시 plateau를 극복하고, 일반 reasoning model을 planner로 사용해 복잡한 정리를 subgoal로 분해한 뒤 shared proof cache를 통해 병렬 prover agent들이 협업하는 계층적 multi-agent tree search로 추론 시 탐색 공간을 축소한다.

Achievement

Figure 4. Sustained Performance Improvement through Expert Iteration and Periodic Retraining. This graph plots the prove

1. miniF2F 95.08% 달성: 기존 LLM step-prover들을 크게 능가하고 최고 수준의 whole-proof 생성 모델과 대등한 SoTA 성능을 기록.
2. ProofNet-test 41.4% 달성: step-level prover 중 SoTA 수준이며 분포 변화에 대한 강건한 일반화 능력을 입증.
3. 성능 plateau 극복: adaptive tactic-level 데이터 필터링과 주기적 재학습(periodic retraining)을 통해 장기간 RL 학습에서도 지속적 성능 향상을 달성(Fig. 4).
4. 탐색 복잡도 감소: planner 기반 계층적 분해로 전체 계산량을 subgoal 복잡도의 곱에서 합으로 전환, multi-agent 협업 효율성 증대.

How

Figure 3. Overview of the multi-agent tree search architecture. The Planner agent decomposes the main theorem into a seq

• MDP 튜플 M = (S, A, P, R)로 Lean 4 tactic mode의 proof search를 정식화: 상태는 Lean tactic state, 행동은 tactic string, 전이는 Lean checker에 의해 결정적으로 실행, 보상은 성공 증명 궤적에 대해서만 1인 sparse reward.
• multi-stage expert iteration 파이프라인: Proof Generation → Adaptive Tactic Filtering(perplexity 분포 기반, Fig. 2) → Model Refinement의 inner loop를 반복하다가 성능이 plateau에 도달하면 outer loop로 aggressive data curation과 data re-synthesis 후 base checkpoint에서 재학습하는 periodic retraining(soft reset) 수행.
• 추론 시 planner(범용 reasoning model)가 복잡한 정리를 반복적으로 subgoal로 분해하고, 이 subgoal들이 tree search의 "checkpoint" 역할을 하며 성공한 증명 궤적을 shared proof cache에 저장해 병렬 prover agent 팀이 협업하도록 구성(Fig. 3).

Originality

• distillation 없이 tactic-level perplexity 기반 adaptive filtering으로 자동 커리큘럼을 형성하는 off-policy expert iteration 변형을 제안.
• RL plateau 극복을 위한 periodic retraining(soft reset) 메커니즘을 formal theorem proving 도메인에 도입.
• 단일 tree search가 아닌 planner가 주도하는 계층적 subgoal 분해와 shared proof cache를 활용한 multi-agent 협업 탐색 구조를 결합해 탐색 복잡도를 곱셈에서 덧셈 구조로 전환.

Limitation & Further Study

• 논문 발췌본에는 ablation 및 세부 실험 설정(하이퍼파라미터, 필터링 임계값, planner-prover 상호작용 세부 프로토콜)이 충분히 제시되지 않아 각 구성요소의 개별 기여도 검증이 제한적일 수 있음.
• 도메인이 Lean 4 formal mathematics에 국한되어 있어, 저자들이 언급한 "다른 long-horizon multi-turn reasoning 도메인으로의 일반화 가능성"은 실증되지 않은 주장에 머무름.
• shared proof cache 및 multi-agent 협업 시스템의 계산 비용(추론 시 컴퓨팅 자원 소모)에 대한 정량적 분석이 부족해 실용적 배포 시 비용 효율성 평가가 필요.
• periodic retraining이 반복될 때 장기적으로 몇 차례까지 plateau를 극복할 수 있는지에 대한 이론적 한계나 수렴 보장이 제시되지 않음.

Evaluation

총평: 학습과 추론 양쪽의 스케일링 문제를 하나의 통합된 시스템으로 다루며 SoTA 성능을 달성한 실용적이고 견고한 연구로, formal theorem proving을 넘어 다른 reasoning 도메인에도 시사점을 줄 수 있는 우수한 기여다.