論文の概要: Agentic Algorithm Design: LLMs that Propose, Formalise, and Prove Runtime Bounds for Evolutionary Algorithms in Lean

• arxiv url: http://arxiv.org/abs/2610.35595v2
• Date: Tue, 27 Oct 2026 06:52:27 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-28 21:04:31.364277
• Title: Agentic Algorithm Design: LLMs that Propose, Formalise, and Prove Runtime Bounds for Evolutionary Algorithms in Lean
• Title（参考訳）: Agentic Algorithm Design: リーンにおける進化的アルゴリズムのための実行時境界の提案、形式化、証明を行うLLM
• Abstract要約: 本稿では,進化的アルゴリズムの設計と解析における研究手法に倣ってモデル化されたパイプラインについて述べる。 エージェントはブラックボックス最適化アルゴリズムを提案し、Leanガードは欠陥のある設計をフィルタリングする。 パイプラインはまた、整数値のサブモジュラー最小化のためのブラックボックス最適化アルゴリズムを設計し、解析する。
• 参考スコア（独自算出の注目度）: 7.716156977428554
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: LLMs now prove hard theorems in Lean. Can they also design algorithms and prove their correctness and efficiency? LLM-guided design of optimisation heuristics (such as AlphaEvolve) is purely empirical. Automated theorem provers with LLMs prove given statements. So far, there has been little evidence that LLMs can do both: design an algorithm and guarantee its efficiency by a mathematical proof. We present a staged pipeline modelled after research methodology in design and analysis of evolutionary algorithms. The agent proposes black-box optimisation algorithms, and Lean guards filter out flawed designs. The agent then defines a potential function and proves drift bounds that guarantee an expected runtime improvement over the baseline algorithm. At no point in the pipeline are the algorithms compared empirically. The agent generates a black-box optimisation algorithm with expected runtime $O(n^2)$ on a CycleUncover problem, where the classical (1+1) EA needs runtime $e^{Ω(n)}$. The pipeline also designs and analyses a black-box optimisation algorithm for integer-valued submodular minimisation with expected runtime $O(n^{2+2c})$, and it matches the classical runtime $O(n^2)$ on LeadingOnes. Across 8 problem classes, 12 of 15 runs with frontier models complete the pipeline with a machine-checked expected-runtime bound. An ablation study shows that removing the staging and asking the agent to zero-shot an algorithmic design with a runtime guarantee leads to a copy of the seeded baseline algorithm (random search) or to incomplete proofs. Our study suggests that machine-checked specifications in Lean can replace empirical evaluation in open-ended algorithm discovery. To the best of our knowledge, this is the first example of an automated pipeline that designs efficient black-box optimisation algorithms with machine-checked runtime bounds in Lean.
• Abstract（参考訳）: LLMはリーンで難しい定理を証明します。 また、アルゴリズムを設計し、その正確さと効率性を証明できますか? 最適化ヒューリスティック(AlphaEvolveなど)のLLM誘導設計は純粋に経験的である。 LLMを用いた自動定理証明器は与えられた言明を証明する。 LLMはアルゴリズムを設計し、その効率を数学的証明によって保証する。 本稿では,進化的アルゴリズムの設計と解析における研究手法に倣ってモデル化されたパイプラインについて述べる。 エージェントはブラックボックス最適化アルゴリズムを提案し、Leanガードは欠陥のある設計をフィルタリングする。 次にエージェントはポテンシャル関数を定義し、ベースラインアルゴリズムよりも期待されるランタイム改善を保証するドリフトバウンダリを証明します。 パイプラインのどの点でも、アルゴリズムは経験的に比較される。 エージェントは、期待されるランタイム$O(n^2)$でブラックボックス最適化アルゴリズムを生成し、古典的な (1+1) EA はランタイム $e^{Ω(n)}$ を必要とする。 パイプラインはまた、整数値のサブモジュール最小化のためのブラックボックス最適化アルゴリズムを、期待されるランタイム$O(n^{2+2c})$で設計し分析し、古典的なランタイム$O(n^2)$ on LeadingOnesと一致する。 8つの問題クラスで15のうち12がフロンティアモデルで実行され、マシンチェックされた予測実行バウンダリでパイプラインが完了する。 アブレーション研究では、エージェントがステージングを除去し、実行時保証付きアルゴリズム設計をゼロショットするよう要求すると、シードされたベースラインアルゴリズム(ランダム検索)のコピーや不完全証明が導かれる。 我々の研究は、リーンにおけるマシンチェックされた仕様は、オープンなアルゴリズム発見における経験的評価を置き換えることができることを示唆している。 私たちの知る限りでは、これはリーンでマシンチェックされたランタイム境界を持つ効率的なブラックボックス最適化アルゴリズムを設計する自動化パイプラインの最初の例です。

関連論文リスト

• LLMs Can Design Near-Optimal OR Algorithms [2.0813318162800702]
  大規模言語モデル(LLM)は、よく特定された操作研究(OR)問題に対して効果的なアルゴリズムを設計することができる。 本稿では,在庫管理,待ち行列ネットワーク制御,アソート最適化について検討する。
  論文  参考訳（メタデータ） (2026-08-27T16:01:11Z)
• Budget-Efficient Automatic Algorithm Design via Code Graph [2.982218441172364]
  大規模言語モデル(LLM)は自動アルゴリズム設計(AAD)のための強力なツールとして登場した。 我々は予算効率のよい自動アルゴリズム設計を定式化し、検索ポリシーは計算コストに制限のある実現された適合性を最大化する。 提案手法を3つの最適化問題に対して実証的に検証し,同じトークン予算で全アルゴリズム探索よりもグラフ検索の方が一貫した優位性を示す。
  論文  参考訳（メタデータ） (2026-05-11T14:01:52Z)
• When Switching Algorithms Helps: A Theoretical Study of Online Algorithm Selection [0.15469452301122175]
  オンラインセレクション(OAS)は、フィットネスのランドスケープの変化に最適化プロセスを適用することを目的としており、特定のポートフォリオから任意のアルゴリズムを上回ることが期待されている。 現在、OASがスピードアップを達成できるという理論的な結果は得られていない。 本稿では,2つのアルゴリズムの切り換えが,それぞれのアルゴリズムの分離よりも問題的に高速であることを示す最初の理論的例を示す。
  論文  参考訳（メタデータ） (2026-04-08T18:11:36Z)
• $\nabla$-Reasoner: LLM Reasoning via Test-Time Gradient Descent in Latent Space [71.23672814629448]
  $nabla$-Reasonerは、トークンログに対する差別化可能な最適化をデコードループに統合する反復生成フレームワークである。 $nabla$-Reasonerは、挑戦的な数学的推論ベンチマークで20%以上の精度の向上を実現している。
  論文  参考訳（メタデータ） (2026-03-05T08:42:54Z)
• Provable Scaling Laws for the Test-Time Compute of Large Language Models [84.00141420901038]
  本研究では,大規模言語モデルのテスト時間計算において,証明可能なスケーリング法則を享受する2つのアルゴリズムを提案する。 1つは2段階ノックアウト方式のアルゴリズムで、各候補は複数の相手に対して平均勝利率で評価される。 もう1つは2段階のリーグ方式のアルゴリズムで、各候補は複数の相手に対して平均勝利率で評価される。
  論文  参考訳（メタデータ） (2024-11-29T05:29:47Z)
• Choosing the Right Algorithm With Hints From Complexity Theory [16.33500498939925]
  我々は,メトロポリスのアルゴリズムが,合理的な問題サイズを考慮に入れた全てのアルゴリズムの中で,明らかに最良のものであることを示す。 このタイプの人工アルゴリズムは、$O(n log n)$ランタイムを持つので、重要度に基づくコンパクト遺伝的アルゴリズム(sig-cGA)は、高い確率で、DLB問題を解くことができる。
  論文  参考訳（メタデータ） (2021-09-14T11:12:32Z)

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

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