Fugu-MT 論文翻訳(概要): LimICE: Integrating LLM into ICE Framework for Efficient Loop Invariant Inference

論文の概要: LimICE: Integrating LLM into ICE Framework for Efficient Loop Invariant Inference

arxiv url: http://arxiv.org/abs/2607.27606v1
Date: Thu, 30 Jul 2026 02:50:09 GMT
ステータス: 翻訳完了
システム内更新日: 2026-07-31 21:37:00.370003
Title: LimICE: Integrating LLM into ICE Framework for Efficient Loop Invariant Inference
Title（参考訳）: LimICE: 効率的なループ不変推論のためのLLMをICEフレームワークに統合する
Abstract要約: インクリメンタル合成のための新しい学習フレームワークであるインクリメンタルICEを提案する。本フレームワークはIC3の漸進的哲学を一般的な不変学習フレームワークICEに統合する。このフレームワークでは、LLMを利用して順序付けられたレムマ列を生成するループ不変合成ツールLimICEをインスタンス化する。
参考スコア（独自算出の注目度）: 10.534386090450276
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Loop invariant synthesis is a fundamental problem in program verification, yet the inherent undecidability makes it highly challenging. Recent studies have increasingly employed various machine learning techniques to generate loop invariants. However, most of these methods adopt a monolithic approach. Due to the inability to strictly constrain the learning process, learning-based methods struggle to simultaneously consider all necessary conditions and generate complete invariants when tackling complex problems. In fact, a loop invariant is often an ordered sequence of lemmas, rather than a single invariant formula. This motivates us to propose Incremental ICE, a novel learning framework for incremental synthesis. Our framework integrates the incremental philosophy of IC3 into the general invariant learning framework ICE. By defining a lemma-specific learning objective and introducing a counterexample filtering mechanism, we can achieve sound incremental learning. Under this framework, we instantiate a loop invariant synthesis tool, LimICE, which leverages LLMs to generate the ordered sequence of lemmas and incorporates ICE-DT as a fallback mechanism to complement the lemma sequence. Experiments on 367 linear benchmarks and 50 nonlinear benchmarks demonstrate the effectiveness of the proposed approach. LimICE solves 349 (out of 367) linear problems on an average of 15.2 seconds and 47 (out of 50) nonlinear problems on an average of 8.8 seconds. Compared to the state-of-the-art LLM-based baseline, our approach solves 12-24% more instances while running 36-63% faster across linear and nonlinear benchmarks. LimICE also consistently outperforms strong non-LLM baselines and solves at least 86 and 27 additional instances on the linear and nonlinear benchmarks, respectively.
Abstract（参考訳）: ループ不変合成は、プログラム検証の基本的な問題であるが、固有の不決定性は、非常に困難である。近年の研究では、ループ不変量を生成するために様々な機械学習技術が採用されている。しかし、これらの手法のほとんどはモノリシックなアプローチを採用している。学習過程を厳格に制約することができないため、学習ベースの手法は、複雑な問題に取り組む際に必要なすべての条件を同時に考慮し、完全な不変量を生成するのに苦労する。実際、ループ不変量は単一の不変式ではなく、しばしば順序付けられた補題列である。これはインクリメンタルシンセサイザーのための新しい学習フレームワークであるインクリメンタルICEを提案する動機となっている。本フレームワークはIC3の漸進的哲学を一般的な不変学習フレームワークICEに統合する。補題固有の学習目標を定義し,反例フィルタリング機構を導入することにより,音のインクリメンタル学習を実現することができる。この枠組みでは,LLMを利用して順序付けられた補題列を生成するループ不変合成ツールLimICEをインスタンス化し,ICE-DTをフォールバック機構として組み込んで補足する。 367の線形ベンチマークと50の非線形ベンチマークの実験は、提案手法の有効性を実証している。 LimICEは平均15.2秒で349(うち367)の線形問題を解き、平均8.8秒で47(うち50)の非線形問題を解く。現状のLCMベースラインと比較して,線形および非線形ベンチマークで36～63%高速に動作しながら,12～24%のインスタンスを探索する。 LimICEはまた、強い非LLMベースラインを一貫して上回り、それぞれ線形ベンチマークと非線形ベンチマークで少なくとも86と27のインスタンスを解決している。

関連論文リスト

SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification [2.6426981014417046]
我々は、意味マッピングと正式な認証を分離するLLM支援SMTフレームワークであるSOVERを紹介する。また、NLEquiv-150は100の等価性と50の故意に非等価な非線形改質ペアの公的なベンチマークである。
論文参考訳（メタデータ） (2026-09-01T05:05:12Z)
Not All Problems Are Best Modeled as MILP: A DSL-Centric Framework for Flexible and Accurate Optimization Modeling [18.793227025879993]
我々は、厳密なMILPの定式化からドメイン固有の言語表現へ焦点を移すフレームワークOptiを提案する。 LLMを利用して、自然言語を標準化されたドメイン受け入れ構造にマッピングすることで、Optiは問題の定式化を実行から切り離す。
論文参考訳（メタデータ） (2026-08-07T09:50:52Z)
Scaling Self-Play with Self-Guidance [62.13619253976748]
Self-Guided Self-Play (SGS)は、Conjecturerをジェネラシーから遠ざけるセルフプレイアルゴリズムである。 SGSは80ラウンド未満のセルフプレイで、最強のベースラインの解決率を上回っています。
論文参考訳（メタデータ） (2026-04-22T05:50:23Z)
$\ abla$-Reasoner: LLM Reasoning via Test-Time Gradient Descent in Latent Space [71.23672814629448]
$nabla$-Reasonerは、トークンログに対する差別化可能な最適化をデコードループに統合する反復生成フレームワークである。 $nabla$-Reasonerは、挑戦的な数学的推論ベンチマークで20%以上の精度の向上を実現している。
論文参考訳（メタデータ） (2026-03-05T08:42:54Z)
Para-B&B: Load-Balanced Deterministic Parallelization of Solving MIP [50.917107318582715]
MIP(Mixed-integer Programming)は、連続型と整数型の両方の決定変数を組み込むことで線形プログラミングを拡張する。本稿では,高性能MIPソルバであるHiGHSに対して,決定論的並列分岐結合の完全なオープンソース実装を初めて提案する。本手法では,ワーカスレッド間で完全なソルバ状態を複製することにより,厳密な決定性を保証する新しいデータ並列アーキテクチャを提案する。
論文参考訳（メタデータ） (2026-02-10T14:17:53Z)
Inference-Aware Meta-Alignment of LLMs via Non-Linear GRPO [55.574265038358455]
推論対応メタアライメント(IAMA)は、大きな言語モデルを多様な人間の好みに合わせる新しいアプローチである。 IAMAは、異なる推論時間アライメントアルゴリズムによって複数のタスクに効果的にアライメントできるようにベースモデルを訓練する。確率測度の空間における最適解に確実に収束する非線形GRPOを提案する。
論文参考訳（メタデータ） (2026-02-02T03:50:42Z)
Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers [2.0686733932673604]
現代, 推論に最適化された大規模言語モデルが, シンボリックアプローチよりも優れているかどうかを考察する。 OpenAIのO1、O1-mini、O3-miniを、Z3 SMTソルバと密結合した生成とチェックのパイプラインに統合します。私たちのフレームワークは、100%のカバレッジ(133のうち133)を達成し、133のうち107よりも優れています。
論文参考訳（メタデータ） (2025-08-01T08:15:15Z)
OptiBench Meets ReSocratic: Measure and Improve LLMs for Optimization Modeling [62.19438812624467]
大規模言語モデル (LLM) は数学的推論における問題解決能力を示した。本稿では,人間可読入力と出力を用いたエンドツーエンド最適化問題のベンチマークであるOptiBenchを提案する。
論文参考訳（メタデータ） (2024-07-13T13:27:57Z)
Reinforcement Learning for Branch-and-Bound Optimisation using Retrospective Trajectories [72.15369769265398]
機械学習は分岐のための有望なパラダイムとして登場した。分岐のための単純かつ効果的なRLアプローチであるレトロ分岐を提案する。我々は現在最先端のRL分岐アルゴリズムを3～5倍に上回り、500の制約と1000の変数を持つMILP上での最高のILメソッドの性能の20%以内である。
論文参考訳（メタデータ） (2022-05-28T06:08:07Z)
Multiblock ADMM for nonsmooth nonconvex optimization with nonlinear coupling constraints [3.2815423235774634]
非線形制約を伴う多重ブロック非平滑交互最適化問題のクラスを解くための乗算器の手法を提案する。一次変数の各ブロックの更新に主要なシーケンス化手順を用いる。
論文参考訳（メタデータ） (2022-01-19T15:31:30Z)
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)

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

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