論文の概要: Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models

• arxiv url: http://arxiv.org/abs/2607.27964v2
• Date: Sun, 02 Aug 2026 10:30:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-04 15:07:24.12135
• Title: Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models
• Title（参考訳）: 大規模言語モデルを用いたデッドロックフリー通信プロトコルの仕様誘導合成
• Authors: Yang Li, Ping Hou, Nobuko Yoshida,
• Abstract要約: シントロピー(英: Syntropy)は、MPST仕様とLLMによってガイドされたプロトコルの洗練を合成するためのフレームワークである。 改良制約を直接生成プロセスに組み込んで、生成された変種がこれらの保証を満たすことを保証する。 本評価は, 高い構文的正しさを維持しつつ, 95.6%-99.5%の妥当性を達成し, 多様な非自明な精細化を実現していることを示す。
• 参考スコア（独自算出の注目度）: 2.1311014724439845
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Ensuring behavioural correctness in communication protocols is a central challenge in distributed software systems, as subtle inconsistencies can lead to deadlocks. In such settings, protocol refinement - the safe substitution of a protocol that preserves correctness and compatibility with other components - is essential. Large language models (LLMs) have demonstrated strong capabilities in code generation and program synthesis, yet lack mechanisms to reliably produce outputs with correct behaviour. Formal specification approaches, such as multiparty session types (MPST), offer rigorous guarantees, including deadlock freedom, but provide limited support for automatically constructing protocol refinements. In this paper, we present Syntropy, a framework for synthesising protocol refinements guided by MPST specifications and LLMs. It incorporates refinement constraints directly into the generation process, ensuring the generated variants satisfy these guarantees. Our comprehensive evaluation indicates that Syntropy achieves 95.6%-99.5% validity while maintaining high syntactic correctness, and produces diverse, non-trivial refinements across multiple LLMs.
• Abstract（参考訳）: 通信プロトコルにおける振る舞いの正しさを保証することは、微妙な不整合がデッドロックを引き起こす可能性があるため、分散ソフトウェアシステムにおける中心的な課題である。 このような設定では、プロトコルのリファインメント(他のコンポーネントとの正確性と互換性を維持するプロトコルの安全な置換)が不可欠である。 大規模言語モデル(LLM)は、コード生成とプログラム合成において強力な能力を示してきたが、正しい振る舞いで出力を確実に生成するメカニズムが欠如している。 マルチパーティセッションタイプ(MPST)のような形式的な仕様アプローチは、デッドロックの自由を含む厳格な保証を提供するが、プロトコルの洗練を自動的に構築するための限定的なサポートを提供する。 本稿では,MPST仕様とLLMでガイドされたプロトコルリファインメントを合成するためのフレームワークであるSyntropyを提案する。 改良制約を直接生成プロセスに組み込んで、生成された変種がこれらの保証を満たすことを保証する。 総合評価の結果,Syntropyは高い構文的正しさを維持しつつ95.6%-99.5%の妥当性を達成し,複数のLCMに対して多種多様な非自明な精細化を実現していることがわかった。

関連論文リスト

• Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis [14.825615940318038]
  ZkEVMは、オフチェーン実行の正しさを保証するゼロ知識を生成する。 微妙な実装上のバグは、意味的に欠陥のある状態を証明する有効な証明につながる可能性がある。 SMTソルバによる形式検証は、これを防止できるが、仕様によってボトルネックとなる。 Rustから実行可能なPython/Z3検証モデルを合成するフレームワークであるVeri Synthを提案する。
  論文  参考訳（メタデータ） (2026-07-22T06:20:36Z)
• LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean [9.293322518056357]
  本稿では,タイプベースの推論とトレースベースの推論を組み合わせることで,ステートフルプロトコルとアンバウンドプロトコルのモジュール検証を実現する手法を提案する。 私たちはこのフレームワークをリーン実証アシスタント用のLeanDYライブラリとして実装し、DY*の設計を構築し拡張します。 我々は、LeanDYでSegWitスタイルのブロックチェーンプリミティブを形式化し、支払いチャネルの詳細な形式化を行うことで、その表現性を実証する。
  論文  参考訳（メタデータ） (2026-07-03T15:12:30Z)
• When LLMs Develop Languages: Symbolic Communication for Efficient Multi-Agent Reasoning [85.36421257648294]
  CoT(Chain-of-Thought)は、難しい推論タスクにおいて、大きな言語モデル(LLM)を改善する。 コミュニケーション言語シンボリズムルーティング(R)を提案する。 Rは、それぞれの言語シンボルフレームワークを、コンパクトなシンボル、使用規則、メッセージパス契約を備えた再利用可能なシンボルプロトコルとして扱います。 Rは、標準のCoTと比較してレイテンシ指向のトークンの補完を$3sim 6times$に削減する。
  論文  参考訳（メタデータ） (2026-06-28T12:02:42Z)
• A Technical Taxonomy of LLM Agent Communication Protocols [60.76747983053368]
  本研究では,大規模言語モデル(LLM)エージェント通信プロトコルの分類と解析を行う技術的分類法を開発する。 このフレームワークはプロトコルの選択をガイドし、プライバシーやポリシー執行といったオープンな研究ギャップを強調する。
  論文  参考訳（メタデータ） (2026-06-17T14:45:20Z)
• SEVerA: Verified Synthesis of Self-Evolving Agents [12.9624447364193]
  自己進化型エージェントフレームワークは、安全性や正確性の正式な保証を提供しない。 エージェントコード生成を制約付き学習問題として定式化し、ハードな形式仕様とソフトな目的とを組み合わせてタスクユーティリティをキャプチャする。 探索はFGGMコールを含む候補パラメトリックプログラムを合成し、検証は全てのパラメータ値に対する厳しい制約に関して正当性を証明し、制約のない学習に還元する。
  論文  参考訳（メタデータ） (2026-03-26T07:32:20Z)
• Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
  生成のための教師なし共形推論フレームワークを提案する。 我々のゲートは、分断されたUPPよりも厳密で安定した閾値を提供する。 その結果は、ラベルのない、API互換の、テスト時間フィルタリングのゲートになる。
  論文  参考訳（メタデータ） (2025-09-26T23:40:47Z)
• ProtocolLLM: RTL Benchmark for SystemVerilog Generation of Communication Protocols [45.66401695351214]
  本稿では,広く使用されているSystemVerilogプロトコルを対象とした最初のベンチマークスイートであるProtocolLLMを紹介する。 我々は,ほとんどのモデルがタイミング制約に従う通信プロトコルのSystemVerilogコードを生成するのに失敗したことを観察する。
  論文  参考訳（メタデータ） (2025-06-09T17:10:47Z)
• Towards Semantic Communication Protocols: A Probabilistic Logic Perspective [69.68769942563812]
  我々は,NPMを確率論理型言語ProbLogで記述された解釈可能なシンボルグラフに変換することによって構築された意味プロトコルモデル(SPM)を提案する。 その解釈性とメモリ効率を利用して、衝突回避のためのSPM再構成などのいくつかの応用を実演する。
  論文  参考訳（メタデータ） (2022-07-08T14:19:36Z)
• Data post-processing for the one-way heterodyne protocol under composable finite-size security [62.997667081978825]
  本研究では,実用的連続可変(CV)量子鍵分布プロトコルの性能について検討する。 ヘテロダイン検出を用いたガウス変調コヒーレント状態プロトコルを高信号対雑音比で検討する。 これにより、プロトコルの実践的な実装の性能を調べ、上記のステップに関連付けられたパラメータを最適化することができる。
  論文  参考訳（メタデータ） (2022-05-20T12:37:09Z)

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

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