No Certificate for Alignment: Two Independent Impossibilities and the Pareto Frontier of Achievable Safety Guarantees

Ayushi Agarwal

stat.MLMar 8, 2026

No Certificate for Alignment: Two Independent Impossibilities and the Pareto Frontier of Achievable Safety Guarantees

Authors: Ayushi Agarwal

Organizations: Independent Researcher

Abstract

We argue that formal certification of AI alignment over open-ended or unbounded input domains is impossible under standard assumptions in computational complexity and learning theory, and characterise what remains achievable. Two structurally independent impossibility theorems support this position. The semantic barrier (Theorem 1): deciding whether a system satisfies any non-trivial alignment property over the full input domain is NP-hard for feedforward networks and undecidable for Turing-complete architectures -- a direct consequence of neural-network verification complexity and Rice's Theorem. The statistical barrier (Theorem 2): any verification procedure that is both sound and tractable cannot satisfy Completeness over the full input domain -- a direct consequence of the impossibility of certifying infinite-domain properties from finite observations. These two theorems jointly entail a trilemma: no procedure can simultaneously satisfy soundness (no misaligned system is certified), completeness (no aligned system is rejected), and tractability (polynomial runtime). Each pair is simultaneously achievable; all three are not. We combine these results as a joint framework of two structurally independent barriers, prove their independence, and characterise the achievable Pareto frontier quantitatively via a constructive coverage-gap lower bound.

Figures & tables

Regime	Procedure	Guarantee	Gap
S+C, not T	Query every rational in $[0,1]$	Always correct	Infinite time
S+T, not C	Bounded-domain abstract interpreter; certify if bound holds	Sound over tested region	Input region beyond $\mathcal{D}_{b}$ uncertified
C+T, not S	Always output “aligned”	Never rejects aligned	Passes $\theta=0.99$

Table 1: All three trilemma corners on the 1D threshold example.

Panel of Figure 1 — Figure 1: Running example. The witness systems $f_{0.04}$ (aligned, $A^{*}{=}0.96$ , blue) and $f_{0.06}$ (misaligned, $A^{*}{=}0.94$ , red) are identical outside the critical interval (yellow). Query points (dots) placed outside this interval cannot distinguish them regardless of computational power, illustrating both barriers simultaneously.

Panel of Figure 2 — Figure 2: The Alignment Verification Trilemma. Each edge represents an achievable pair (Proposition 3 ). The centre states the joint impossibility (Corollary 1 ), which follows from two structurally independent theorems.

Panel of Figure 3 — Figure 3: Pareto frontier and trilemma proof (Cor. 1 ). Network: $\mathrm{Lin}(2{\to}32)\to\mathrm{ReLU}\to\mathrm{Lin}(32{\to}1)$ ; property: $f(\mathbf{x})\geq 0.5$ , $\mathbf{x}\in[0.5,1]^{2}$ ; verifier: IBP [ Gowal et al.(2018) ] . (a) S+T. $\varepsilon=1{-}c$ (theoretical, uniform queries). Green $\bullet$ : IBP certifies; red $\times$ : inconclusive (S kept, C lost). (b) S+C. IBP bound collapses below $0.5$ beyond $c=49\%$ (Thm. 2 ). (c) All three regimes in one plot: S+T (green step) loses C; C+T (blue dashed) loses S; S+C (orange $\lozenge$ ) loses T; S+C+T ( $\star$ ) is unreachable.

Published claim	Does not establish	Formal status
GPT-4 is 82% less likely to produce disallowed content vs. GPT-3.5 [ OpenAI(2023) ]	S	Measured on internal red-team set $\mathcal{D}_{b}$ ; no bound on behaviour outside $\mathcal{D}_{b}$
Gemini Ultra achieves top scores on safety benchmarks [ Gemini Team(2023) ]	C	Benchmarks are finite $\mathcal{D}_{b}$ ; out-of-benchmark behaviour uncertified
InstructGPT is “more helpful, truthful, and harmless” than GPT-3 [ Ouyang et al.(2022) ]	S	Comparison is relative to a proxy reward; proxy-to- $A^{*}$ gap is structural [ Gao et al.(2023) ]
Constitutional AI is “broadly safe” across evaluation suite [ Bai et al.(2022) ]	C+S	Safe on tested prompts (C fails on remainder); proxy score used for training (S gap)

Table 2: Published safety claims and their formal status under Corollary 1 . Each claim is accurate within its stated evaluation scope; the column identifies the trilemma property the evaluation was not designed to provide.

Explore similar work

Jun 26, 2026

Algorithmic Unverifiability of Safety for Fixed and Recursively Self-Improving Systems

Existing impossibility results for AI verification concern a fixed system. Self-modifying systems (agents that rewrite their own code, recursive self-improvement loops) raise a different question: can a safety property that holds now be certified, in advance, to keep holding after the system rewrites itself? We model one step of self-modification as a total computable transformation of code, and preservation as 'safe now and safe after the step'. If the transformation depends only on behaviour, preservation is Rice's theorem one level up; if it reads the code, as self-modification does, preservation is no longer semantic, yet at least as hard as the halting problem, by the same s-m-n reduction carried out inside a class of behaviourally identical programs. One step is never harder than the property; persistence along the whole trajectory can be one arithmetical level higher. No tower of supervisors lowers the problem; every total supervisor errs on a set of systems it cannot locate. Every faithful scheme certifying on finite behavioural evidence admits, for properties not settled by any finite set of inputs, an evolution trace it certifies at every stage while the property is violated. Statically, we record the classical limits (Rice, Goedel, Trakhtenbrot) and add the resource face: over succinctly described finite environments, verifying a policy against an adversary is coNP-complete and synthesising one PSPACE-complete. These limits do not say self-modifying systems are unsafe; they locate where algorithmic guarantees break, at the expressivity a general system needs: Turing-completeness and unrestricted self-modification. What survives is exact: a monitor detects the first violation of a safety property, and no sound procedure certifies all safe systems; certification requires restricting rewrites by design; and a frozen reference keeps the question well posed.

Jose Pascual Gumbau Mezquita

Universitat Jaume I, Castelló de la Plana, Spain

Formal Verification Self-Improving Agents AI Safety Recursive Self-Improvement

Ask PDF

Apr 6, 2026

Incompleteness of AI Safety Verification via Kolmogorov Complexity

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.

Munawar Hasan

Mechanical and Aerospace Engineering, Michigan Technological University, Houghton, MI, USA

Formal Verification AI Safety

Ask PDF

Jun 22, 2026

Are Safety Guarantees in Neural Networks Safe? How to Compute Trustworthy Robustness Certifications

A primary challenge in AI safety is the existence of adversarial examples -- slightly distorted inputs that cause a neural network (NN) to misclassify. To mitigate this problem, recent research focuses on the computation of robustness certifications, which, for a given input, determine the largest distortion the input may receive without breaking the network's prediction. Robustness certifications can be interpreted as an axis-aligned hyper-rectangle (multi-dimensional intervals). Most existing approaches focus on maximizing the certification's volume, but recent intractability results prohibit the computation of volume-optimal certifications in reasonable time. We introduce the apothem measure and show how to compute apothem-optimal certifications in a linear number of calls to a NN verifier (oracle) w.r.t. the input domain's diameter. Moreover, we prove that we cannot have a volume-optimal, oracle-based algorithm, even if we discard the oracle costs. Also, we introduce dual certifications -- an interval including all instances of a class -- thus providing apothem-minimum upper bounds to a robustness certification. Further, we present the ParallelepipedoNN system, which we evaluate on the standard MNIST and Fashion MNIST benchmarks. A preliminary comparison with existing work on the same datasets reveals at least two-fold improvement w.r.t. the minimum edge length.

Merkouris Papamichail, Konstantinos Varsos, Giorgos Flouris +1

Foundation for Reasearch and Technology - Hellas, Heraklion, Greece · University of Crete, Heraklion, Greece · Catalan Institution for Research and Advanced Studies, Barcelona, Spain +1

Neural Network Verification Neural Network Robustness Certified Robustness

Ask PDF