LeanRefiner: Agentic Global-to-Local Optimization of Lean Proofs

Motivation

• Known: Lean과 Mathlib 기반의 자동 정리 증명(automated theorem proving)과 autoformalization 분야는 LeanDojo, DeepSeek-Prover-V2, Prover Agent 등으로 빠르게 발전하여 미해결 목표에 대한 검증된 증명을 대규모로 생성할 수 있게 되었다.
• Gap: 기존 연구는 대부분 아직 풀리지 않은 정리를 증명하거나 informal 수학을 formal화하는 데 집중했을 뿐, 이미 verifier를 통과한 증명이 장황하고 반복적이며 유지보수하기 어렵다는 문제, 즉 correctness 확보 이후의 증명 최적화 문제는 충분히 다뤄지지 않았다.
• Why: 자동 생성된 Lean 증명이 늘어나면서 검증 통과 여부와 별개로 가독성과 유지보수성이 중요한 실무적 문제가 되며, hard correctness constraint를 유지하면서 증명을 압축·재구성하는 기법은 formal math 라이브러리의 품질과 확장성에 직접적으로 기여한다.
• Approach: LeanRefiner는 theorem-level global restructuring agent와 pattern-guided local reduction agent를 단계적으로 결합하고, 최종적으로 Lean 컴파일·sorry 없음·theorem statement 보존·길이 감소를 검사하는 unified verifier-guided selector로 후보 증명의 채택 여부를 결정하는 agentic 프레임워크이다.

Achievement

Figure 1. Proof length distributions on the combined main bench-

1. Proof optimization after correctness 과제 정식화: 이미 verified된 Lean 증명을 compilation, sorry 없음, declaration 보존 등 hard gate 하에서 재작성하는 문제로 최초로 formalize함.
2. LeanRefiner 프레임워크 제안: theorem-level global restructuring과 bounded proof fragment 단위의 local reduction을 결합한 agentic 시스템을 설계함.
3. 세 개의 verified Lean proof collection에 대한 대규모 실험: LeanRefiner가 엄격한 verifier 제약을 만족하면서도 일관되게 proof length를 줄임을 실증함 (예: median 60줄에서 21줄로 감소).
4. 원인 분석: 성능 향상이 단순 cleanup이나 특정 backend 의존이 아니라 global-local agent 간 staged collaboration에서 기인함을 ablation을 통해 규명함.

How

Figure 2. Overview of LeanRefiner. Starting from a verified but redundant proof, the system performs theorem-level globa

• 입력: sorry 없이 검증된 Lean 증명 p
• Global restructuring agent: theorem-first global task, semantic proof plan, compact external-lemma frontier를 이용해 더 짧은 proof route를 재구성
• 후보가 Lean에서 accept되면 시스템이 proof structure를 재추출하여 갱신된 context를 local agent에 전달
• Local reduction agent: proof zones와 verifier diagnostics를 바탕으로 redundant/compressible fragment에 대해 bounded replacement를 탐색
• Unified verifier-guided selector: Lean 통과, theorem statement 보존, 새로운 sorry 없음, 현재 proof보다 길이 단축이라는 조건을 모두 만족할 때만 후보를 채택
• 세 개의 verified Lean proof collection에서 proof length 변화와 backend sensitivity, per-proof length 비교, 대표 사례(AMC12A 2003 P5) 등을 통해 검증

Originality

• 기존 Lean 자동화 연구가 주로 미해결 목표 증명(theorem proving)이나 autoformalization에 집중한 것과 달리, "correctness 확보 이후"의 증명 최적화라는 새로운 task를 명시적으로 정의함
• ImProver, ProofOptimizer, ProofJudge 등 유사한 proof optimization 연구와 달리, global-to-local의 staged agent 협력 구조와 verifier-guided hard gate를 결합한 점이 차별화됨
• 단일 학습된 simplifier가 아니라 theorem-level 재구성과 local pattern 기반 축소를 분리된 agent로 설계하여 서로 다른 Lean-derived view(전역 planning artifact vs 로컬 proof zone/diagnostics)를 활용하는 구조적 독창성이 있음

Limitation & Further Study

• 발췌된 초록·본문 상 실험 세부사항(구체적 backend LLM, 데이터셋 규모, baseline과의 정량적 비교 수치)이 충분히 제시되지 않아 재현성 및 일반화 가능성 평가가 제한적임
• 가독성(readability)이 길이만으로 완전히 결정되지 않는다는 점을 스스로 인정하면서도, 평가 프로토콜이 여전히 길이 감소와 verifier 통과 위주로 구성되어 있어 사용자 관점의 정성적 가독성 평가가 부족할 수 있음
• global-local agent의 staged collaboration이 계산 비용(반복적 Lean 컴파일 및 LLM 호출)을 얼마나 증가시키는지에 대한 효율성 분석이 필요함
• 후속 연구로 human-facing proof quality(예: ProofJudge와 같은 pairwise preference)와의 결합, 더 다양한 도메인의 정리들에 대한 일반화 검증이 필요함

Evaluation

총평: 검증된 Lean 증명의 사후 최적화라는 실용적이면서도 그동안 간과되었던 문제를 명확히 정의하고, verifier 제약 하에서 작동하는 global-to-local agentic 시스템으로 유의미한 길이 감소를 달성한 점에서 의미 있는 기여이나, 정량적 비교와 가독성 평가의 심층성은 향후 보완이 필요하다.