論文の概要: Incompleteness of AI Safety Verification via Kolmogorov Complexity

• arxiv url: http://arxiv.org/abs/2604.04876v1
• Date: Mon, 06 Apr 2026 17:26:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-07 15:49:19.309671
• Title: Incompleteness of AI Safety Verification via Kolmogorov Complexity
• Title（参考訳）: コルモゴロフ複雑度によるAI安全検証の不完全性
• Authors: Munawar Hasan,
• Abstract要約: 本研究は,本質的な情報理論の限界から検証の限界が生じることを示す。 任意の高複雑性のポリシーに準拠する全てのインスタンスを証明できる有限形式検証器は存在しない。
• 参考スコア（独自算出の注目度）: 0.20305676256390928
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Ensuring that artificial intelligence (AI) systems satisfy formal safety and policy constraints is a central challenge in safety-critical domains. While limitations of verification are often attributed to combinatorial complexity and model expressiveness, we show that they arise from intrinsic information-theoretic limits. We formalize policy compliance as a verification problem over encoded system behaviors and analyze it using Kolmogorov complexity. We prove an incompleteness result: for any fixed sound computably enumerable verifier, there exists a threshold beyond which true policy-compliant instances cannot be certified once their complexity exceeds that threshold. Consequently, no finite formal verifier can certify all policy-compliant instances of arbitrarily high complexity. This reveals a fundamental limitation of AI safety verification independent of computational resources, and motivates proof-carrying approaches that provide instance-level correctness guarantees.
• Abstract（参考訳）: 人工知能(AI)システムが正式な安全と政策上の制約を満たすことを保証することは、安全クリティカルドメインにおける中心的な課題である。 検証の限界はしばしば組合せ複雑性とモデル表現性に起因するが、本質的な情報理論の限界から生じることを示す。 我々は,ルールコンプライアンスを符号化されたシステム動作に対する検証問題として定式化し,Kolmogorov複雑性を用いて解析する。 固定音響計算可能検証器には、その複雑性がしきい値を超えると、真のポリシー準拠のインスタンスを認証できないしきい値が存在する。 したがって、任意の高複雑性のポリシーに準拠する全てのインスタンスを証明できる有限形式検証器は存在しない。 これは、計算リソースに依存しないAIの安全性検証の基本的な制限を明らかにし、インスタンスレベルの正確性を保証するための証明付きアプローチを動機付けている。

関連論文リスト

• Verification of Robust Properties for Access Control Policies [51.736723807086385]
  既存のアクセス制御ポリシーの検証方法は、検証が進む前に、ポリシーを完全かつ完全に決定する必要がある。 本稿では,政策構造がどのような決定を下すか,どのような決定を下すか,あるいはその後の拡張に拘わらず,その決定を行うかという課題について,ロバストなプロパティ検証を導入する。 可能なすべてのポリシー拡張を普遍的に定量化しているにもかかわらず、判断は二階述語論理プログラミング言語における探索の証明に還元されることを示す。
  論文  参考訳（メタデータ） (2026-03-13T17:14:38Z)
• On the Formal Limits of Alignment Verification [0.24049560288708582]
  AIの安全性に関する根本的な疑問は、アライメントが正式に認定されるかどうかである。 検証手順が3つの特性を同時に満たさないことを証明する。音性(不整合系が認定されない)、一般性(検証は時間内に実行される)、トラクタビリティである。 その結果、完全なニューラルネットワーク検証の計算複雑性、行動観察による内部目標構造の非識別性、無限領域上で定義された特性に対する有限証拠の限界という3つの独立した障壁が導かれる。
  論文  参考訳（メタデータ） (2026-03-08T23:03:21Z)
• Generalized Security-Preserving Refinement for Concurrent Systems [36.14488865240512]
  本稿では,IFS特性が実装と抽象化の間に保持されていることを証明するための改良型合成手法を提案する。 我々は,セキュリティポリシーの収集に対する2つの非保存ケーススタディを検証するために,我々のアプローチを適用した。
  論文  参考訳（メタデータ） (2025-11-10T09:06:01Z)
• The Alignment Trap: Complexity Barriers [0.0]
  本稿は、AIアライメントは単に難しいだけでなく、基本的な論理的矛盾に基づくものである、と論じる。 私たちは、すべての必要な安全ルールを列挙できないため、マシンラーニングを正確に使用しています。 このパラドックスは、5つの独立した数学的証明によって確認される。
  論文  参考訳（メタデータ） (2025-06-12T02:30:30Z)
• Explainable Compliance Detection with Multi-Hop Natural Language Inference on Assurance Case Structure [1.5653612447564105]
  自然言語推論(NLI)に基づくコンプライアンス検出手法を提案する。 保証ケースのクレーム・アビデンス・エビデンス構造をマルチホップ推論として定式化し、説明可能かつトレーサブルなコンプライアンス検出を行う。 本結果は,規制コンプライアンスプロセスの自動化におけるNLIベースのアプローチの可能性を強調した。
  論文  参考訳（メタデータ） (2025-06-10T11:56:06Z)
• Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation [52.626086874715284]
  我々は、安全でない出力の階層構造を検証する抽象的DNN検証と呼ばれる新しい問題定式化を導入する。 出力到達可能な集合に関する抽象的解釈と推論を活用することにより,形式的検証プロセスにおいて,複数の安全性レベルを評価することができる。 我々の貢献には、新しい抽象的安全性の定式化と既存のアプローチとの関係を理論的に探求することが含まれる。
  論文  参考訳（メタデータ） (2025-05-08T13:29:46Z)
• Safe Inputs but Unsafe Output: Benchmarking Cross-modality Safety Alignment of Large Vision-Language Model [73.8765529028288]
  我々は、モダリティ間の安全アライメントを評価するために、セーフインプットとアンセーフアウトプット(SIUO)と呼ばれる新しい安全アライメントの課題を導入する。 この問題を実証的に調査するため,我々はSIUOを作成した。SIUOは,自己修復,違法行為,プライバシー侵害など,9つの重要な安全領域を含むクロスモダリティベンチマークである。 以上の結果から, クローズドおよびオープンソース両方のLVLMの安全性上の重大な脆弱性が明らかとなり, 複雑で現実的なシナリオを確実に解釈し, 応答する上で, 現行モデルが不十分であることが示唆された。
  論文  参考訳（メタデータ） (2024-06-21T16:14:15Z)
• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  問題を非現実的な仮定にシフトすることなく,スケーラブルな形式検証アルゴリズムを開発する。 問題を非現実的な仮定にシフトさせることなく,スケーラブルな形式検証アルゴリズムを開発するためには,バリア証明書の概念を用いる。 本稿では,2乗法最適化とガウス過程エンベロープを用いて効率よくプログラムを解く方法を示す。
  論文  参考訳（メタデータ） (2024-03-15T17:32:02Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。 本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
  論文  参考訳（メタデータ） (2022-01-28T16:53:56Z)

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

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