論文の概要: Talking with Verifiers: Automatic Specification Generation for Neural Network Verification

• arxiv url: http://arxiv.org/abs/2603.02235v1
• Date: Fri, 13 Feb 2026 09:36:40 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-09 01:20:08.101409
• Title: Talking with Verifiers: Automatic Specification Generation for Neural Network Verification
• Title（参考訳）: 検証者と話す:ニューラルネットワーク検証のための自動仕様生成
• Authors: Yizhak Y. Elboher, Reuven Peleg, Zhouxing Shi, Guy Katz, Jan Křetínský,
• Abstract要約: 検証パイプラインに新しいコンポーネントを導入し、既存の検証ツールを幅広いドメインや仕様スタイルに適用できるようにします。 我々のフレームワークは、自然言語で仕様を定式化し、それを自動解析し、最先端のニューラルネットワーク検証と互換性のある形式的な検証クエリに変換する。 以上の結果から,この翻訳プロセスは,計算オーバーヘッドの少ないユーザに対して高い忠実性を維持しつつ,実際の高レベル要求への形式検証の適用性を著しく拡張することを示す。
• 参考スコア（独自算出の注目度）: 5.883923958146327
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Neural network verification tools currently support only a narrow class of specifications, typically expressed as low-level constraints over raw inputs and outputs. This limitation significantly hinders their adoption and practical applicability across diverse application domains where correctness requirements are naturally expressed at a higher semantic level. This challenge is rooted in the inherent nature of deep neural networks, which learn internal representations that lack an explicit mapping to human-understandable features. To address this, we bridge this gap by introducing a novel component to the verification pipeline, making existing verification tools applicable to a broader range of domains and specification styles. Our framework enables users to formulate specifications in natural language, which are then automatically analyzed and translated into formal verification queries compatible with state-of-the-art neural network verifiers. We evaluate our approach on both structured and unstructured datasets, demonstrating that it successfully verifies complex semantic specifications that were previously inaccessible. Our results show that this translation process maintains high fidelity to user intent while incurring low computational overhead, thereby substantially extending the applicability of formal DNN verification to real-world, high-level requirements.
• Abstract（参考訳）: ニューラルネットワーク検証ツールは現在、限られた仕様のみをサポートしており、通常は生の入力や出力に対する低レベルの制約として表現される。 この制限は、高いセマンティックレベルで自然に正しい要求が表現される様々なアプリケーションドメインにおける採用と実用性を著しく妨げます。 この課題は、人間の理解可能な特徴への明示的なマッピングを持たない内部表現を学習するディープニューラルネットワークの本質的な性質に根ざしている。 これを解決するために、我々は検証パイプラインに新しいコンポーネントを導入し、既存の検証ツールを幅広いドメインや仕様スタイルに適用することで、このギャップを埋める。 我々のフレームワークは、自然言語で仕様を定式化し、それを自動解析し、最先端のニューラルネットワーク検証と互換性のある形式的な検証クエリに変換する。 我々は、構造化データセットと非構造化データセットの両方に対するアプローチを評価し、これまでアクセス不能であった複雑なセマンティック仕様の検証に成功したことを示す。 以上の結果から,この変換プロセスは,計算オーバーヘッドの少ないユーザに対して高い忠実性を維持しつつ,実世界の高レベル要求への形式的DNN検証の適用性を著しく拡張することを示す。

関連論文リスト

• Neural Network Reprogrammability: A Unified Theme on Model Reprogramming, Prompt Tuning, and Prompt Instruction [57.19302613163439]
  モデル適応のための統一フレームワークとして,ニューラルネットワークの再プログラム可能性を導入する。 本稿では,4つの重要な側面にまたがる情報操作アプローチを分類する分類法を提案する。 残る技術的課題や倫理的考察も分析する。
  論文  参考訳（メタデータ） (2025-06-05T05:42:27Z)
• A Formally Verified Robustness Certifier for Neural Networks (Extended Version) [0.0]
  ニューラルネットワークは入力中の小さな摂動の影響を受けやすいため、それらが誤分類される。 グローバルなロバストニューラルネットワークは、入力の分類がそのような摂動によって変更できないことを証明するために機能を使用する。 本稿では,プログラムとその仕様,実装と検証に要する重要な設計決定について述べる。
  論文  参考訳（メタデータ） (2025-05-11T12:05:14Z)
• A General Framework for Property-Driven Machine Learning [1.0485739694839669]
  逆行訓練は,小摂動に対するロバスト性を向上させるために,$epsilon$-cubesで行うことができることを示す。 コンピュータビジョン以外の領域は、一般化された超矩形を通してより柔軟な入力領域の仕様を必要とすることがある。 本稿では,これら2つの補完的アプローチを,プロパティ駆動機械学習の単一フレームワークに組み込む方法について検討する。
  論文  参考訳（メタデータ） (2025-05-01T11:33:38Z)
• Formal Verification of Deep Neural Networks for Object Detection [1.947473271879451]
  ディープニューラルネットワーク(DNN)は、現実世界のアプリケーションで広く使われているが、エラーや敵攻撃に弱いままである。 この研究は形式的検証を、より複雑なエホブジェクト検出モデルの領域に拡張する。
  論文  参考訳（メタデータ） (2024-07-01T13:47:54Z)
• VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees [3.208888890455612]
  VNN(Verification-Friendly Neural Networks)を生成するための新しいフレームワークを提案する。 本稿では,予測性能と検証親和性とのバランスをとるための学習後最適化フレームワークを提案する。
  論文  参考訳（メタデータ） (2023-12-15T12:39:27Z)
• On the verification of Embeddings using Hybrid Markov Logic [2.113770213797994]
  本稿では,学習した表現の複雑な性質を検証するためのフレームワークを提案する。 このフレームワーク内のプロパティのパラメータを学習するためのアプローチを提案する。 本稿では,グラフニューラルネットワーク,深部知識追跡,知能学習システムにおける検証について述べる。
  論文  参考訳（メタデータ） (2023-12-13T17:04:09Z)
• Privacy-preserving machine learning with tensor networks [37.01494003138908]
  テンソルネットワークアーキテクチャは、特にプライバシー保護機械学習に期待できる特性を持つことを示す。 まず、フィードフォワードニューラルネットワークに存在する新たなプライバシ脆弱性を説明し、それを合成および実世界のデータセットで説明する。 このような条件がテンソルネットワークアーキテクチャによって満たされていることを厳密に証明する。
  論文  参考訳（メタデータ） (2022-02-24T19:04:35Z)
• A Lightweight, Efficient and Explainable-by-Design Convolutional Neural Network for Internet Traffic Classification [9.365794791156972]
  本稿では、インターネットトラフィック分類のための新しい軽量・効率的・eXplainable-by-design畳み込みニューラルネットワーク(LEXNet)を提案する。 LEXNetは(軽量で効率の良い目的のために)新しい残留ブロックと(説明可能性のために)プロトタイプ層に依存している。 商用グレードのデータセットに基づいて、LEXNetは最先端のニューラルネットワークと同じ精度を維持することに成功した。
  論文  参考訳（メタデータ） (2022-02-11T10:21:34Z)
• Deep Speaker Embeddings for Far-Field Speaker Recognition on Short Utterances [53.063441357826484]
  深層話者埋め込みに基づく話者認識システムは,制御条件下での大幅な性能向上を実現している。 制御されていない雑音環境下での短い発話に対する話者検証は、最も困難で要求の高いタスクの1つである。 本稿では,a)環境騒音の有無による遠距離話者検証システムの品質向上,b)短時間発話におけるシステム品質劣化の低減という2つの目標を達成するためのアプローチを提案する。
  論文  参考訳（メタデータ） (2020-02-14T13:34:33Z)

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

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