What Helps Agentic Lean Provers? A Trace-Level Attribution Study

Motivation

• Known: 기존 연구들은 tool-bearing harness(compiler feedback, retrieval, search, decomposition)를 결합하여 Lean agent의 end-to-end 성능을 향상시켜 왔으나, 어떤 요소가 실제로 성능 향상에 기여하는지는 불분명했다.
• Gap: 복잡한 agentic Lean prover는 base model, feedback loop, retriever, tool interface, search policy, test-time compute 등 여러 요소가 얽혀 있어 pass rate만으로는 어떤 구성 요소가 실제로 도움이 되는지 attribution하기 어렵다는 근본적 한계가 존재한다.
• Why: 단순 pass rate 비교로는 성능 향상의 원인을 알 수 없어, 실패 유형(retrieval 부족, search 실패, commitment 실패)에 따라 다른 개선책이 필요함에도 이를 구분하지 못하면 향후 agent 설계 방향을 잘못 잡을 위험이 있다.
• Approach: capability ladder(M0, BoN, M1, M1.5, M2, M2.5, M3)를 정의하여 compiler feedback, residual proof-state feedback, interactive tool 채널, retrieval을 하나씩 순차적으로 추가하며 aggregate pass rate와 trace 수준의 행동 변화를 함께 분석한다.

Achievement

Figure 1. Lower-ladder outcomes on standalone_mix100.

1. Compiler feedback의 명확한 효과: M1@8(compiler-error refinement)는 네 번의 Gemini 반복 실행에서 5–8/100을 해결하여, one-shot generation(0/100) 및 BoN@8(3/100) 대비 뚜렷한 향상을 보였다.
2. Residual proof-state feedback의 혼재된 효과: M1.5는 일부 매칭 row(seed 89 @8, seed-42B depth @16에서 12/100)에서는 개선을 보이나 seed 42A @8에서는 M1이 더 우수해, 일관된 우위를 주장할 수 없는 pre-tool baseline으로 자리매김한다.
3. Tool access와 tool use의 괴리 규명: M2에서 LSP/MCP 스타일 도구(diagnostics, goal, term-goal, hover, completions, whole-file run-code)를 도입해도 모델은 whole-file compilation을 주된 정보 채널로 삼을 뿐, 추가 도구는 별다른 이득을 주지 못함을 보였다.
4. Trace 기반 실패 모드 규명: 다수의 실패 run이 최종 제출로 이어지지 않고 계속 tool을 탐색(probing)하는 commitment failure 패턴을 발견하여, 향후 retrieval/search/restart/decompose/commit 정책 설계의 구체적 목표를 제시하였다.

How

Figure 3. Tool-use summary in the M2 Gemini LSP configura-

• Lean 4 벤치마크(100 tasks: ProofNetSharp 40개, FATE-H 20개, FATE-X 20개, 최근 대회 문제 20개)를 frozen 상태로 고정하여 사용
• Kimina Lean Server 기반의 경량 Python harness를 구축하여 model response, proof submission/tool call, tool execution, JSONL trace logging을 alternating 방식으로 수행
• capability ladder(M0 one-shot → BoN → M1 compiler feedback → M1.5 residual proof-state → M2 interactive tool → M2.5 submission-local feedback/Mathlib → M3 premise retrieval)를 단계별로 정의하고 각 rung에서 attribution 질문을 설정
• Gemini-3-Flash와 DeepSeek-V4-Flash 두 모델 계열에서 실험을 수행하되, Gemini는 shallow-feedback block과 M2 tool-surface 비교에, DeepSeek-V4-Flash는 더 저렴한 비용으로 richer tool/retrieval 캠페인에 활용
• solve 판정은 compile-plus-hygiene 기준(오류 없음, sorry 없음, cheat pattern/theorem drift 없음)으로 엄격히 정의
• 4×40 protocol(최대 4회 제출, 제출 전 최대 40회 tool call)로 명확한 commit point를 설정하고 trace 로그를 통해 tool 사용 패턴, solve-set 분포 등을 분석

Originality

• pass rate라는 단일 aggregate 지표 대신 trace-level 분석을 통해 agentic Lean prover의 각 구성 요소(compiler feedback, proof-state feedback, tool access, retrieval)를 개별적으로 isolate하여 attribution한 최초의 체계적 시도
• capability ladder라는 명시적 프레임워크를 제안하여 각 rung이 답해야 할 attribution 질문을 명확히 규정
• tool access와 tool use를 구분하는 개념적 기여: 도구가 제공된다고 해서 자동으로 더 나은 prover가 되는 것이 아니라 문제를 해결하는 경로(route)만 바뀐다는 관찰
• commit-vs-explore behavior를 명시적 정책 목표로 제시하여, 최종 verdict만이 아니라 trace 자체를 supervision signal로 활용해야 한다는 방법론적 제안

Limitation & Further Study

• 100-task라는 비교적 작은 고정 벤치마크와 제한된 seed/run 수(특히 M1.5 등에서 결과가 seed에 따라 mixed)로 인해 통계적 신뢰도가 낮고 일부 결론(M1.5 우위 여부 등)이 dominance result가 아닌 잠정적 관찰에 그침
• 실험이 여러 harness revision에 걸쳐 수행되어 완전히 통제된 단일 환경이 아니며, repository commit이 아닌 benchmark/verifier contract만을 고정 요소로 삼음
• Gemini와 DeepSeek-V4-Flash 간 richer tool/retrieval 실험이 불균등하게 배분되어(DeepSeek 위주) 모델 간 완전한 대응 비교가 어려움
• 4×40 protocol의 cap 설정이 결과에 미치는 영향에 대한 추가 검증과, retrieval(M3) 단계의 구체적 이득에 대한 더 깊은 분석이 후속 연구로 필요
• 향후 연구는 trace 기반 신호를 활용해 명시적인 retrieve/search/restart/decompose/commit 정책을 학습하는 방향으로 확장될 수 있음

Evaluation

총평: Agentic Lean prover의 성능을 구성 요소별로 분해하여 분석한 실용적이고 시의적절한 attribution 연구로, 특히 tool access와 tool use의 구분 및 commitment failure 발견은 향후 agent 설계에 중요한 시사점을 준다. 다만 소규모 벤치마크와 mixed된 통계적 결과로 인해 일부 결론의 확증성은 제한적이며 workshop-level 초기 연구로서의 성격이 강하다.