Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search

Motivation

• Known: LLM이 RL로 생성한 Lean proof는 correctness에는 강하지만 장황하고 가독성이 낮으며, 기존 code refactoring 연구는 fine-tuning 기반 혹은 agentic framework 기반으로 이 문제를 다뤄왔다.
• Gap: 기존 Lean refactoring 연구는 proof length, compilation cost, version compatibility가 서로 tension 관계에 있는 multi-objective 특성을 간과했고, Lean/Mathlib의 빠른 버전 변화에 LLM의 knowledge cutoff가 대응하지 못하며, training 기반 파이프라인은 매 LLM 릴리즈마다 재학습이 필요해 model churn과 Lean 릴리즈 주기 모두에 확장성이 없다.
• Why: Lean/Mathlib은 기계 검증 수학 및 LLM 기반 정리 증명 연구의 핵심 인프라인데, 장황하고 버전에 취약한 proof는 사람의 이해와 compilation을 어렵게 하여 대규모 라이브러리(Mathlib) 유지보수에 실질적 병목이 되므로, 이를 재학습 없이 해결하는 것은 실용적으로 중요하다.
• Approach: frozen agentic LLM을 Lean/Mathlib 버전과 예상 compilation-cost 감소 등이 densely annotated된 refactoring strategy database로부터의 retrieval로 steering하여, 추론 시점에 다중 목적을 동적으로 필터링·재순위화(rerank)하는 방식을 제안한다.

Achievement

1. 대규모 데이터셋 공개: 200K개 이상의 long-short proof pair와 9K개의 refactoring strategy(컴파일 비용 감소 및 호환 Lean/Mathlib 버전이 주석된)로 구성된 현재까지 최대 규모의 Lean refactoring dataset을 공개했다.
2. 압축 성능: miniF2F, PutnamBench, Putnam2025 등 competition benchmark에서 70% 이상의 token-level compression, PFR·PhysLean·Analysis·FLT 등 연구용 repository에서 20% 이상의 compression을 달성하며 기존 연구와 Claude Code를 능가했다.
3. 다중 목적 제어 가능성: 길이 외에도 compilation cost를 30% 이상 절감하고, Lean 버전 전반에 걸쳐 compression 성능을 유지하며, refactor된 miniF2F proof가 향후 Lean/Mathlib 릴리즈에 대해 원본보다 더 강한 zero-shot version transfer(type-check 성공률)를 보였다.

How

Figure 4. Overview of Lean Refactor framework. 1. We first summarize raw long-short proof pairs sourced from diverse Lea

• raw long-short proof pair로부터 title, natural-language description, precondition pattern, step-by-step application guide, before/after example, categorical potential length reduction tag의 6개 필드로 구성된 재사용 가능한 refactoring strategy를 distill하여 strategy bank를 구축.
• 각 strategy는 Lean/Mathlib version compatibility 및 expected compilation-cost reduction 등 메타데이터로 densely annotated됨.
• 추론 시 target proof를 dependency annotation을 통해 semantically grounding하고, multi-objective retrieve-and-rerank pipeline으로 proof length·compilation cost·version compatibility 간 trade-off를 사용자 지정 목적에 맞게 조정.
• planner, refactorer, debugger로 구성된 plug-and-play agent loop를 통해 어떤 frozen frontier LLM(Gemini, Claude, GPT 계열)이든 재학습 없이 프레임워크에 연결 가능하도록 설계.
• version-filtered retrieval을 통해 특정 target Lean 버전에 맞춘 strategy만 선별적으로 활용.

Originality

• Lean proof refactoring을 proof length뿐 아니라 compilation cost, version compatibility까지 포함한 native multi-objective 문제로 재정의하고, 이들 간의 tension(약한 상관관계, Pearson correlation 0.09~0.12)을 실증적으로 입증했다.
• 모델 fine-tuning 없이 frozen LLM을 retrieval-augmented strategy bank로 steering하여 Lean/Mathlib의 빠른 버전 변화와 LLM knowledge cutoff 간의 misalignment 문제를 해결하는 접근은 기존 training 기반 refactoring 연구와 차별화된다.
• competition proof에 편중된 기존 벤치마크의 한계를 지적하고 연구 수준(research-level) repository(PFR, PhysLean, Analysis, FLT)로 평가를 확장한 점이 독창적이다.

Limitation & Further Study

• 발췌된 본문에는 strategy bank 구축 및 retrieve-and-rerank 파이프라인의 세부 알고리즘, ablation 분석이 충분히 제시되지 않아 각 컴포넌트(메타데이터 필터링, reranking)의 개별 기여도를 판단하기 어렵다.
• version transfer 실험이 miniF2F라는 competition benchmark에 국한되어 있어, research-level repository에서의 version robustness 검증이 부족해 보인다.
• strategy bank 자체의 최신성 유지(재프로파일링) 비용과 자동화 정도, 그리고 매우 새로운 Mathlib API에 대한 strategy 부재 시 성능 저하 가능성에 대한 논의가 필요하다.
• 후속 연구로 strategy bank의 자동 업데이트 메커니즘과 더 다양한 정리 증명 언어(Coq, Isabelle 등)로의 일반화 가능성을 탐구할 수 있다.

Evaluation

총평: Lean proof refactoring의 실용적 난점(multi-objective tension, version fragility, 데이터 부족)을 명확히 규명하고, 재학습 없는 retrieval-augmented agentic 접근으로 이를 해결한 실용적이고 임팩트 있는 연구이나, 워크숍 페이퍼 특성상 세부 방법론과 ablation 검증이 다소 제한적이다.