Lean-рефакторинг: многоцелевая управляемая оптимизация доказательств посредством агентного поиска стратегий

Аннотация

Мы представляем Lean Refactor — подключаемый агентный фреймворк с дополнением извлечениями для многоцелевого, управляемого и устойчивого к версиям рефакторинга Lean-доказательств. Доказательства, сгенерированные LLM, как известно, являются корректными, но многословными и хрупкими при смене версий библиотек, однако существующие работы по рефакторингу упускают из виду три практические проблемы: 1) рефакторинг Lean по своей сути многоцелевой (длина доказательства, стоимость компиляции и совместимость версий часто находятся в противоречии); 2) репозитории Lean обладают хрупкой совместимостью, в то время как выпуски LLM не учитывают версии Lean/Mathlib; 3) конвейеры на основе обучения требуют повторной тонкой настройки при каждом новом выпуске LLM, не масштабируясь ни при смене моделей, ни в цикле выпуска Lean. Lean Refactor управляет замороженным агентным LLM с помощью извлечений из кураторской базы данных многоцелевых стратегий рефакторинга, каждая из которых плотно аннотирована метаданными, такими как поддерживаемые версии Lean/Mathlib и ожидаемое снижение стоимости компиляции. Эксперименты показывают сжатие на уровне токенов более 70% на бенчмарках соревнований, более 20% на исследовательских репозиториях и сокращение времени компиляции до 60%, что превосходит предыдущие работы и Claude Code. Извлечение с фильтрацией по версии дополнительно улучшает сжатие для целевой версии Lean, а рефакторизованные доказательства miniF2F демонстрируют более сильный нулевой перенос версий на будущие выпуски Lean по сравнению с их нерефакторизованными аналогами.

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.