Lean Refactor: Mehrzieloptimierung kontrollierbarer Beweise durch agentische Strategiensuche

Zusammenfassung

Wir präsentieren Lean Refactor, ein Plug-and-Play-retrievalgestütztes agentisches Framework für multiobjektive, steuerbare und versionsrobuste Refaktorisierung von Lean-Beweisen. Von LLMs generierte Beweise sind bekanntermaßen zwar korrekt, aber ausführlich und über Bibliotheksversionen hinweg zerbrechlich, während bestehende Refaktorisierungsarbeiten drei praktische Herausforderungen übersehen: 1) Lean-Refaktorisierung ist inhärent multiobjektiv (Beweislänge, Kompilierungskosten und Versionskompatibilität stehen oft im Widerspruch); 2) Lean-Repositorien haben eine fragile Kompatibilität, wohingegen LLM-Veröffentlichungen nichts über Lean-/Mathlib-Versionen wissen; 3) Trainingsbasierte Pipelines erfordern wiederholte Feinabstimmung mit jeder neuen LLM-Version und skalieren weder mit dem Modellwechsel noch mit dem Veröffentlichungszyklus von Lean. Lean Refactor steuert ein eingefrorenes agentisches LLM mit Abfragen aus einer kuratierten Datenbank multiobjektiver Refaktorisierungsstrategien, die jeweils dicht mit Metadaten wie unterstützten Lean-/Mathlib-Versionen und erwarteter Reduzierung der Kompilierungskosten annotiert sind. Experimente zeigen über 70 % Token-Kompression bei Wettbewerbs-Benchmarks, über 20 % bei Forschungsrepositorien und bis zu 60 % Reduzierung der Kompilierungszeit und übertreffen damit frühere Arbeiten und Claude Code. Versionsgefiltertes Retrieval verbessert die Kompression auf die Ziel-Lean-Version weiter, und refaktorisierte miniF2F-Beweise weisen einen stärkeren Zero-Shot-Versionstransfer auf zukünftige Lean-Versionen auf als ihre nicht refaktorisierten Gegenstücke.

English

We present Lean Refactor, a plug-and-play retrieval-augmented agentic framework for multi-objective, controllable, and version-robust refactoring of Lean proofs. LLM-generated proofs are notoriously correct-but-verbose and brittle across library versions, yet existing refactoring works overlook three practical challenges: 1) Lean refactoring is natively multi-objective (proof length, compilation cost, and version compatibility are often in tension); 2) Lean repositories have fragile compatibility, whereas LLM releases are unaware of Lean/Mathlib versions; 3) Training-based pipelines require repeated fine-tuning with each new LLM release, scaling neither with model churn nor with Lean's release cycle. Lean Refactor steers a frozen agentic LLM with retrievals from a curated database of multi-objective refactoring strategies, each densely annotated with metadata such as supported Lean/Mathlib versions and expected compilation-cost reduction. Experiments show over 70% token-level compression on competition benchmarks, over 20% on research repositories, and up to 60% compilation-time reduction, outperforming prior work and Claude Code. Version-filtered retrieval further improves compression on the target Lean version, and refactored miniF2F proofs exhibit stronger zero-shot version transfer to future Lean releases than their unrefactored counterparts.