論文の概要: Verified Learning for Compiler Optimization: An LLM-Guided Architecture with Formal Control

• arxiv url: http://arxiv.org/abs/2609.27214v1
• Date: Wed, 23 Sep 2026 01:22:34 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-25 00:05:17.818253
• Title: Verified Learning for Compiler Optimization: An LLM-Guided Architecture with Formal Control
• Title（参考訳）: コンパイラ最適化のための検証学習:形式制御によるLLMガイドアーキテクチャ
• Abstract要約: 検証中心のシステムアーキテクチャを用いて,大規模言語モデルがコンパイラ最適化に参加することができるかどうかを検討する。 Wyvernが生成した変換にコード中心のLLMを微調整し、Alive2をフィードバックループに埋め込んで、生成されたリライト毎にセマンティックな保存を強制します。 ほとんどのベンチマークではWyvernは高速だが、9.8%は学習システムの下で同等あるいは改善されたランタイムを実現しており、意味的な違反は観測されていない。
• 参考スコア（独自算出の注目度）: 1.3682073278404534
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Compiler optimizations traditionally rely on handcrafted heuristics that often fail to generalize across programs and architectures. We investigate whether large language models can participate in compiler optimization through a verification-centered systems architecture that couples generative rewriting with formal equivalence checking. Using lazification in LLVM IR as a case study, we fine-tune a code-centric LLM on transformations produced by Wyvern and embed Alive2 into a feedback loop that enforces semantic preservation for every generated rewrite. Correctness is enforced externally as a runtime control layer rather than learned implicitly. During inference, candidate transformations are symbolically validated and regenerated when necessary, ensuring accepted rewrites satisfy formal constraints. On the LLVM test suite, the fine-tuned model reproduces core optimization behaviors while applying fewer transformations overall. Although Wyvern remains faster on most benchmarks, 9.8% achieve comparable or improved runtime under the learned system, with no semantic violations observed. Verification overhead remains bounded and convergence stable. These results demonstrate that generative AI components can be safely integrated into compiler pipelines through deterministic validation and structured feedback, offering a scalable architectural pattern for trustworthy AI-driven software infrastructure.
• Abstract（参考訳）: コンパイラの最適化は伝統的に手作りのヒューリスティックに依存しており、プログラムやアーキテクチャをまたいだ一般化に失敗することが多い。 生成的書き換えと形式的等価性チェックを結合した検証中心のシステムアーキテクチャにより,大規模言語モデルがコンパイラ最適化に参加することができるかどうかを検討する。 LLVM IRのラジフィケーションをケーススタディとして、Wyvernが生成した変換にコード中心のLLMを微調整し、Alive2をフィードバックループに組み込み、生成されたリライト毎にセマンティックな保存を強制する。 正確性は暗黙的に学習するのではなく、ランタイムコントロール層として外部的に強制される。 推論中、候補変換は記号的に検証され、必要に応じて再生され、受け入れられた書き換えが形式的な制約を満たすことが保証される。 LLVMテストスイートでは、微調整されたモデルがコア最適化の振る舞いを再現すると同時に、全体的な変換を少なくする。 ほとんどのベンチマークではWyvernの方が高速だが、9.8%は学習システムの下で同等あるいは改善されたランタイムを実現しており、意味的な違反は観測されていない。 検証オーバーヘッドは有界であり、収束は安定である。 これらの結果は、決定論的検証と構造化されたフィードバックを通じて、生成可能なAIコンポーネントをコンパイラパイプラインに安全に統合できることを示し、信頼できるAI駆動ソフトウェアインフラストラクチャのためのスケーラブルなアーキテクチャパターンを提供する。

関連論文リスト

• AutoVecCoder: Teaching LLMs to Generate Explicitly Vectorized Code [69.84692701646769]
  AutoVecCoderは、大規模言語モデルに自動明示的ベクトル化機能を持たせるために設計された新しいフレームワークである。 自動データ合成パイプラインであるVecPromptは、ドメイン固有の固有の知識を注入する。 強化学習フレームワークであるVecRLは、コード生成と実行効率を一致させる。 このフレームワークでトレーニングされたAutoVecCoder-8Bは、SimdBenchのSSEおよびAVXサブセット上で最先端のパフォーマンスを達成する。
  論文  参考訳（メタデータ） (2026-05-18T07:33:15Z)
• LLM Translation of Compiler Intermediate Representation [2.614444430580024]
  本稿では,GIMPLE を LLVM IR に変換するための変換器モデル IRIS-14B を提案する。 我々の知る限りでは、IRIS-14BはIR-to-IR翻訳のために明示的に訓練された最初のモデルである。 現在入手可能な最先端のオープンモデルを含む、広く使われているモデルの精度は、13～1000億のパラメータから44ポイントまで向上している。
  論文  参考訳（メタデータ） (2026-05-07T13:22:23Z)
• Understanding by Reconstruction: Reversing the Software Development Process for LLM Pretraining [66.89012795621349]
  大規模言語モデル(LLM)は、複雑なソフトウェア工学に必要な、深く、長期にわたる推論に苦しむことが多い。 本稿では,再構築による理解という,新しいパラダイムを提案する。 マルチエージェントシミュレーションを用いて潜在エージェント軌道を合成するフレームワークを提案する。
  論文  参考訳（メタデータ） (2026-03-11T09:23:20Z)
• Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
  LLM推論を改善するための実用的な方法として、推論時計算が再導入されている。 テスト時間スケーリング(TTS)アルゴリズムの多くは、自動回帰デコーディングに依存している。 そこで我々は,dLLM のための効率的な TTS フレームワーク Prism を提案する。
  論文  参考訳（メタデータ） (2026-02-02T09:14:51Z)
• Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
  シリコングレードの正しさは、 (i) シミュレーション中心の評価の限られたカバレッジと信頼性、 (ii) 回帰と修復幻覚、 (iii) エージェントハンドオフ間で意図が再解釈される意味的ドリフトによってボトルネックが残っている。 エージェントの意図を整合させる設計契約を確立するマルチエージェントフレームワークであるVeri-Sureを提案する。
  論文  参考訳（メタデータ） (2026-01-27T16:10:23Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• REASONING COMPILER: LLM-Guided Optimizations for Efficient Model Serving [6.19179006129561]
  本稿では,逐次的かつコンテキスト対応な意思決定プロセスとして最適化を定式化する,新しいコンパイルフレームワーク(Dubbed Reasoning)を提案する。 提案手法は,LLM誘導推論がコンパイラ最適化のランドスケープを変革する可能性を示す。
  論文  参考訳（メタデータ） (2025-06-02T07:02:46Z)
• SymRTLO: Enhancing RTL Code Optimization with LLMs and Neuron-Inspired Symbolic Reasoning [30.938876549335067]
  本稿では,新しいニューロン-シンボリックRTL最適化フレームワークであるSymRTLOを提案する。 有限状態機械(FSM)論理の解析と最適化のための記号モジュールを提案する。 Synopsys Design Compiler と Yosys による RTL-Rewriter ベンチマークの実験では、SymRTLO は 43.9% と 62.5% と 51.1% に向上している。
  論文  参考訳（メタデータ） (2025-04-14T16:15:55Z)
• COrAL: Order-Agnostic Language Modeling for Efficient Iterative Refinement [80.18490952057125]
  反復改良は、複雑なタスクにおける大規模言語モデル(LLM)の能力を高める効果的なパラダイムとして登場した。 我々はこれらの課題を克服するために、コンテキストワイズ順序非依存言語モデリング(COrAL)を提案する。 当社のアプローチでは、管理可能なコンテキストウィンドウ内で複数のトークン依存関係をモデル化しています。
  論文  参考訳（メタデータ） (2024-10-12T23:56:19Z)

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

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