論文の概要: Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers

• arxiv url: http://arxiv.org/abs/2508.00419v1
• Date: Fri, 01 Aug 2025 08:15:15 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-08-04 18:08:53.795505
• Title: Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers
• Title（参考訳）: ループ不変量生成:最適化LLMとSMT解のハイブリッドフレームワーク
• Authors: Varun Bharti, Shashwat Jha, Dhruv Kumar, Pankaj Jalote,
• Abstract要約: 現代, 推論に最適化された大規模言語モデルが, シンボリックアプローチよりも優れているかどうかを考察する。 OpenAIのO1、O1-mini、O3-miniを、Z3 SMTソルバと密結合した生成とチェックのパイプラインに統合します。 私たちのフレームワークは、100%のカバレッジ(133のうち133)を達成し、133のうち107よりも優れています。
• 参考スコア（独自算出の注目度）: 2.0686733932673604
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Loop invariants are essential for proving the correctness of programs with loops. Developing loop invariants is challenging, and fully automatic synthesis cannot be guaranteed for arbitrary programs. Some approaches have been proposed to synthesize loop invariants using symbolic techniques and more recently using neural approaches. These approaches are able to correctly synthesize loop invariants only for subsets of standard benchmarks. In this work, we investigate whether modern, reasoning-optimized large language models can do better. We integrate OpenAI's O1, O1-mini, and O3-mini into a tightly coupled generate-and-check pipeline with the Z3 SMT solver, using solver counterexamples to iteratively guide invariant refinement. We use Code2Inv benchmark, which provides C programs along with their formal preconditions and postconditions. On this benchmark of 133 tasks, our framework achieves 100% coverage (133 out of 133), outperforming the previous best of 107 out of 133, while requiring only 1-2 model proposals per instance and 14-55 seconds of wall-clock time. These results demonstrate that LLMs possess latent logical reasoning capabilities which can help automate loop invariant synthesis. While our experiments target C-specific programs, this approach should be generalizable to other imperative languages.
• Abstract（参考訳）: ループ不変量はループを持つプログラムの正しさを証明するのに不可欠である。 ループ不変性の開発は困難であり、任意のプログラムに対して完全自動合成は保証できない。 記号的手法を用いてループ不変量を合成する手法が提案されており、最近ではニューラルアプローチも提案されている。 これらのアプローチは、標準ベンチマークのサブセットに対してのみループ不変量を正しく合成することができる。 本研究では,現代的推論に最適化された大規模言語モデルが,よりよく機能するかどうかを考察する。 我々はOpenAIのO1、O1-mini、O3-miniをZ3 SMTソルバと密結合した生成・チェックパイプラインに統合し、ソルバの反例を用いて不変の洗練を反復的に導く。 私たちはCode2Invベンチマークを使用し、Cプログラムに正式な事前条件と後条件を提供します。 この133タスクのベンチマークでは、我々のフレームワークは100%のカバレッジ(133のうち133)を達成し、1インスタンスあたり1-2モデルの提案と14-55秒のウォールクロック時間しか必要とせず、133のうち107よりも優れています。 これらの結果から,LLMはループ不変合成の自動化に役立つ潜在論理的推論能力を有することが示された。 実験では,C言語固有のプログラムを対象としているが,他の命令型言語にも適用可能である。

関連論文リスト

• SymRTLO: Enhancing RTL Code Optimization with LLMs and Neuron-Inspired Symbolic Reasoning [18.40402135952776]
  本稿では,新しいニューロン-シンボリックRTL最適化フレームワークであるSymRTLOを提案する。 有限状態機械(FSM)論理の解析と最適化のための記号モジュールを提案する。 Synopsys Design Compiler と Yosys による RTL-Rewriter ベンチマークの実験では、SymRTLO は 43.9% と 62.5% と 51.1% に向上している。
  論文  参考訳（メタデータ） (2025-04-14T16:15:55Z)
• Sample, Don't Search: Rethinking Test-Time Alignment for Language Models [55.2480439325792]
  新しいテストタイムアライメントアプローチであるQAlignを紹介します。 テスト時間計算をスケールする際、QAlignは各プロンプトの最適配向分布からのサンプリングに収束する。 マルコフ連鎖モンテカルロのテキスト生成における最近の進歩を取り入れることで、基礎となるモデルを変更したり、ロジットアクセスを必要とせずに、より良い整合出力を可能にする。
  論文  参考訳（メタデータ） (2025-04-04T00:41:40Z)
• Fully Autonomous Programming using Iterative Multi-Agent Debugging with Large Language Models [8.70160958177614]
  大言語モデル(LLM)を用いたプログラム合成は「ニアミス症候群」に苦しむ 我々は、SEIDR(Synthesize, Execute, Instruct, Debug and repair)と呼ばれるマルチエージェントフレームワークでこの問題に対処する。 代替に焦点を当てた、修復に焦点を当てた、ハイブリッドなデバッグ戦略を比較することで、これらのトレードオフを実証的に探求します。
  論文  参考訳（メタデータ） (2025-03-10T16:56:51Z)
• EquiBench: Benchmarking Large Language Models' Understanding of Program Semantics via Equivalence Checking [55.81461218284736]
  EquiBenchは、大規模言語モデル(LLM)を評価するための新しいベンチマークである。 2つのプログラムが全ての可能な入力に対して同一の出力を生成するかどうかを決定する。 19の最先端LCMを評価し、最高の精度は63.8%と76.2%であり、これは50%のランダムベースラインよりわずかに高い。
  論文  参考訳（メタデータ） (2025-02-18T02:54:25Z)
• Ranking LLM-Generated Loop Invariants for Program Verification [14.7590099354867]
  大規模言語モデルは、0ショット設定でプログラムのクラスに対するループ不変量を合成することができる。 これは、不変性を確立するためのプログラム検証者への多数の呼び出しにつながる可能性がある。 我々は正しい帰納的不変量と誤った試みを区別できるランク付け器を設計した。
  論文  参考訳（メタデータ） (2023-10-13T18:13:52Z)
• ALGO: Synthesizing Algorithmic Programs with LLM-Generated Oracle Verifiers [60.6418431624873]
  大きな言語モデル(LLM)は、機能記述からコードを実装するのに優れているが、アルゴリズムの問題に悩まされている。 我々は,アルゴリズムプログラムを LLM 生成 Oracle で合成するフレームワーク ALGO を提案し,その生成をガイドし,その正確性を検証する。 実験の結果,ALGOを装着すると,Codexモデルよりも8倍,CodeTよりも2.6倍の1サブミッションパス率が得られることがわかった。
  論文  参考訳（メタデータ） (2023-05-24T00:10:15Z)
• A Fully Single Loop Algorithm for Bilevel Optimization without Hessian Inverse [121.54116938140754]
  両レベル最適化問題に対して,Hessian 逆フリーな完全単一ループアルゴリズムを提案する。 我々のアルゴリズムは$O(epsilon-2)$と収束することを示す。
  論文  参考訳（メタデータ） (2021-12-09T02:27:52Z)
• Enabling Retargetable Optimizing Compilers for Quantum Accelerators via a Multi-Level Intermediate Representation [78.8942067357231]
  我々は、最適化され、再ターゲット可能で、事前コンパイルが可能なマルチレベル量子古典中間表現(IR)を提案する。 ゲートベースのOpenQASM 3言語全体をサポートし、共通量子プログラミングパターンのカスタム拡張と構文の改善を提供します。 私たちの研究は、通常のPythonのアプローチよりも1000倍高速で、スタンドアロンの量子言語コンパイラよりも5～10倍高速なコンパイル時間を実現しています。
  論文  参考訳（メタデータ） (2021-09-01T17:29:47Z)
• A Reinforcement Learning Environment for Polyhedral Optimizations [68.8204255655161]
  マルコフ決定過程(MDP)として多面体モデルにおける法的変換空間の形状に依存しない定式化を提案する。 変換を使う代わりに、定式化は可能なスケジュールの抽象空間に基づいている。 我々の総合的MDP定式化は、強化学習を用いて幅広いループで最適化ポリシーを学習することを可能にする。
  論文  参考訳（メタデータ） (2021-04-28T12:41:52Z)
• Static Neural Compiler Optimization via Deep Reinforcement Learning [1.458855293397494]
  本稿では,位相整合問題に対する深層強化学習手法を用いる。 LLVMのO3シークエンスを構成するサブシーケンスを用いて、エージェントはトレーニングに使用するソースコードのセット上でO3シークエンスより優れていることを学習する。 我々は、我々のアプローチを用いて訓練されたモデルは、ニューラル最適化エージェントとして現代のコンパイラに統合できると考えている。
  論文  参考訳（メタデータ） (2020-08-20T13:16:29Z)
• Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version) [19.87276407545565]
  我々は、一般SMT学習のための新しいニューラルネットワーク、Gated Continuous Logic Network (G-CLN)を導入する。 G-CLNは継続論理ネットワーク(CLN)アーキテクチャを拡張し、ゲーティングユニットとドロップアウトを提供する。 G-CLNの収束率は2次問題に対して9.7.5%、CLNモデルに対して39.2%である。
  論文  参考訳（メタデータ） (2020-03-17T21:44:37Z)

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

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