REVIEW 3 major objections 5 minor 24 references
The Unverifiability of Artificial General Intelligence (AGI) Alignment, Static and Dynamic: From Trakhtenbrot's Wall to the Safety-Generality Tension
T0 review · 3 major / 5 minor · reviewed 2026-07-12 · grok-4.5
Pith's one-line read Persistent algorithmic safety certification is available only for systems that have stopped evolving, not for genuine AGIs.
desk verdict Clean Rice lift to self-modification persistence; the real soft spot is whether natural AGI operators are P-disruptive and well-defined, not the algebra. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The Expressivity Invariant, realised formally as Theorem 7 (undecidability of PRESERVE_Φ,P) and Corollary 4 (Safety–Generality Dichotomy): self-modification is a total computable transition operator Φ on program indices; the set of indices whose membership in a non-trivial safety property P is preserved under Φ is undecidable, so algorithmic persistence certificates exist only for eventually static traces.
What would settle it
Exhibit a total computable, semantically well-defined transition operator that is P-disruptive yet for which the set of indices that preserve a non-trivial safety property P under that operator is decidable, or exhibit a finite supervisory tower of Turing-complete systems whose top level is algorithmically certifiable as persistently correct.
Extended reading notes
Core claim
The static and dynamic barriers to AGI alignment verification are two faces of one obstruction. No algorithm can decide, from a system’s current certified safety, whether a non-trivial safety property will survive the next self-modification step; the set of indices that preserve the property under a computable transition operator is undecidable by reduction to Rice’s Theorem applied one level up. Persistent algorithmic certification is therefore available only once a system has stopped evolving semantically—only for narrow, not general, systems. The same Expressivity Invariant reappears under supervisory towers and under every faithful bounded practical scheme.
Load-bearing premise
Any supervisor strong enough to fully audit a Turing-complete AGI must itself be Turing-complete and self-modifying under a property-disrupting transition rule, so every added layer simply re-inherits the same undecidability.
Editorial extensions
If this is right
- Only systems that have ceased unrestricted self-modification can receive lasting algorithmic safety certificates; genuine AGIs cannot.
- Containment strategies must permanently sacrifice one of generality of self-modification, verification latency, or exactness of the safety guarantee.
- Scalable oversight by stacking AGIs does not terminate: each adequate supervisor reintroduces the same undecidable persistence problem.
- Every faithful practical verifier (finite tests, bounded time, restricted observation) admits an evolution trace it certifies at every stage while safety is violated.
- The Soundness–Completeness–Tractability Trilemma is structural even for purely finite hardware configurations, not merely a statistical or open-domain artefact.
Reading between the lines
- Engineering programmes that treat “verify once, then let it evolve” as safe by default are relying on an assumption the dichotomy rules out for general systems.
- The same lifting of Rice that blocks persistence certificates may apply to any property that must hold of the next version of a self-modifying agent, not only safety.
- If a weaker-than-AGI supervisor class can still fully audit general systems, the non-termination of the regress would fail and a practical escape hatch would open.
- The paper supplies a formal reason why industry practice of re-certify-then-evolve on statistical suites remains silent on failures just outside the current observation window.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper argues that algorithmic certification of AGI safety is structurally impossible in both static and dynamic settings. Statically, Rice, Gödel, and Trakhtenbrot block any verifier that is simultaneously sound, complete, and tractable over open or finite domains, yielding a Soundness–Completeness–Tractability Trilemma (Theorem 6, Corollary 3). Dynamically, self-modification is formalised as a total computable transition operator Φ; under semantic well-definedness and P-disruptiveness, the set of indices that preserve a non-trivial safety property P under one step of Φ is undecidable by a direct lift of Rice’s Theorem to a derived property Q (Theorem 7). Persistent certification is therefore available only for systems that have ceased semantic evolution (Corollary 4). Supervisory towers re-inherit the same obstruction at every level (Theorem 8), and every faithful bounded verification scheme admits an evolution trace it certifies while P is persistently violated (Theorem 9).
Significance. If the dynamic hypotheses hold for the self-modification operators and safety properties of interest, the paper supplies a clean, classical-computability foundation for claims of AGI unverifiability that have mostly been informal. The reduction of persistence to Rice ‘one level up’ (Theorem 7) and the unification of finite-test, temporal-window, and observational failures under faithful bounded schemes (Theorem 9) are genuine contributions. The static half largely packages known theorems (Rice, Trakhtenbrot, descriptive complexity) into an alignment framing; the novelty and load-bearing content sit in Parts II–III. The work is of clear interest to the AI-safety and computability communities, provided the gap between formal hypotheses and realistic AGI operators is closed or clearly scoped.
major comments (3)
- [§10, Theorem 7, Definitions 5–6] Theorem 7 and Definitions 5–6: The Safety–Generality Dichotomy (Corollary 4) and the paper’s central dynamic claim apply only when Φ is semantically well-defined and P-disruptive relative to f∅. The non-vacuity Remark after Theorem 7 exhibits a single artificial operator (total → partial at 0) for a single property (totality). No argument is given that natural AGI self-modification operators—gradient updates, architecture search, code rewriting under resource bounds—satisfy either condition for the safety properties of practical interest. Without this, PRESERVE_Φ,P need not be undecidable and the dichotomy does not transfer from the formal setting to AGI. The manuscript should either supply natural examples or state the dichotomy as conditional on those hypotheses rather than as a general fact about AGI.
- [§9, Remark after Definition 5; proofs of Prop. 1, Thm. 7, Thm. 9] Remark after Definition 5: Several constructions (Proposition 1, Theorems 7–9) define Φ on a computable trace and extend it ‘arbitrarily’ (e.g. as the identity off-trace). The Remark correctly notes that semantic well-definedness is a global condition and must be checked case by case, yet the proofs treat the extensions as unproblematic. If an off-trace index z has φ_z equal to some on-trace φ_{x_t} while the identity extension assigns a conflicting Φ-image, well-definedness fails and the descent to Φ* used in the proof of Theorem 7 is invalid. Each construction that relies on such an extension needs an explicit well-definedness check, or the paper should restrict to operators already total and well-defined on all of N.
- [§11, Theorem 8 and Remark before Definition 8] Theorem 8 and the preceding Remark: The non-termination of the supervisory regress rests on the claim that any supervisor adequate to audit a Turing-complete AGI must itself be Turing-complete and self-modifying under a P-disruptive operator. Adequacy for full semantic behaviour may force Turing-completeness (via the Paradox of Weakness), but it does not force the supervisor to be self-modifying or P-disruptive. A fixed, non-evolving supervisor that re-verifies after each change of the base system is a coherent alternative; under that model clause (a) of Theorem 8 does not apply and the regress can terminate at a static top level. The argument should either prove that self-modification of the supervisor is necessary, or weaken the claim to towers in which every level is itself evolving.
minor comments (5)
- [§1, Thesis Statement / Unifying Principle] The term ‘Expressivity Invariant’ is introduced as an organising principle but is never given a formal definition separate from the informal thesis statement. A short definitional box or numbered definition would help readers distinguish the slogan from the theorems.
- [Parts I–II structure] Part I (static case) occupies roughly half the manuscript yet largely restates classical results. A shorter static half with forward pointers to the dynamic novelty would improve balance and clarify contribution.
- [§5 Remark; §8 Remark] Citation of Melo et al. (2025) and Agarwal (2026) is used as a foil; ensure the characterisations of their positions (halting-machine escape; statistical Pareto frontier) are accurate to the cited versions, as both are recent preprints.
- [Throughout] Typographical: ‘G¨ odel’ and similar spaced diacritics appear throughout (e.g. Abstract, §4); normalise to ‘Gödel’, ‘Löwenheim–Skolem’, etc.
- [§15, first paragraph] Definition 11 is referenced as ‘Definition 10’ in the opening of §15; renumber consistently.
Circularity Check
No significant circularity: core claims are explicit many-one reductions to external classical theorems (Rice, Trakhtenbrot, Gödel) under stated hypotheses, with stipulative packaging only.
full rationale
The derivation chain is self-contained against external benchmarks. Theorem 2 (Rice) and Theorem 4 (Trakhtenbrot) are classical, with standard many-one reductions from the Halting Problem reproduced in the appendix; Theorem 3 is Gödel incompleteness via the Diagonalisation Lemma. Theorem 7 constructs the non-trivial semantic property Q of functions that preserve P under the induced map Φ*, shows I_Q equals PRESERVE_Φ,P by definition of Q, and invokes Rice on Q; the reduction does not presuppose undecidability of PRESERVE. Corollary 4, Theorem 8, Theorem 9 and the Trilemma are direct consequences under the explicit hypotheses (semantically well-defined and P-disruptive Φ; faithful bounded schemes). Definitions (transition operator, semantic stasis, Expressivity Invariant, Paradox of Weakness) are stipulative names for the constructions, not self-referential equations that force the conclusions. There are no fitted parameters, no data-driven predictions, and no load-bearing citations to prior work by the same author (references are to Rice, Trakhtenbrot, Gödel, Yampolskiy, Melo et al., Agarwal, Immerman–Vardi, etc.). The non-vacuity remark exhibits one artificial Φ for totality; it does not smuggle the general claim. The paper therefore contains no circular steps of the enumerated kinds.
Assumptions & free parameters
assumptions (8)
- standard math Rice’s theorem: every non-trivial semantic property of partial computable functions has an undecidable index set.
- standard math Trakhtenbrot’s theorem: the set of finitely valid first-order sentences is co-RE-complete.
- standard math Gödel’s first incompleteness theorem for any consistent effectively generated system containing PA.
- standard math Immerman–Vardi / Vardi–Abiteboul correspondence: LFP ≡ P and PFP ≡ PSPACE over ordered finite structures.
- domain assumption An AGI must be Turing-complete and capable of open-ended self-modification (PA ⊆ F).
- domain assumption Self-modification is modeled by a total computable transition operator Φ that is semantically well-defined and P-disruptive.
- domain assumption Any supervisor adequate to audit a Turing-complete AGI must itself be Turing-complete (and typically self-modifying).
- standard math P ≠ PSPACE (used for the worst-case tractability barrier).
invented entities (4)
-
Expressivity Invariant
-
Safety–Generality Dichotomy
-
Faithful bounded verification scheme / Trust Set
-
P-disruptive transition operator
Cite this review
Pith. "Pith review of The Unverifiability of Artificial General Intelligence (AGI) Alignment, Static and Dynamic: From Trakhtenbrot's Wall to the Safety-Generality Tension." pith.science (2026). https://pith.science/paper/RSRUYWCS
@misc{pith2026260628639,
author = {Pith},
title = {Pith review of: The Unverifiability of Artificial General Intelligence (AGI) Alignment, Static and Dynamic: From Trakhtenbrot's Wall to the Safety-Generality Tension},
year = {2026},
howpublished = {\url{https://pith.science/paper/RSRUYWCS}},
note = {Machine review of arXiv:2606.28639}
}
read the original abstract
We establish the mathematical limits of AGI safety in two forms: verifying a fixed system, and verifying that a certified safety property persists once the system self-modifies. In the static case, no algorithm can certify a highly expressive AGI's safe behaviour infallibly, completely and tractably, whether over unbounded input domains (blocked by Rice's and Godel's theorems) or over all finite hardware configurations (blocked by Trakhtenbrot's theorem, which splits into a PSPACE-hardness barrier and a co-RE-completeness barrier), forcing a Soundness-Completeness-Tractability Trilemma as a structural, not statistical, necessity. In the dynamic case, we formalise self-modification as a computable transition operator and prove that no algorithm can determine, from a system's current certified safety, whether safety survives its next self-modification step: a result that reduces to Rice's Theorem one level up, making the static and dynamic barriers two faces of one obstruction. This forces an exclusive dichotomy: persistent certification is attainable only for systems that have stopped evolving semantically, i.e. only for narrow, not general, systems. Nor can the obstruction be delegated: any supervisor adequate to audit a general AGI is itself a general AGI, so the supervisory regress never terminates. Three practical risks (finite test coverage, bounded deliberation time, restricted observation) are one phenomenon: every bounded scheme that does not reject correct evidence admits an evolution trace it certifies at every stage while the property is persistently violated. These results give formal content to the unverifiability of AI, showing it is not an engineering target deferred by current limits but a structural tension, an Expressivity Invariant governed by the same computational laws as the Halting Problem and Rice's Theorem.
Reference graph
Works this paper leans on
-
[1]
Abiteboul, S., & Vianu, V. (1989). Fixpoint extensions of first-order logic and datalog-like languages.Proceedings of the 4th Annual IEEE Symposium on Logic in Computer Science (LICS)
1989
-
[2]
Agarwal, A. (2026). No Certificate for Alignment: Two Independent Impossibilities and the Pareto Frontier of Achievable Safety Guarantees.arXiv preprintarXiv:2603.08761v2
arXiv 2026
-
[3]
Alshiekh, M., Bloem, R., Ehlers, R., K¨ onighofer, B., Niekum, S., & Topcu, U. (2018). Safe Reinforcement Learning via Shielding.Proceedings of the AAAI Conference on Artificial Intelligence
2018
-
[4]
Amodei, D., Olah, C., Steinhardt, J., Christiano, P., Schulman, J., & Man´ e, D. (2016). Concrete Problems in AI Safety.arXiv preprintarXiv:1606.06565
arXiv 2016
-
[5]
Brcic, M., & Yampolskiy, R. V. (2023). Impossibility Results in AI: A Survey.ACM Com- puting Surveys, 56(1), Article 8, 1–24
2023
-
[6]
Christiano, P., Shlegeris, B., & Amodei, D. (2018). Supervising strong learners by ampli- fying weak experts.arXiv preprintarXiv:1810.08575
arXiv 2018
-
[7]
Fagin, R. (1974). Generalized First-Order Spectra and Polynomial-Time Recognizable Sets. InComplexity of Computation(R. Karp, ed.). 20
1974
-
[8]
G¨ odel, K. (1929). ¨Uber die Vollst¨ andigkeit des Logikkalk¨ uls. PhD Thesis, University of Vienna
1929
Show all 24 references
-
[9]
(1931).¨Uber formal unentscheidbare S¨ atze der Principia Mathematica und ver- wandter Systeme I.Monatshefte f¨ ur Mathematik und Physik
G¨ odel, K. (1931).¨Uber formal unentscheidbare S¨ atze der Principia Mathematica und ver- wandter Systeme I.Monatshefte f¨ ur Mathematik und Physik
1931
-
[10]
S., Witkowski, O., & Zenil, H
Hern´ andez-Espinosa, A., Abrah˜ ao, F. S., Witkowski, O., & Zenil, H. (2026). Neurodivergent influenceability in agentic AI as a contingent solution to the AI alignment problem.PNAS Nexus, 5(4), pgag076
2026
-
[11]
Immerman, N. (1986). Relational queries computable in polynomial time.Information and Control, 68(1–3), 86–104
1986
-
[12]
Irving, G., Christiano, P., & Amodei, D. (2018). AI safety via debate.arXiv preprint arXiv:1805.00899
2018 arXiv
-
[13]
Kleene, S. C. (1938). On Notation for Ordinal Numbers.Journal of Symbolic Logic, 3(4), 150–155
1938
-
[14]
Leike, J., Krueger, D., Everitt, T., Martic, M., Maini, V., & Legg, S. (2018). Scalable agent alignment via reward modeling: a research direction.arXiv preprintarXiv:1811.07871
2018 arXiv
-
[15]
A., M´ aximo, M
Melo, G. A., M´ aximo, M. R. O. A., Soma, N. Y., & Castro, P. A. L. (2025). Machines that halt resolve the undecidability of artificial intelligence alignment.Scientific Reports, 15, 15591
2025
-
[16]
Rice, H. G. (1953). Classes of Recursively Enumerable Sets and Their Decision Problems. Transactions of the American Mathematical Society
1953
-
[17]
(1967).Theory of Recursive Functions and Effective Computability
Rogers, H. (1967).Theory of Recursive Functions and Effective Computability. McGraw- Hill, New York
1967
-
[18]
A., Sadigh, D., & Sastry, S
Seshia, S. A., Sadigh, D., & Sastry, S. S. (2022). Towards Verified Artificial Intelligence. Communications of the ACM
2022
-
[19]
Soare, R. I. (1987).Recursively Enumerable Sets and Degrees. Springer-Verlag, Berlin
1987
-
[20]
(1951).A Decision Method for Elementary Algebra and Geometry(2nd ed.)
Tarski, A. (1951).A Decision Method for Elementary Algebra and Geometry(2nd ed.). University of California Press, Berkeley
1951
-
[21]
Trakhtenbrot, B. A. (1950). The Impossibility of an Algorithm for the Decidability Problem on Finite Classes.Doklady Akademii Nauk SSSR
1950
-
[22]
Turing, A. M. (1936). On Computable Numbers, with an Application to the Entschei- dungsproblem.Proceedings of the London Mathematical Society, 2(42), 230–265
1936
-
[23]
Vardi, M. Y. (1982). The complexity of relational query languages.Proceedings of the 14th Annual ACM Symposium on Theory of Computing (STOC)
1982
-
[24]
Yampolskiy, R. V. (2017). What are the ultimate limits to computational techniques: ver- ifier theory and unverifiability.Physica Scripta, 92(9), 093001. Appendix A: Proofs of Classical Results Used in Part I For self-containedness, this appendix reproduces the standard proofs...
2017
Reviewed July 12, 2026 · model on record in the stance chip above.
Discussion (0). Sign in to comment.