Skip to content

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

🕒 Published (v1): 2026-05-18 04:19 UTC · Source: Arxiv · link

Why this paper was selected

Lean Refactor: plug-and-play harness for multi-objective controllable proof optimization

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

Lean Refactor is a retrieval-augmented agentic framework that steers a frozen LLM to refactor Lean 4 proofs along multiple objectives (proof length, compilation cost, version compatibility) without fine-tuning. It externalizes refactoring knowledge into a densely annotated strategy bank of 9,237 unique strategies derived from 200K long–short proof pairs, with metadata tracking compile-cost reduction and Lean/Mathlib version compatibility. It achieves >70% token-level compression on competition benchmarks and up to 60% compilation-time reduction, outperforming both prior fine-tuning-based methods and Claude Code.

Problem

LLM-generated Lean proofs are correct but verbose and brittle across Lean/Mathlib version updates. Three gaps drive the work: (1) proof refactoring is inherently multi-objective—proof length and compilation cost are weakly correlated (Pearson \(r \approx 0.09\)–\(0.12\)) and frequently in tension; (2) frontier LLMs have static knowledge cutoffs that predate recent Lean/Mathlib weekly releases, causing hallucination of stale tactics; (3) fine-tuning–based refactoring pipelines require costly retraining with every new LLM or Lean release, and paired refactoring data for Lean is scarce.

Method

Strategy bank construction. Raw long–short proof pairs are sourced from NuminaMath-1.5, FineLeanCorpus, Mathlib, and ATLAS; proofs are synthesized with Goedel-Prover-V2-32B and GPT-OSS-120B. GPT-OSS-120B distills each pair into structured strategies (title, precondition, application guide, before/after example); an LLM-as-judge pipeline filters bad extractions; Qwen3-Embedding-8B clustering deduplicates semantically equivalent entries. Each strategy is annotated with (a) median compilation-time speedup, profiled via lake env lean --profile, and (b) a version-compatibility set verified by recompiling under Lean v4.14.0, v4.16.0, v4.22.0, and v4.24.0.

Retrieval model. Qwen3-Embedding-8B is fine-tuned on 639,090 (proof segment, strategy) pairs using in-batch negatives with a false-negative margin \(m\):

\[\mathcal{L} = -\frac{1}{B}\sum_{i=1}^{B} \log \frac{\exp(\text{Sim}(q_i, c_i^+)/\tau)}{\sum_{c \in \mathcal{C}_B} \mathbb{1}(q_i, c)\exp(\text{Sim}(q_i, c)/\tau)}\]

Boundary augmentation jitters segment boundaries to bridge training/inference distribution mismatch.

Objective-conditioned retrieval. At inference, the user specifies an objective; the retrieval rule is reshaped accordingly: pure cosine top-K for shortest proof; two-stage retrieve-then-rerank by annotated compile-cost reduction for compilation speed; version filtering to strategies whose compatibility set includes the target toolchain. Objectives compose (e.g., version filter stacked on compile reranking).

Agent loop. A planner LLM proposes a sequence of refactoring steps mapped to proof segments; a refactorer LLM rewrites each targeted segment; a debugger LLM repairs compile failures using Lean 4 compiler feedback for up to \(D\) rounds. The loop terminates at a budget of \(B\) LLM API calls or when proof length falls below target \(T\). All three roles are filled by any frozen frontier LLM (tested on Gemini, Claude, GPT series) with no retraining.

Key Contributions

  • Largest Lean refactoring dataset to date: >200K long–short proof pairs and 9,237 unique strategies, each annotated with compile-cost reduction and Lean/Mathlib version compatibility.
  • Multi-objective controllable refactoring at inference time via metadata-driven retrieve-and-rerank, with no model retraining required for new objectives, LLM backbones, or Lean versions.
  • State-of-the-art proof compression: >70% on competition benchmarks (miniF2F, PutnamBench, Putnam2025), >20% on research-level repositories (PFR, PhysLean, Analysis, FLT).
  • Up to 60% compilation-time reduction (Putnam2025 with reranking), versus ProofOptimizer which worsens compilation time on miniF2F (−12.89%).
  • Refactored miniF2F proofs type-check on more future Lean/Mathlib releases than unrefactored proofs, demonstrating improved version resilience.
  • Demonstrated LLM-agnosticism: Claude Code's own performance improves when given access to the strategy retrieval tool, but the full framework still outperforms it.

Results

  • miniF2F (competition): Lean Refactor 88.40% length reduction vs. ProofOptimizer 87.90%; compilation time +30.17% relative reduction vs. ProofOptimizer −12.89% (i.e., ProofOptimizer worsens compile time).
  • PutnamBench (competition): Lean Refactor 70.38% vs. ProofOptimizer 57.20%; reranking achieves 42.62% compile-time reduction vs. ProofOptimizer 21.14%.
  • Putnam2025 (competition): Lean Refactor 79.27%; reranking achieves 60.14% compile-time reduction (6.05 s absolute).
  • Research-level (Analysis/FLT/PFR/PhysLean): 17–34% length reduction with Lean Refactor vs. 8–17% for Base Agent w/o Retrieval.
  • Claude Haiku 4.5 backbone, matched budget: Lean Refactor 51.35% (PutnamBench) and 21.09% (Analysis) vs. Claude Code's best 34.91% and 10.05% (even with strategy retrieval tool added).
  • Retrieval ablation: targeted retrieval consistently outperforms random retrieval; planner removal causes persistent debug loops on long research proofs.
  • 42–67% of refactored proofs reduce external/intra-project dependencies, indicating genuine logical simplification.

Limitations

  • ProofOptimizer comparison is not backbone- or budget-matched; ProofOptimizer uses a fine-tuned 7B model with up to 6×64 + 2×1024 samples per theorem vs. Lean Refactor's 30 API calls—direct comparison conflates paradigm differences.
  • Research-level compression (20–34%) is substantially lower than competition-level (70–88%), reflecting the greater complexity of intra-project dependency networks.
  • Strategy bank must be re-profiled as new Lean/Mathlib versions ship; this is presented as an advantage but imposes ongoing maintenance overhead.
  • Version-compatibility annotation is restricted to four toolchains (v4.14.0, v4.16.0, v4.22.0, v4.24.0); generalization to versions outside this range is not verified.
  • Budget-constrained experiments (30 API calls per theorem) may understate potential performance; the framework's test-time scaling behavior is only partially reported (curves deferred to Appendix P).

Relevance to Harnesses / Meta-Harnesses

Lean Refactor is a direct instance of a plug-and-play meta-harness pattern: it wraps arbitrary frozen LLMs in a structured orchestration layer (planner → refactorer → debugger) and externalizes domain knowledge into a versioned, metadata-annotated strategy bank retrieved at inference time. The design separates the harness logic (retrieval rules, objective conditioning, agent loop termination) from both the underlying model and the evolving tool ecosystem (Lean/Mathlib), achieving what fine-tuning pipelines cannot: instant transfer to new LLM backbones and forward compatibility with new library versions by re-profiling the bank. The objective-conditioned retrieval mechanism—where the same bank serves different optimization targets by swapping only the reranking rule—demonstrates a composable control surface for multi-objective harnesses, a pattern applicable beyond formal proof to any domain where domain knowledge can be distilled into annotated, retrievable strategies. The empirical finding that even a general-purpose agent (Claude Code) improves measurably when given access to the strategy retrieval tool validates the core harness thesis: structured external knowledge retrieval lifts frozen LLMs more reliably than either model-internal knowledge or generic tool access alone.