論文の概要: Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
- arxiv url: http://arxiv.org/abs/2605.20244v1
- Date: Mon, 18 May 2026 04:19:41 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-21 19:19:56.229236
- Title: Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
- Title（参考訳）: Lean Refactor: エージェント戦略検索による多目的制御可能な証明最適化
- Abstract要約: Lean Refactor(リンク)は、Lean proofs(リンク)のための検索強化エージェントフレームワークである。
Lean Refactorは、Lean/Mathlibバージョンをサポートするメタデータをアノテートしたフリーズされたエージェント検索を操縦する。
実験では、競合ベンチマークで70%以上のトークンレベルの圧縮、研究リポジトリで20%以上の圧縮、コンパイル時間の最大60%の削減が示されている。
- 参考スコア（独自算出の注目度）: 42.21181713802239
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: 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.
- Abstract（参考訳）: Lean Refactor(リンク)は、多目的、制御可能、そして、Leanの証明のバージョンロバストリファクタリングのための、プラグ&プレイで検索可能なエージェントフレームワークです。
LLMの生成した証明は、ライブラリバージョンにまたがって正確だが、既存のリファクタリングは、3つの実践的な課題を見落としている。
1) リーンリファクタリングは本質的に多目的(長さ、コンパイルコスト、バージョン互換性は緊張することが多い)です。
2) リーンリポジトリには脆弱な互換性があるのに対して、LLMリリースはリーン/マドリブのバージョンに気づいていない。
3) トレーニングベースのパイプラインは、新しいLCMリリース毎に繰り返し微調整を必要とします。
リーンリファクタリング(Lean Refactor)は、多目的リファクタリング戦略のキュレートされたデータベースから取得したフリーズエージェント LLM を操り、それぞれがサポート対象のLean/Mathlibバージョンやコンパイルコストの削減といったメタデータを密接なアノテーションでアノテートする。
実験では、コンペティションベンチマークで70ドル以上、研究リポジトリで20ドル以上、コンパイル時間の短縮で60ドル以上、事前の作業とClaude Codeを上回っている。
バージョンフィルタリング検索は、ターゲットのLeanバージョンに対する圧縮をさらに改善し、リファクタリングされたminiF2F証明は、リファクタリングされていないバージョンよりも、将来のLeanリリースへのゼロショットバージョン転送を強く示す。
関連論文リスト
- RefactorAssist: Agentic Refinement for Reliable Code Refactoring [0.3657314044338856]
大規模言語モデル(LLM)は、ソフトウェア工学のタスクを自動化する可能性を実証している。
LLMは、しばしば微妙なエラーを導入し、機能的な振る舞いの変化やユニットテストの失敗につながる。
LLM生成物の機能的正しさを向上させるためにRefactorAssistエージェントを開発した。
論文 参考訳（メタデータ） (2026-08-02T01:32:22Z) - From Restructuring to Stabilization: A Large-Scale Experiment on Iterative Code Readability Refactoring with Large Language Models [5.31828955342405]
大規模言語モデル(LLM)は、自動化されたコードタスクにますます使われています。
この記事では、コード可読性のためのLLMの能力を体系的に研究する。
論文 参考訳（メタデータ） (2026-02-25T12:05:25Z) - DiffuRank: Effective Document Reranking with Diffusion Language Models [71.16830004674513]
拡散言語モデル(dLLM)に基づいて構築されたフレームワークであるDiffuRankを提案する。
dLLMは、左から右への順序に制約されないより柔軟なデコーディングと生成プロセスをサポートする。
モデルサイズが類似した自己回帰LDMに匹敵する性能を示す。
論文 参考訳（メタデータ） (2026-02-13T02:18:14Z) - SWE-Refactor: A Repository-Level Benchmark for Real-World LLM-Based Code Refactoring [20.694251041823097]
大規模言語モデル(LLM)は、ソフトウェア工学のタスクに取り組むことに広く関心を集めている。
既存のベンチマークは一般的に3つの欠点に悩まされる。
SWE-Refactor は開発者によって書かれた 18 の Java プロジェクトから抽出された 1,099 の挙動保存 LLM で構成されている。
論文 参考訳（メタデータ） (2026-02-03T16:36:29Z) - AlignCoder: Aligning Retrieval with Target Intent for Repository-Level Code Completion [55.21541958868449]
リポジトリレベルのコード補完フレームワークであるAlignCoderを提案する。
我々のフレームワークは、初期クエリとターゲットコードのセマンティックギャップを橋渡しする拡張クエリを生成する。
我々は、拡張クエリにおける推論情報を活用してより正確な検索を行うAlignRetrieverのトレーニングに強化学習を採用する。
論文 参考訳（メタデータ） (2026-01-27T15:23:14Z) - Refactoring Codebases through Library Design [21.039476331720312]
成長と再利用性をサポートする方法でコードに対するコードエージェントの能力を調べる。
本稿では,再利用可能なライブラリを生成するためのベンチマークと手法を提案する。
我々は,ライブラリと最先端のライブラリ生成手法を比較し,それを実世界のコードベースで研究する。
論文 参考訳（メタデータ） (2025-05-26T07:26:33Z) - StepCoder: Improve Code Generation with Reinforcement Learning from
Compiler Feedback [58.20547418182074]
2つの主要コンポーネントからなるコード生成の新しいフレームワークであるStepCoderを紹介します。
CCCSは、長いシーケンスのコード生成タスクをCurriculum of Code Completion Subtaskに分割することで、探索課題に対処する。
FGOは、未実行のコードセグメントをマスクすることでのみモデルを最適化し、Fine-Grained Optimizationを提供する。
提案手法は,出力空間を探索し,対応するベンチマークにおいて最先端の手法より優れた性能を発揮する。
論文 参考訳（メタデータ） (2024-02-02T13:14:31Z) - LLMRefine: Pinpointing and Refining Large Language Models via Fine-Grained Actionable Feedback [65.84061725174269]
最近の大規模言語モデル(LLM)は、世代品質を改善するために人間のフィードバックを活用している。
LLMの出力を最適化する推論時間最適化手法であるLLMRefineを提案する。
機械翻訳、長文質問応答(QA)、話題要約を含む3つのテキスト生成タスクについて実験を行った。
LLMRefineは、すべてのベースラインアプローチを一貫して上回り、翻訳タスクの1.7 MetricXポイント、ASQAの8.1 ROUGE-L、トピックの要約の2.2 ROUGE-Lの改善を実現している。
論文 参考訳（メタデータ） (2023-11-15T19:52:11Z) - LLatrieval: LLM-Verified Retrieval for Verifiable Generation [67.93134176912477]
検証可能な生成は、大きな言語モデル(LLM)がドキュメントをサポートするテキストを生成することを目的としている。
本稿では,LLatrieval (Large Language Model Verified Retrieval)を提案する。
実験により、LLatrievalは幅広いベースラインを著しく上回り、最先端の結果が得られることが示された。
論文 参考訳（メタデータ） (2023-11-14T01:38:02Z) - Coarse-Tuning Models of Code with Reinforcement Learning Feedback [0.0]
コード上で事前訓練されたLarge Language Models (LLM) が、プログラム合成の主流のアプローチとして登場した。
コードの品質を評価する接地関数からのフィードバックを用いて、強化学習により事前学習したLLMをさらに訓練するRCCFを提案する。
論文 参考訳（メタデータ） (2023-05-25T22:09:08Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。