論文の概要: Protocol-Driven Development: Governing Generated Software Through Invariants and Continuous Evidence
- arxiv url: http://arxiv.org/abs/2605.12981v3
- Date: Tue, 19 May 2026 08:37:24 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-20 15:03:08.270408
- Title: Protocol-Driven Development: Governing Generated Software Through Invariants and Continuous Evidence
- Title(参考訳): プロトコル駆動開発: 不変性と継続的なエビデンスによる生成したソフトウェアの支配
- Abstract要約: ここでは、主要なソフトウェアアーチファクトがコードではなく、機械で強化可能なプロトコルであるプロトコル駆動開発(PDD)を紹介します。
PDDは、自動化されたソフトウェアエンジニアリングのためのガバナンスモデルを定義する。
- 参考スコア(独自算出の注目度): 2.124730017640531
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Automated program synthesis lowers the cost of producing implementations but introduces a harder governance problem: determining which generated artifacts are admissible. Natural-language specifications are ambiguous, and example-based tests sample only part of the behavioral space. Used alone, neither provides a sufficient control boundary. We introduce Protocol-Driven Development (PDD), where the primary software artifact is a machine-enforceable protocol rather than code. We define a protocol as the triplet P = (S, B, O), specifying structural, behavioral, and operational invariants. Their conjunction defines the admissible implementation space of a software component. Under PDD, implementations are replaceable realizations discovered through constrained search. An implementation is admitted only if it satisfies the protocol and produces a verifiable Evidence Chain of compliance. Admission is grounded in protocol satisfaction and recorded evidence rather than trust in the generator. For deployed systems, we extend the Evidence Chain into a Dynamic Evidence Ledger. Runtime verifiers append signed observations, invariant checks, and violations to the ledger, allowing monitorable obligations to be continuously attested. This connects live failures back to the generation loop without granting the generator runtime authority. Combining formal methods, property testing, runtime verification, policy-as-code, and software provenance, PDD defines a governance model for automated software engineering. Its organizing principle is that code is transient, while the protocol carries durable authority.
- Abstract(参考訳): 自動プログラム合成は、実装のコストを下げるが、どの生成したアーティファクトが許容可能かを決定するという、より難しいガバナンス問題を提起する。
自然言語仕様は曖昧であり、例ベースのテストは行動空間の一部だけをサンプリングする。
単独で使用すると、どちらも十分な制御境界を提供しない。
ここでは、主要なソフトウェアアーチファクトがコードではなく、機械で強化可能なプロトコルであるプロトコル駆動開発(PDD)を紹介します。
プロトコルを三重項 P = (S, B, O) として定義し、構造的、行動的、操作的不変量を指定する。
彼らの協力関係は、ソフトウェアコンポーネントの許容可能な実装空間を定義する。
PDDの下では、実装は制約付き探索によって発見される代替可能な実現である。
実装は、プロトコルを満たし、コンプライアンスの検証可能なエビデンスチェーンを生成する場合にのみ許可される。
許可はプロトコルの満足度に基づいており、ジェネレータへの信頼よりも証拠を記録している。
デプロイシステムでは、Evidence ChainをDynamic Evidence Ledgerに拡張します。
実行時検証者は、署名された観察、不変チェック、および台帳への違反を追加し、監視可能な義務を継続的に証明する。
これにより、ジェネレータランタイムの権限を付与することなく、ライブ障害をジェネレータループに戻すことができる。
形式的なメソッド、プロパティテスト、実行時検証、ポリシ・アズ・コード、ソフトウェアプロファイランスを組み合わせることで、PDDは自動化されたソフトウェアエンジニアリングのためのガバナンスモデルを定義します。
その組織原理は、コードは過渡的であり、プロトコルは耐久性のある権威を持っている。
関連論文リスト
- $Z^2$-ACT: End-to-End Verifiable Agentic Intent Control for Open 6G RAN [43.15181031994434]
本稿では,ゼロ知識監査制御とゼロ信頼検証エージェントインテントアーキテクチャを提案する。
実大規模言語モデルは、オペレータの意図をIntent Contractsに変換するために、非リアルタイムパスで使用される。
その結果、動作フィルタリングと攻撃レジリエンスを適度なレイテンシとシグナリングコストで改善したことが示唆された。
論文 参考訳(メタデータ) (2026-08-21T12:44:03Z) - Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
Veroはリポジトリレベルで共同実装と証明を評価する最初のベンチマークである。
Python、Dafny、Verus、Coqにまたがる実世界のリポジトリから43のマルチモジュールインスタンスが含まれている。
ベンチマークの信頼性を改善するため、Veroには、エージェントが提供された仕様の不満足さを正式に証明できる監査メカニズムも含まれている。
論文 参考訳(メタデータ) (2026-08-13T17:41:27Z) - Constraint-Driven Synthesis of Hyper Petri Nets [46.9047309711542]
本稿では,ペトリネット(PN)を用いた制約ロボットシステムのモデリングと合成について述べる。
全ての可観測系状態が与えられた論理的制約を満たしつつ、実行可能な遷移意味論と整合性を維持したモデルを構築する方法について検討する。
提案手法では,観測可能な状態に対する明示的な実行セマンティクスを導入する。
論文 参考訳(メタデータ) (2026-07-24T07:57:19Z) - PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
我々は、スケジューリング、検証、メモリ、ベンチマーク、安全性をシステムレベルのサービスとして提供するPhyAgentOSを紹介します。
セッション中心のセッションは、スケジューリング、互換性、監督された実行、エビデンス収集、受け入れの最小単位として、アクションではなくセッションを扱う。
SessionVerifierは、実行終了とセマンティックタスク完了を、成功、失敗、または再計画のエビデンスに基づいて判断する。
ベンチマークはデプロイメントセッションと検証パスを再利用するので、結果は実際の実行に遡る。
論文 参考訳(メタデータ) (2026-07-18T04:46:53Z) - CAVA: Canonical Action Verification and Attestation for Runtime Governance of Agentic AI Systems [0.6526824510982799]
本稿では、異種エージェントのアクティビティを標準ランタイムオブジェクトに変換するランタイム・セマンティック・レイヤを提案する。
このコントリビューションは、デプロイ側AIガバナンスに必要な基盤として、アクションレベルの標準化とポリシー順応可能なセマンティックパターンを定式化したシステムである。
論文 参考訳(メタデータ) (2026-07-15T11:34:34Z) - Proof-Carrying Agent Actions: Model-Agnostic Runtime Governance for Heterogeneous Agent Systems [0.6526824510982799]
本稿では,アクション証明書を中心としたランタイム中立ガバナンスモデルであるProof-Carrying Agent Actions (PCAA)を提案する。
PCAAは5つのチェックポイント(事前行動の許容、行動のオープン、仮定のキャプチャ、承認、結果のクロージャ)を統括する。
異種エージェント制御プレーンと開示バウンダリ評価プロトコルの参照実装を用いてモデルについて検討する。
論文 参考訳(メタデータ) (2026-06-02T18:10:35Z) - Autogenesis: A Self-Evolving Agent Protocol [60.15939127351914]
本稿では,自己進化プロトコルであるAutogenesis Protocol(AGP)を紹介する。
本稿では,実行中のプロトコル登録リソースを動的にインスタンス化し,検索し,精錬する自己進化型マルチエージェントシステムAGSを提案する。
論文 参考訳(メタデータ) (2026-04-16T14:04:06Z) - REGAL: A Registry-Driven Architecture for Deterministic Grounding of Agentic AI in Enterprise Telemetry [0.0]
大規模言語モデル(LLM)は、エージェント自動化の新しい形態を可能にする。
本稿では,企業テレメトリにおけるエージェントAIシステムの決定論的基盤化のためのレジストリ駆動型アーキテクチャREGALを提案する。
論文 参考訳(メタデータ) (2026-03-03T14:13:39Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳(メタデータ) (2025-11-26T06:39:19Z) - 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) - ModelForge: Using GenAI to Improve the Development of Security Protocols [1.9241821314180376]
プロトコル仕様の翻訳を自動化する新しいツールであるModelForgeを紹介する。
自然言語処理(NLP)と生成AI(GenAI)の進歩を活用することで、ModelForgeはプロトコル仕様を処理し、CPSAプロトコル定義を生成する。
論文 参考訳(メタデータ) (2025-06-08T06:27:09Z) - Validating Network Protocol Parsers with Traceable RFC Document Interpretation [11.081773172066766]
オラクルとトレーサビリティの問題は、プロトコルの実装がいつバグがあると考えられるかを決定する。
この研究はどちらも考慮し、大規模言語モデル(LLM)の最近の進歩を利用した効果的なソリューションを提供する。
我々は、C、Python、Goで書かれた9つのネットワークプロトコルとその実装を使用して、我々のアプローチを広く評価してきた。
論文 参考訳(メタデータ) (2025-04-25T03:39:19Z) - Keeping Behavioral Programs Alive: Specifying and Executing Liveness Requirements [2.4387555567462647]
タスクがまだ完了していないことを示すために,"must-finish"を付けたタグ付け状態のイディオムを提案する。
また,B"uchiautoaへの翻訳に基づくセマンティクスと,マルコフ決定プロセス(MDP)に基づく2つの実行メカニズムも提供する。
論文 参考訳(メタデータ) (2024-04-02T11:36:58Z) - Towards an Enforceable GDPR Specification [49.1574468325115]
プライバシ・バイ・デザイン(PbD)は、EUなどの現代的なプライバシー規制によって規定されている。
PbDを実現する1つの新しい技術は強制(RE)である
法律規定の正式な仕様を作成するための一連の要件と反復的な方法論を提示する。
論文 参考訳(メタデータ) (2024-02-27T09:38:51Z) - Towards Semantic Communication Protocols: A Probabilistic Logic
Perspective [69.68769942563812]
我々は,NPMを確率論理型言語ProbLogで記述された解釈可能なシンボルグラフに変換することによって構築された意味プロトコルモデル(SPM)を提案する。
その解釈性とメモリ効率を利用して、衝突回避のためのSPM再構成などのいくつかの応用を実演する。
論文 参考訳(メタデータ) (2022-07-08T14:19:36Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。