Fugu-MT 論文翻訳(概要): Self-evolving network verifiers

論文の概要: Self-evolving network verifiers

arxiv url: http://arxiv.org/abs/2608.11340v1
Date: Tue, 11 Aug 2026 18:45:15 GMT
ステータス: 翻訳完了
システム内更新日: 2026-08-13 19:07:54.336969
Title: Self-evolving network verifiers
Title（参考訳）: 自己進化型ネットワーク検証器
Abstract要約: シンボリックネットワーク検証器は、ルーティング入力と障害の広大な空間にわたって正確性を推論することができる。代わりに、実際のネットワークの振る舞いを忠実に捉えるために、モデルが自動的に進化すべきである、と私たちは主張する。
参考スコア（独自算出の注目度）: 4.369247388526747
License: http://creativecommons.org/licenses/by/4.0/
Abstract: Symbolic network verifiers can reason about correctness across vast spaces of routing inputs and failures, but only for the protocols and features an expert has encoded by hand. Creating and maintaining a faithful model of the control plane is both difficult and never-ending, since no written source specifies perfectly what a network does: vendor implementations deviate from the RFCs, and behaviour shifts with releases. The burden of constant upkeep ultimately keeps verification out of many networks that need it. We argue that the model should instead evolve automatically to faithfully capture the actual network behaviour. To achieve that, we leverage the only source that specifies it unambiguously: the router software itself. In a counterexample-guided loop, a coding agent proposes extensions to the verifier's symbolic encoding, while a trusted oracle (e.g., emulated routers) supplies the ground-truth routing state. The agent iteratively refines the network model using each disagreement with the oracle. As early evidence, a prototype of this system taught a 3,000-line SMT-based verifier three features it did not support: OSPF areas, BGP route reflection, and L3VPN over EVPN, converging autonomously on models that match the oracle, even noticing vendor-specific behaviour. Automating model growth shifts the hard problem from writing verification systems to systematically testing them; we propose a research agenda for trusting and harnessing automatically evolved verifiers.
Abstract（参考訳）: シンボリックネットワーク検証器は、ルーティング入力と障害の広大な空間にわたって正確性を推論することができるが、専門家が手作業で符号化したプロトコルと機能に限られる。ベンダの実装はRFCから逸脱し、リリースによって振る舞いが変わる。絶え間ないアップキープの重荷は、最終的にそれを必要とする多くのネットワークから検証を外し続ける。代わりに、実際のネットワークの振る舞いを忠実に捉えるために、モデルが自動的に進化すべきである、と私たちは主張する。これを実現するために、ルータソフトウェア自体を曖昧に指定する唯一のソースを利用する。符号化エージェントは、反例誘導ループにおいて、検証者のシンボル符号化の拡張を提案し、信頼されたオラクル(例えばエミュレートされたルータ)は、接地トラスルーティング状態を提供する。エージェントは、宣誓供述書との相違を利用してネットワークモデルを反復的に洗練する。初期の証拠として、このシステムのプロトタイプは3000行のSMTベースの検証器に、サポートしていない3つの機能を教えた: OSPF領域、BGPルートリフレクション、EVPN上のL3VPN。モデルの成長の自動化は、検証システムの記述から体系的なテストへと難しい問題をシフトさせ、自動進化検証器を信頼し活用するための研究課題を提案する。

関連論文リスト

VeriEvol: Scaling Multimodal Mathematical Reasoning via Verifiable Evol-Instruct [71.22358682581215]
ビジュアルな数学的推論のための強化学習のスケーリングは、難しい質問を生成すること以上のものを必要とします。これは2つのコンポーネントからなる反復的なフレームワークであるVeriEvolとしてインスタンス化します。 5ベンチマークのビジュアル・マス・スイートでは、10Kから250KサンプルまでのSFTデータのスケーリングが平均精度を35.42から54.73に引き上げている。
論文参考訳（メタデータ） (2026-06-22T16:17:30Z)
From Detection to Response: A Deep Learning and Retrieval-Augmented Generation Framework for Network Intrusion Mitigation [0.7136933021609079]
本稿では,脅威検出と行動応答のギャップを埋める統一的なエンドツーエンドフレームワークを提案する。まず、独立に訓練された3つのバイナリディープニューラルネットワーク(DNN)のアンサンブルで、ネットワークトラフィックフローをBenign, Denial of Service(DoS)またはDistributed Denial of Service(DDoS)に分類する。第2に、Retrieval-Augmented Generation (RAG)パイプラインは、トップ5の異常な機能から説明対応プロンプトを構築する。
論文参考訳（メタデータ） (2026-05-18T07:17:55Z)
Protocol-Driven Development: Governing Generated Software Through Invariants and Continuous Evidence [2.124730017640531]
ここでは、主要なソフトウェアアーチファクトがコードではなく、機械で強化可能なプロトコルであるプロトコル駆動開発(PDD)を紹介します。 PDDは、自動化されたソフトウェアエンジニアリングのためのガバナンスモデルを定義する。
論文参考訳（メタデータ） (2026-05-13T04:23:14Z)
ChipMATE: Multi-Agent Training via Reinforcement Learning for Enhanced RTL Generation [55.947962672433675]
ChipMATEは、RTL生成のための最初の自己学習型マルチエージェントフレームワークである。 ChipMATEは産業的な実践に触発され、VerilogエージェントとPythonのリファレンスモデルエージェントをペアにし、相互に出力を検証する。 ChipMATEは、VerilogEval V2で75.0%と80.1%パス@1を4Bと9Bベースモデルで達成している。
論文参考訳（メタデータ） (2026-05-13T01:04:21Z)
Towards Verifiable AI with Lightweight Cryptographic Proofs of Inference [3.3323431541048385]
完全証明を軽量なサンプリングベースアプローチで置き換える検証フレームワークとプロトコルを提案する。我々は,機能的に異なるモデル間のトレース分離を活用可能な条件を定式化し,検証可能な推論プロトコルの安全性について議論する。我々の手法は、最先端の暗号証明システムと比較して、証明時間を桁違いに削減する。
論文参考訳（メタデータ） (2026-03-19T15:24:27Z)
TorchLean: Formalizing Neural Networks in Lean [71.68907600404513]
本稿では,学習モデルを一級数学的対象として扱うフレームワークであるTorchLeanを紹介する。我々はTorchLeanのエンドツーエンドを、証明された堅牢性、PINNの物理インフォームド残差、Lyapunovスタイルのニューラルコントローラ検証で検証する。
論文参考訳（メタデータ） (2026-02-26T05:11:44Z)
CREDIT: Certified Ownership Verification of Deep Neural Networks Against Model Extraction Attacks [54.04030169323115]
我々は、モデル抽出攻撃(MEA)に対する認証された所有権検証であるCREDITを紹介する。 DNNモデル間の類似性を定量化し、実用的な検証しきい値を提案し、このしきい値に基づいてオーナシップ検証を行うための厳密な理論的保証を提供する。我々は、さまざまなドメインやタスクにまたがるいくつかの主流データセットに対するアプローチを広範囲に評価し、最先端のパフォーマンスを実現した。
論文参考訳（メタデータ） (2026-02-23T23:36:25Z)
CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
論文参考訳（メタデータ） (2024-11-20T14:16:55Z)
Can Large Vision-Language Models Correct Semantic Grounding Errors By Themselves? [61.899791071654654]
本稿では,視覚言語モデル(VLM)が,フィードバックの「受信」によって意味的接地を改善することができるかどうかを検討する。適切に刺激すれば、VLMは1ステップと反復の両方でフィードバックを活用できる。検討したすべての設定において、すべてのモデルにまたがる自動フィードバックを用いて、基底精度を一貫して改善することを示す。
論文参考訳（メタデータ） (2024-04-09T17:59:04Z)
Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers [1.5749416770494706]
車両には、ニューラルネットワーク仕様を記述するための表現力のあるドメイン固有言語が備わっている。同様のITPの形式化において、保守性とスケーラビリティに関する過去の問題を克服しています。ニューラルネットワーク検証器であるMarabouをAgdaに接続し、ニューラルネットワークで操縦された車が道路を離れないことを正式に検証することで、その実用性を実証する。
論文参考訳（メタデータ） (2022-02-10T18:09:23Z)
Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming [97.40955121478716]
本稿では,ネットワークアクティベーションの総数にのみ線形なメモリを必要とする一階二重SDPアルゴリズムを提案する。 L-inf の精度は 1% から 88% ,6% から 40% に改善した。また,変分オートエンコーダの復号器に対する2次安定性仕様の厳密な検証を行った。
論文参考訳（メタデータ） (2020-10-22T12:32:29Z)

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

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