論文の概要: Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models

• arxiv url: http://arxiv.org/abs/2605.24619v1
• Date: Sat, 23 May 2026 15:06:15 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-26 19:50:18.2768
• Title: Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models
• Title（参考訳）: IC3および大規模言語モデルによる分散プロトコルの帰納不変量の合成
• Authors: Weining Cao, Guangyuan Wu, Yuan Yao, Hengfeng Wei, Taolue Chen, Xiaoxing Ma,
• Abstract要約: 我々は、TLA+状態上でIC3スタイルのプロセスを実行することにより、誘導的不変量を合成する、ニューロシンボリックなフレームワークであるIC3Synを提案する。 我々は、コンセンサス、再構成、クライアントサーバシステムにまたがる29の分散プロトコル上でIC3Synを評価する。
• 参考スコア（独自算出の注目度）: 10.962435384504301
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Distributed protocols are notoriously difficult to verify correctly. Proving safety typically requires inductive invariants that both imply the desired property and are preserved by every protocol transition; yet inferring such invariants remains a major bottleneck: existing approaches either restrict the protocol models to a decidable fragment of first-order logic or demand expert-crafted templates. We present IC3Syn, a neuro-symbolic framework that synthesizes inductive invariants by executing an IC3-style process over TLA+ states with the assistance of Large Language Models (LLMs). At large, IC3Syn combines a symbolic IC3 controller, which decomposes invariant synthesis into focused blocking tasks and an LLM which provides protocol-level reasoning that IC3 alone lacks for TLA+ specifications. This integration enables a disciplined yet flexible search for invariants without imposing logical restrictions or requiring manual templates. We evaluate IC3Syn on 29 distributed protocols spanning consensus, reconfiguration and client-server systems, and compare it against Endive, IC3PO, SWISS and DistAI. IC3Syn discovers candidate invariants for all 29 protocols, including MongoLoglessDynamicRaft (MLDR), an industrial-scale Raft-based reconfiguration protocol for which none of the compared tools reports a solution, as well as one complex Paxos variant. In each case, the invariants synthesized on finite instances are shown in TLAPS to be inductive for the full unbounded protocol, thereby establishing safety.
• Abstract（参考訳）: 分散プロトコルは、正確な検証が難しいことで知られている。 安全性を証明するには典型的には、望ましいプロパティを暗示し、すべてのプロトコルトランジションによって保存される帰納的不変性を必要とするが、そのような不変性を推論することは大きなボトルネックであり、既存のアプローチではプロトコルモデルを一階述語論理の決定可能な断片に制限するか、専門家が作成したテンプレートを要求するかのいずれかである。 我々は,大言語モデル(LLMs)の助けを借りて,TLA+状態上でIC3スタイルのプロセスを実行することにより,誘導的不変量を合成する,ニューロシンボリックなフレームワークであるIC3Synを提案する。 IC3Synは、IC3コントローラと、IC3だけがTLA+仕様に欠けているというプロトコルレベルの推論を提供するLCMを組み合わせた。 この統合により、論理的な制約を課したり、手動のテンプレートを必要とせずに、規律付きながら柔軟な不変の検索が可能になる。 コンセンサス,再構成,クライアントサーバシステムにまたがる29の分散プロトコル上でIC3Synを評価し,Endive,IC3PO,SWISS,DistAIと比較した。 IC3Synは、産業規模のRaftベースの再構成プロトコルであるMongoLoglessDynamicRaft(MLDR)を含む29のプロトコルの候補不変性を発見した。 いずれの場合も、有限個のインスタンスで合成された不変量は TLAPS で示され、完全な非有界なプロトコルに対して帰納的であり、それによって安全性が確立される。

関連論文リスト

• From I/O to Code with Discovery Agent [103.88427301265669]
  IO2Codeの発見エージェントであるDIO-Agentを提案する。 本手法は,プログラム空間上の進化的探索としてIO2Codeをフレーム化する。 大規模な実験により、DIO-Agentは従来のプログラムバイサンプル法とSOTA進化エージェントベースラインの両方を一貫して上回っていることが示された。
  論文  参考訳（メタデータ） (2026-05-14T18:57:32Z)
• CktFormalizer: Autoformalization of Natural Language into Circuit Representations [23.44745731124114]
  CktFormalizerは、Lean 4.0に組み込まれた依存型HDLを通じてハードウェア生成をリダイレクトするフレームワークである。 VerilogEval(156問題)、RTLLM(50問題)、ResBench(56問題)では、CktFormalizerは直接Verilog生成と競合するシミュレーションパスレートを達成する。
  論文  参考訳（メタデータ） (2026-05-08T14:20:06Z)
• Beyond Structure: Revolutionising Materials Discovery via AI-Driven Synthesis Protocol-Property Relationships [0.0]
  このギャップを埋めるには、実行可能な合成プロトコルを主設計変数として扱う合成第一パラダイムへの転換が必要であると我々は主張する。 i) 合成手順を機械可読プロトコルとして表現する、(ii) 生成および逆設計モデルを展開して反応経路やレシピを提案する、(iii) 実験現実や持続可能性制約に対するプロトコルを洗練するためにクローズドループ最適化を統合する、という3つの柱の上に構築されたロードマップを概説する。
  論文  参考訳（メタデータ） (2026-05-01T00:48:39Z)
• Multigrain-aware Semantic Prototype Scanning and Tri-Token Prompt Learning Embraced High-Order RWKV for Pan-Sharpening [46.94213480279033]
  パンシャーピングのための多言語対応セマンティックプロトタイプスキャンパラダイムを提案する。 我々は、高階RWKVアーキテクチャとセマンティッククラスタリングから派生したトリトケンプロンプト機構を用いる。 実験により,本手法の優位性を実証した。
  論文  参考訳（メタデータ） (2026-04-16T05:10:03Z)
• TermiGen: High-Fidelity Environment and Robust Trajectory Synthesis for Terminal Agents [70.68963723787424]
  TermiGenは検証可能な環境とレジリエントな専門家軌道を合成するためのエンドツーエンドパイプラインである。 TermiGen-Qwen2.5-Coder-32B は TerminalBench 上で 31.3% のパスレートを達成した。
  論文  参考訳（メタデータ） (2026-02-06T23:56:50Z)
• Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
  生成のための教師なし共形推論フレームワークを提案する。 我々のゲートは、分断されたUPPよりも厳密で安定した閾値を提供する。 その結果は、ラベルのない、API互換の、テスト時間フィルタリングのゲートになる。
  論文  参考訳（メタデータ） (2025-09-26T23:40:47Z)
• LLM-Assisted Model-Based Fuzzing of Protocol Implementations [9.512044399020514]
  プロトコル動作の障害は脆弱性やシステム障害につながる可能性がある。 プロトコルテストに対する一般的なアプローチは、プロトコルの状態遷移と期待される振る舞いをキャプチャするマルコフモデルを構築することである。 本稿では,大規模言語モデル(LLM)を利用して,ネットワークプロトコルの実装をテストするためのシーケンスを自動的に生成する手法を提案する。
  論文  参考訳（メタデータ） (2025-08-03T13:16:18Z)
• ProtocolLLM: RTL Benchmark for SystemVerilog Generation of Communication Protocols [45.66401695351214]
  本稿では,広く使用されているSystemVerilogプロトコルを対象とした最初のベンチマークスイートであるProtocolLLMを紹介する。 我々は,ほとんどのモデルがタイミング制約に従う通信プロトコルのSystemVerilogコードを生成するのに失敗したことを観察する。
  論文  参考訳（メタデータ） (2025-06-09T17:10:47Z)
• Squeezeformer: An Efficient Transformer for Automatic Speech Recognition [99.349598600887]
  Conformerは、そのハイブリッドアテンション・コンボリューションアーキテクチャに基づいて、様々な下流音声タスクの事実上のバックボーンモデルである。 Squeezeformerモデルを提案する。これは、同じトレーニングスキームの下で、最先端のASRモデルよりも一貫して優れている。
  論文  参考訳（メタデータ） (2022-06-02T06:06:29Z)

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

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