論文の概要: Agentic Verified Optimization of Real-World Software

• arxiv url: http://arxiv.org/abs/2610.30188v1
• Date: Tue, 20 Oct 2026 17:33:22 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-24 02:08:44.080482
• Title: Agentic Verified Optimization of Real-World Software
• Title（参考訳）: 実世界のソフトウェアにおけるエージェント検証最適化
• Abstract要約: コーディングエージェントは、アルゴリズム、データ構造、実行戦略を変更することで、プログラムを高速にすることができる。 本稿では,エージェントが既存のエージェントと等価性を示すマシンチェックとともに,より高速な実装を実現するエージェント検証最適化を提案する。 既存の実装が仕様として機能するため、そのタスクは検証済みコード生成の仕様記述ボトルネックを避ける。
• 参考スコア（独自算出の注目度）: 48.200692884947216
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Program optimization aims to improve performance while preserving behavior. Coding agents can already make programs faster by changing algorithms, data structures, and execution strategies. However, existing equivalence checks mostly rely on tests, which agents have been shown to exploit, passing the tests without preserving the intended behavior. We propose agentic verified optimization, in which an agent produces a faster implementation together with a machine-checked proof of equivalence to the existing one. Because the existing implementation serves as the specification, the task avoids the specification-writing bottleneck of verified code generation, and recent advances in theorem proving make the proofs attainable. We formulate the task at the function and repository levels in Lean 4, where programs can be both executed and reasoned about. Few real-world applications are written in Lean, so we develop Aqueduct, an agentic framework that migrates C, C++, Go, and Rust programs into native Lean, validates each port by differential testing against its original. On the 189 reference implementations in Verina, agents produce faster proved rewrites for 156, including algorithmic changes such as replacing exponential recursion with dynamic programming. On 17 migrated applications, their 92 proved rewrites speed up 47 of 51 application scenarios. These application-level gains are smaller than the function-level ones, making the choice of functions to optimize an important problem. Current agents can thus already carry out verified optimization on both standalone functions and applications migrated from real programs. We discuss the remaining challenges and the steps toward verified optimization in production.
• Abstract（参考訳）: プログラム最適化は、動作を保ちながらパフォーマンスを改善することを目的としている。 コーディングエージェントは、アルゴリズム、データ構造、実行戦略を変更することで、プログラムを高速にすることができる。 しかし、既存の等価チェックは主にテストに依存しており、エージェントが悪用されることが示され、意図した振る舞いを保たずにテストに合格する。 本稿では,エージェントが既存のエージェントと等価性を示すマシンチェックとともに,より高速な実装を実現するエージェント検証最適化を提案する。 既存の実装が仕様として機能するため、そのタスクは検証済みコード生成の仕様記述ボトルネックを回避し、最近の定理証明の進歩によって証明が達成できる。 プログラムの実行と推論の両方が可能なLean 4の関数レベルとリポジトリレベルのタスクを定式化します。 C、C++、Go、RustのプログラムをネイティブのLeanに移行するエージェントフレームワークであるAqueductは、オリジナルのものとの差分テストによって各ポートを検証する。 Verinaの189の参照実装では、エージェントは指数的再帰を動的プログラミングに置き換えるなどのアルゴリズム的な変更を含む、156の高速に証明された書き換えを生成する。 17の移行アプリケーションでは、92のリライトによって51のアプリケーションシナリオのうち47が高速化された。 これらのアプリケーションレベルのゲインは関数レベルのゲインよりも小さく、重要な問題を最適化する関数を選択する。 したがって、現在のエージェントは、実際のプログラムから移行したスタンドアロン関数とアプリケーションの両方に対して、すでに検証済みの最適化を実行することができる。 本研究は,本運用における検証最適化に向けた残りの課題とステップについて論じる。

関連論文リスト

• Is manual software optimization a thing of the past? [0.0]
  本研究では,大規模言語モデルが科学ソフトウェアの性能向上を自律的に達成できるかどうかを考察する。 我々は3つの計算問題に対してソフトウェアを最適化するLLMエージェントを課題とした。 改良には低レベルのコード最適化、数学的修正、グラフレットカウントのための全く新しいアルゴリズムが含まれていた。
  論文  参考訳（メタデータ） (2026-09-29T15:42:17Z)
• The Optimizer Is the Agent: Reasoning-Driven Search across Prompts, Programs, and ML Workflows [72.9051182568928]
  推論駆動最適化のための統合フレームワークであるReASearchを提案する。 共有エージェントループとドメイン固有のツールにより、ReASearchは、プロンプト、プログラム、MLを最適化するために、まったく同じスキャフォールドをインスタンス化する。 我々は,複雑な探索行動がエージェントの推論プロセスから自然に現れることを観察する。
  論文  参考訳（メタデータ） (2026-08-07T02:15:39Z)
• TTHE: Test-Time Harness Evolution [50.26245555541721]
  既存のアプローチでは、デプロイ前、トレーニング前、あるいはテスト時に凍結される固定されたエージェントワークフローの開発データを最適化する。 我々は、エージェントがテスト入力で生成するラベルのない実行トレースのみを使用して、評価自体にハーネスを最適化できるかどうかを問う。 評価中、TTHEは候補ハーネスの人口を維持し、それらの実行トレースの理由をエージェントプロジェクタを通じてそれらを洗練する。 その後、審査員は実行元プロキシ信号から改善されたハーネスをコミットし、選択したプログラムは継続してその後の入力を統治する。
  論文  参考訳（メタデータ） (2026-07-09T05:53:39Z)
• PERFOPT-Bench: Evaluating Coding Agents on Software Performance Optimization [18.924749191192433]
  パフォーマンスの最適化は独特なエージェント的タスクである。 本稿では,このフルパフォーマンス・エンジニアリング・ループを評価するベンチマークであるPERFOPT-Benchを紹介する。
  論文  参考訳（メタデータ） (2026-07-08T08:32:18Z)
• AdaExplore: Failure-Driven Adaptation and Diversity-Preserving Search for Efficient Kernel Generation [59.964989458924585]
  AdaExploreは、パフォーマンスクリティカルなカーネルコード生成のための蓄積された実行フィードバックによる自己改善を可能にするエージェントフレームワークである。 適応段階では、エージェントはタスクを合成し、繰り返し発生する障害を有効ルールの再利用可能なメモリに変換する。 探索段階では、候補核を木として整理し、小さな局所精製とより大きな構造再生を交互に行う。
  論文  参考訳（メタデータ） (2026-04-17T18:25:03Z)
• Agent-GWO: Collaborative Agents for Dynamic Prompt Optimization in Large Language Models [69.55139736609367]
  Agent-GWOは複雑な推論のための動的プロンプト最適化フレームワークである。 本稿では,Agent-GWOが既存のプロンプト最適化手法よりも精度と安定性を一貫して向上することを示す。
  論文  参考訳（メタデータ） (2026-04-14T07:35:37Z)
• WybeCoder: Verified Imperative Code Generation [22.401681809856896]
  WybeCoderはエージェントコード検証フレームワークである。 コード、不変性、そして証明が共進化する所で、証明・アズ・ユー・ジェネレーション開発を可能にする。
  論文  参考訳（メタデータ） (2026-03-31T00:06:44Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• SWE-fficiency: Can Language Models Optimize Real-World Repositories on Real Workloads? [22.075705411944895]
  SWE-fficiencyは、実際のワークロードにおけるリポジトリレベルのパフォーマンス最適化を評価するためのベンチマークである。 私たちのスイートには、9つの広く使用されているデータサイエンス、機械学習、HPCリポジトリにわたる498のタスクが含まれています。
  論文  参考訳（メタデータ） (2025-11-08T17:55:09Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。