Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean

Motivation

• Known: 기존 agentic theorem prover들은 문제를 자연어 lemma로 분해하고 Lean으로 형식화한 뒤 다수의 proof attempt를 샘플링하고 compiler feedback으로 self-correction을 수행하여 PutnamBench, MiniF2F 등에서 높은 성능을 달성해왔다.
• Gap: 이러한 워크플로우는 모든 입력에 동일한 사전 지정 budget(decomposition, proof generation, self-correction 횟수)을 부여하는 fixed-step policy를 사용하여, 실패할 가능성이 높은 attempt에도 상당한 compute를 낭비하며 문제당 $40~$50에 달하는 비용을 초래한다. 기존 연구는 성능 향상에만 집중했고 워크플로우 비용 최적화 관점은 거의 다루지 않았다.
• Why: Lean 증명은 compiler로 자동 검증 가능해 대규모 샘플링이 가능하지만 그만큼 비용이 폭발적으로 증가하므로, 실패한 궤적으로부터 신호를 추출해 언제 재시도하고 언제 포기할지 결정하는 것은 agentic theorem proving을 실용적 규모로 확장하는 데 핵심적이다.
• Approach: data plane과 control plane으로 구성된 action routing agent를 제안하여, data plane이 자연어 lemma 분해·형식화·proof attempt 샘플링을 수행하고 control plane이 과거 실패한 Lean attempt들을 관찰해 성공 가능성과 추가 시도 비용을 추정한 뒤 현재 target을 계속 시도할지 새로운 breakdown으로 재시작할지 결정한다.

Achievement

Figure 5. Whole-proof cost-quality curves on PutnamBench

1. 비용 절감: PutnamBench 85개 문제 부분집합에서 fixed-step baseline 대비 동일 정확도(parity accuracy)에서 평균 28.9%의 비용 절감을 달성했다.
2. 정확도 향상: 동일 비용(parity cost) 기준으로는 7.9%의 정확도 향상을 보였다.
3. 효율적 자원 배분 근거 제시: 실패한 Lean trajectory가 cost-aware resource allocation을 위한 actionable signal을 제공함을 실증적으로 보였다.

How

Figure 4. Comparison between the fixed-step data plane pipeline

• Breakdown module: GPT-OSS-20B(high reasoning effort)를 사용해 원문제를 자연어로 먼저 풀고, 자연어 solution을 여러 lemma로 구조화한다.
• Formalization 및 proof attempt 샘플링: 자연어 lemma들을 Lean으로 형식화하고, 각 theorem/lemma target에 대해 proof attempt를 샘플링한다(Varambally et al., 2025; Chen et al., 2025c의 lemma-style prover 설계를 계승).
• Control plane(router): 과거 agent history (state, action)로부터 feature x1...xn을 추출하는 경량 모델을 학습시켜, 다음 attempt의 성공 확률(quality) q̂와 비용 ĉ을 추정한다.
• Cost-quality tradeoff 결정: q̂ − λĉ 형태의 tradeoff 점수를 계산하여, 현재 target에 대해 추가 attempt를 지속할지, 아니면 새로운 breakdown으로 restart할지를 동적으로 결정한다.
• 평가: PutnamBench 85문제 부분집합에서 fixed-step baseline과 여러 cost-quality metric(비용-품질 곡선 등)으로 비교한다.

Originality

• Lean 형식 증명이라는 완전 검증 가능한 도메인에 routing/cascading 문헌의 아이디어를 최초로 적용하여, 구조화된 proof trajectory를 관찰하는 agentic search 특유의 환경에 맞춘 router를 설계했다.
• 기존 agentic prover 연구가 성능(solve rate) 극대화에만 집중한 것과 달리, fixed-step policy의 비효율성을 명시적으로 문제 제기하고 cost-quality tradeoff라는 새로운 최적화 축을 도입했다.
• 실패한 Lean attempt trajectory 자체를 향후 성공 확률·비용 추정을 위한 신호로 활용한다는 관점이 참신하다.

Limitation & Further Study

• 평가가 PutnamBench의 85문제라는 비교적 작은 부분집합에 국한되어, 다른 벤치마크(MiniF2F, 연구 수준 문제 등)나 더 큰 규모에서의 일반화 가능성이 검증되지 않았다.
• λ(cost-quality tradeoff 가중치) 선택이나 경량 router 모델의 구체적 학습 방식, feature 설계에 대한 세부 분석과 ablation이 본문 발췌만으로는 충분히 드러나지 않는다.
• baseline이 fixed-step policy 하나로 한정되어, 다른 adaptive/routing 기반 baseline과의 비교가 부족할 수 있다.
• 후속 연구로 다양한 도메인 특화 prover 모델과의 결합, 더 큰 벤치마크로의 확장, router의 online 학습 및 적응 능력 개선 등이 필요하다.

Evaluation

총평: Lean agentic theorem proving에서 흔히 간과되던 비용 효율성 문제를 정면으로 다루며 실용적으로 의미 있는 개선(28.9% 비용 절감)을 보여주는 좋은 워크숍 논문이나, 평가 규모가 작아 일반화 검증이 추가로 필요하다.