Incompleteness of AI Safety Verification via Kolmogorov Complexity

• URL: http://arxiv.org/abs/2604.04876v1
• Date: Mon, 06 Apr 2026 17:26:09 GMT
• Title: Incompleteness of AI Safety Verification via Kolmogorov Complexity
• Abstract summary: We show that limitations of verification arise from intrinsic information-theoretic limits.<n>No finite formal verifier can certify all policy-compliant instances of arbitrarily high complexity.
• Score: 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.

Related papers

• CLAIM: Leading Open-domain Active Clarification of Large Language Models with Uncertainty Measurement [50.91045324738942]
  CLAIM is an uncertainty-driven framework for active clarification learning in open-domain settings.<n>We propose an entropy-driven synthetic data generation pipeline that integrates uncertainty estimation with semantic clustering and reasoning-based judgments.<n> Experimental results demonstrate that CLAIM can learn stable and generalizable clarification strategies without relying on manually labeled data.
  arXiv  Detail & Related papers  (2026-08-12T04:27:45Z)
• Verification of Robust Properties for Access Control Policies [51.736723807086385]
  Existing methods for verifying access control policies require the policy to be complete and fully determined before verification can proceed.<n>We introduce robust property verification: the problem of determining what a policy's structure commits it to regardless of how pending decisions are resolved and regardless of subsequent extension.<n>We show that despite quantifying universally over all possible policy extensions the judgment reduces to proof search in a second-order logic programming language.
  arXiv  Detail & Related papers  (2026-03-13T17:14:38Z)
• On the Formal Limits of Alignment Verification [0.24049560288708582]
  A foundational question for AI safety is whether alignment can be formally certified.<n>We prove that no verification procedure can simultaneously satisfy three properties: soundness (no misaligned system is certified), generality (verification runs in time), and tractability.<n>The result follows from three independent barriers: the computational complexity of full-domain neural network verification, the non-identifiability of internal goal structure from behavioral observation, and the limits of finite evidence for properties defined over infinite domains.
  arXiv  Detail & Related papers  (2026-03-08T23:03:21Z)
• Frontier AI Auditing: Toward Rigorous Third-Party Assessment of Safety and Security Practices at Leading AI Companies [57.521647436515785]
  We define frontier AI auditing as rigorous third-party verification of frontier AI developers' safety and security claims.<n>We introduce AI Assurance Levels (AAL-1 to AAL-4), ranging from time-bounded system audits to continuous, deception-resilient verification.
  arXiv  Detail & Related papers  (2026-01-16T18:44:09Z)
• Generalized Security-Preserving Refinement for Concurrent Systems [36.14488865240512]
  We present a refinement-based compositional approach to prove that IFS properties are preserved between implementation and abstraction.<n>We apply our approach to verify two non-preserving case studies against a collection of security policies.
  arXiv  Detail & Related papers  (2025-11-10T09:06:01Z)
• "Show Me You Comply... Without Showing Me Anything": Zero-Knowledge Software Auditing for AI-Enabled Systems [2.2981698355892686]
  This paper introduces ZKMLOps, a novel MLOps verification framework.<n>It operationalizes Zero-Knowledge Proofs (ZKPs)-cryptographic protocols allowing a prover to convince a verifier that a statement is true.<n>We evaluate the framework's practicality through a study of regulatory compliance in financial risk auditing.
  arXiv  Detail & Related papers  (2025-10-30T15:03:32Z)
• The Alignment Trap: Complexity Barriers [0.0]
  This paper argues that AI alignment is not merely difficult, but is founded on a fundamental logical contradiction.<n>We first establish Theion Paradox: we use machine learning precisely because we cannot enumerate all necessary safety rules.<n>This paradox is then confirmed by a set of five independent mathematical proofs.
  arXiv  Detail & Related papers  (2025-06-12T02:30:30Z)
• Explainable Compliance Detection with Multi-Hop Natural Language Inference on Assurance Case Structure [1.5653612447564105]
  We propose a compliance detection approach based on Natural Language Inference (NLI)<n>We formulate the claim-argument-evidence structure of an assurance case as a multi-hop inference for explainable and traceable compliance detection.<n>Our results highlight the potential of NLI-based approaches in automating the regulatory compliance process.
  arXiv  Detail & Related papers  (2025-06-10T11:56:06Z)
• Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation [52.626086874715284]
  We introduce a novel problem formulation called Abstract DNN-Verification, which verifies a hierarchical structure of unsafe outputs.<n>By leveraging abstract interpretation and reasoning about output reachable sets, our approach enables assessing multiple safety levels during the formal verification process.<n>Our contributions include a theoretical exploration of the relationship between our novel abstract safety formulation and existing approaches.
  arXiv  Detail & Related papers  (2025-05-08T13:29:46Z)
• Safe Inputs but Unsafe Output: Benchmarking Cross-modality Safety Alignment of Large Vision-Language Model [73.8765529028288]
  We introduce a novel safety alignment challenge called Safe Inputs but Unsafe Output (SIUO) to evaluate cross-modality safety alignment.<n>To empirically investigate this problem, we developed the SIUO, a cross-modality benchmark encompassing 9 critical safety domains, such as self-harm, illegal activities, and privacy violations.<n>Our findings reveal substantial safety vulnerabilities in both closed- and open-source LVLMs, underscoring the inadequacy of current models to reliably interpret and respond to complex, real-world scenarios.
  arXiv  Detail & Related papers  (2024-06-21T16:14:15Z)
• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  We develop scalable formal verification algorithms without shifting the problem to unrealistic assumptions. In a pursuit of developing scalable formal verification algorithms without shifting the problem to unrealistic assumptions, we employ the concept of barrier certificates. We show how to solve the resulting program efficiently using sum-of-squares optimization and a Gaussian process envelope.
  arXiv  Detail & Related papers  (2024-03-15T17:32:02Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties. We propose a framework that jointly conducts reinforcement learning and formal verification.
  arXiv  Detail & Related papers  (2022-01-28T16:53:56Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.