Verification and Self-Improvement in Agentic AI: Foundations and Limits

1 Introduction

• A deployed stage fixes the permitted verification procedures, interfaces, resource bounds, task relation, support, transcript exposure, and terminal checker.The framework concerns families indexed by input length, not a single checkpoint or benchmark score.Source: §1 · pp. 1–2
• Native reach uses default support, while the closure frontier includes accepted inputs under any support already permitted by the interface.More attempts can improve discovery without changing either set; making optional feedback routine can enlarge native reach, while admitting a previously forbidden transcript can enlarge the frontier.Source: §1 · p. 2
• A randomized checker needs both a pointwise probability gap and task-relative soundness; repeated evaluation cannot repair a systematically incorrect judge.The stated conditions exclude generic learned judges supported only by average accuracy.Source: §1 · pp. 1–2
• The framework separates search, support, and checker changes, and treats recursive self-improvement as subject to explicit correctness, evidence, resource, and selection-error obligations.Its complexity-theoretic depth obstructions are conditional, and its structural comparisons concern declared verification families rather than imposing a ceiling on open-ended improvement.Source: §1 · pp. 2–3

2 Preliminaries: the deterministic foundation

• A polynomially balanced task bounds the length of each valid encoded output but does not imply that correctness is polynomial-time decidable or that outputs are efficiently findable.Source: §2 · p. 3
• At fixed depth k, Σ_k^P membership is expressed by k alternating quantifier blocks over bounded strings and a deterministic polynomial-time predicate.Depth counts quantifier blocks; the universal-start version defines Π_k^P.Source: §2 · p. 3
• A polynomial-time terminal predicate does not make an alternating game efficiently executable when a quantified domain may contain exponentially many challenges.A sampled critic does not implement a universal quantifier; the classical randomized predicate background is tuple-level BPP verification.Source: §2 · pp. 3–4

3 Probabilistic stages and exact specialization

• A bounded probabilistic stage fixes its depth, length bounds, admissible support and transcripts, and uniform polynomial-time terminal checker.Support and transcript encodings are checked deterministically, and only the terminal core receives hidden random bits after all moves.Source: §3 · p. 4
• Every well-formed bounded tuple has terminal acceptance probability at most 1/3 or at least 2/3, and task-relative soundness separately connects quantified acceptance to task correctness.The gap and soundness are distinct: a confident checker can accept a false answer while satisfying the gap, and quantified soundness need not require every move tuple on every false output to reject.Source: §3 · pp. 4–5
• Native reach uses default support, whereas the closure frontier uses any support admitted by the declared interface.These are languages of task inputs, not accepted-patch sets or success probabilities; unmodeled oracle information cannot be treated as conservative support.Source: §3 · p. 5
• Randomized-verifier acceptance places the probability threshold inside the bounded quantifier formula, with pointwise-gap semantics and a distinct universal-start dual.At depth one, the framework gives NP ⊆ Σ_1^RV ⊆ MA; it does not assume equality with standard MA.Source: §3 · pp. 5–6
• An exact stage has zero terminal randomness, so its exact and probabilistic readings coincide and its native and frontier languages lie in Σ_k^P.Permitted support can be selected with the first existential move; exact checking removes only terminal randomness.Source: §3 · p. 6
• For any L0 ⊆ L1 in Σ_k^RV, a sound depth-k stage can represent that native/frontier pair; when both lie in Σ_k^P, the stage can be exact.This is a representation guarantee, not a method for learning a verifier or discovering a product’s exposure sets.Source: §3 · p. 6

4.1 False acceptance and amplification

• Existential acceptance over random tapes can strictly enlarge a sound depth-one stage’s frontier and admit inputs outside the task domain.A false answer may have a rare accepting tape while remaining below the bounded-error threshold.Source: §4.1 · p. 6
• Independent strict majority preserves the terminal decision map, quantified acceptance, native reach, and frontier while reducing pointwise error to at most e^-N/18.The repetitions use the same tuple, preserve object and move domains, and require independent runs; repeated candidate search and correlated judge calls are not covered.Source: §4.1 · p. 6

4.2 Classical placement and conditional comparisons

• Replacing the randomized terminal predicate by its classical alternating representation costs at most one extra quantifier block.Source: §4.2 · p. 7
• If Σ_1^RV ⊆ NP, some sound randomized depth-one stage has a frontier no exact depth-one stage can equal; if BPP = P, randomized stages have exact companions with the same frontiers.These are conditional class-level comparisons, not general nested-ring claims about the same physical checker.Source: §4.2 · p. 7

• Semantic authority compares quantified acceptance per transcript, not raw model accuracy, and requires both stages to be sound for the same task.Comparisons across encodings require a common transcript encoding or an explicit translation.Source: §5 · pp. 7–8
• A deterministic polynomial-time guard can reject records at either interface without changing native reach or the frontier.The two stages have the same languages with all other data fixed.Source: §5 · p. 8
• Refactoring can shift a raw authority change into an exposure change without changing accepted behavior or escaping the source frontier.Moving a guard from the core to the interface changes the component label, not the accepted behavior.Source: §5 · p. 8
• When target-native transcripts are source-exposed and target acceptance implies source acceptance, every target-native solution lies within the source frontier.Authority-preserving internalization of permitted support can enlarge native reach only within the old frontier; depth alone cannot produce escape under these premises.Source: §5 · p. 8
• Either a core change or an exposure change can produce frontier escape at fixed depth in exact and randomized stages.Separate constructions keep the other component fixed.Source: §5 · p. 8

• An exact depth-(k + 1) target can have a native language outside the frontier of every sound exact depth-k stage for its task.Source: §6 · p. 8
• A randomized depth-k stage cannot cover some exact depth-(k + 2) targets under the stated assumptions.The targets are separator families, and the theorem does not establish a sharp adjacent-level bound.Source: §6 · pp. 8–9
• A guarded language has an exact depth-one certificate representation when certificate acceptance is equivalent to passing every bounded challenge.The certificate checker and certificates must be polynomial-time and polynomially bounded, respectively.Source: §6 · p. 9
• Challenge replacement requires both checker soundness and short certificates for every accepted proposal; soundness alone gives containment, not equality.The paper cites equality of XOR circuits as a restricted family with an exact symbolic checker.Source: §6 · p. 9

7.1 Running task and three exact designs

• The exhaustive lookup checker and certificate design reject the incomplete patch and accept the full repair, while the sampled checker misses an error outside its four tested inputs.The example is finite and does not establish a complexity separation for general program repair.Source: §7.1 · p. 9

7.2 A controlled stochastic extension

• Three independent noisy checks with majority preserve the native and frontier sets, but existential acceptance over random tapes also accepts the incomplete patch.The controlled checker returns the exact result with probability 3/4 and its complement with probability 1/4; the example is not an empirical model of a learned judge.Source: §7.2 · p. 10

7.3 A growing family with an enforced interface

• The XOR family separates search gains from language changes: two full-support policies have an unbounded per-attempt success ratio, while quota changes can alter native reach and the frontier.At d = 6, the three configurations have (|L|, |F|) equal to (1, 42), (42, 42), and (57, 57); the general result follows from the proof, not these finite counts.Source: §7.3 · p. 11

7.4 Declaration protocol and disagreement rules

• The declaration protocol requires task and encoding details, stage and budget records, soundness evidence, comparison proofs, and an explicit audit status.Finite measurements can reveal counterexamples but do not generally prove uniform contracts on an infinite family.Source: §7.4 · pp. 11–12

8 Recursive self-improvement: agent changes and selection

• Self-improvement comparisons concern both the accepted tasks of a successor and how reliably selection identifies improvement; recursion alone establishes neither effectiveness nor a change in verification depth.Structural recursion and effective recursion are distinct, and empirical evidence within experimental settings is not a stage-contract or hierarchy-separation proof.Source: §8 · p. 13, §8.1 · p. 13

8.1 What recent systems make observable

• Recent systems vary prompts, memory, workflows, executable components, and meta-agents, making it necessary to record which component changes and which evaluation remains fixed.These reports provide empirical evidence within their settings, not stage-contract or hierarchy-separation proofs.Source: §8.1 · p. 13

8.2 Deployed stage, improver, and selection rule

• With jointly uniform admission, exposure, interpretation, common bounds, and soundness for every admitted candidate, bounded self-modification remains within the same verification class.The result does not cover an unbounded improvement process without a common resource bound; changing the envelope, interpreter, or quantifier protocol requires a new declaration.Source: §8.2 · pp. 14–15

8.3 Selection error across an adaptive improvement run

• For at most M selection calls, odd majority size N ≥18 log(M/δ) bounds total false-selection probability by δ when each invalid fixed candidate has per-trial false acceptance probability at most 1/3.The per-call conditional guarantee must be established for the improvement criterion separately from a deployed checker’s tuple-level gap.Source: §8.3 · pp. 15–16

9.1 A realizable bounded-error contract

• Two independent randomized matrix-product checks over F2 accept correct products with probability one and incorrect products with probability at most 1/4.The check uses quadratic field operations after the matrices are provided and is not a separation from deterministic polynomial time.Source: §9.1 · p. 16

9.2 Related work

• The framework’s hidden-terminal-coin model is positioned against bounded alternation and Arthur–Merlin systems, with a classical randomized hierarchy bound.Debate and proof certificates offer other approaches to bounded verification, but learned debaters do not automatically realize universal bounded challenges [7].Source: §9.2 · p. 16

9.3 Limitations

• The results classify declared protocol families, not latent intelligence, training dynamics, or the probability that a model discovers a solution.The pointwise-gap model leaves average-case judges, distribution shift, and correlated errors unresolved; finite audits do not empirically validate frontier claims for large deployed systems.Source: §9.3 · p. 17

10 Conclusion

• Native reach uses default support, whereas the frontier includes every support the interface already permits.Making optional support routine can enlarge native reach within the old frontier; escaping it requires a change to semantic authority or exposure containment.Source: §10 · p. 17
• Uniformly bounded self-modification under a common sound interpreter and fixed protocol remains in the same verification class, even if a successor escapes its predecessor’s frontier.A separate conditional-error budget controls false successor selections across adaptive candidate comparisons.Source: §10 · p. 17
• These results leave unbounded improvement processes outside their scope and frame stronger-verification claims as obligations on correctness, admissible evidence, resources, and selection error.Source: §10 · p. 17

AI tool use

• OpenAI’s Codex assisted with manuscript revision, literature synthesis, proof development and checking, and preparation of executable artifacts and figures; the author is responsible for the content.The scope of executable and formal checks is specified in Appendix C.Source: AI tool use · p. 17

A.1 Stage languages and deterministic recovery

• Default support is included among permitted supports, and exposure checks add no alternation; with no coins, the resulting language construction has a deterministic polynomial-time matrix.The appendix also constructs stages realizing a pair of languages through default and optional support.Source: §A.1 · pp. 19–20

A.2 False acceptance and majority amplification

• Existential acceptance over random tapes can accept every input through a rare lucky tape, while independent majority amplification preserves the pointwise gap and the induced languages.The cited tail bound gives error at most e^-N/18 for odd N.Source: §A.2 · p. 20

A.3 Hierarchy bounds and derandomization

• Under BPP = P, a uniform deterministic polynomial-time decider can replace the randomized matrix while retaining domain checks, quantified acceptance, and soundness.Source: §A.3 · p. 20

A.4 Guard-transfer invariance

• A move-independent Boolean guard can transfer between exposure and thresholded acceptance without changing the fused matrix or the resulting native and frontier membership.Source: §A.4 · p. 20

A.5 Depth obstructions and certificate substitution

• The depth-obstruction arguments use soundness and certificate substitution; soundness alone gives only the forward implication from certified to universal acceptance.The proof uses class containment and a forbidden equality to establish conditional coverage obstructions.Source: §A.5 · p. 21

A.6 Bounded self-modification and adaptive selection

• A single uniform verifier can absorb bounded candidate records without adding a quantifier block, provided its domain checks, soundness, and gap contracts hold.For adaptive selection, conditional error bounds sum across calls; countable budgets bound total error but do not imply uniform polynomial runtime for an infinite run.Source: §A.6 · p. 21

A.7 The quota-enforced XOR family

• The quota-enforced XOR family separates unbounded ratios of search success from changes in accepted languages, with both policies’ success probabilities zero below the correct program’s quota.When the correct program is admissible, the reported policy-mass ratio grows without bound as d increases.Source: §A.7 · pp. 21–22

A.8 The randomized matrix-product check

• For an incorrect matrix triple, one test has false-acceptance probability at most 1/2, and independent repetitions yield a pointwise bound of at most 1/4.Correct products pass every test, establishing the stated gap and task soundness.Source: §A.8 · p. 22

B.1 Simulation and support normalization

• Mutual simulation preserves native reach and frontier, and every stage has a representation with the same languages using just two support states.Source: §B.1 · p. 22

B.2 The local invariant of guard transfer

• The guard-transfer invariant factors through the conjunction of exposure and thresholded acceptance, but applies only to the specified refactoring family.It is not a completeness theorem for every representation change.Source: §B.2 · pp. 22–23

B.3 Separate same-depth escape constructions

• At the same depth, frontier escape can be realized by changing only the core or only exposure.The deterministic construction follows using exact verifiers.Source: §B.3 · p. 23

B.4 Finite chains of same-depth frontier expansion

• Any finite strict chain of languages in the randomized-verifier class can be realized with each transition changing only its labeled core or support component.The construction relies on a finite chain; it makes no uniform infinite-chain claim.Source: §B.4 · p. 23

C Finite verification and reproduction

• The finite audits compare the symbolic checker with exhaustive truth tables for d ≤ 4 and record exact language counts and proposal probabilities for d ≤ 6.The stated claim boundaries exclude using finite audits as evidence for complexity-class separation, learned-verifier calibration, or undeclared deployment frontiers.Source: C Finite verification and reproduction · p. 24

D Self-improvement mechanisms and comparative evidence

• The mechanism-level table gives reported designs alongside proposed connections to the stage model, which the paper frames as audit questions rather than established classifications.Source: D Self-improvement mechanisms and… · p. 24, Table 3 · p. 25

D.1 Comparing task improvement and improver improvement

• The RSI survey’s Headroom-Closed Index is not this paper’s closure frontier, and Hyperagents’ fixed task distribution and outer selection process delimit its reported recursion [1] [19].The survey’s post-2026 extension is explicitly illustrative [1].Source: §D.1 · pp. 25–26
• A fair improver comparison fixes the task relation, candidate grammar, evaluator, starting stage, and resource accounting, then measures held-out improvement against evaluation calls, tokens, and compute.A fixed generation count may not equalize cost when candidate runtimes differ; freezing the improver while continuing task-agent search separates search effort from search-procedure changes.Source: §D.1 · p. 26

D.2 Separating diagnosis, ranking, and acceptance

• Diagnostic feedback and ranking signals are distinct from successor-acceptance evidence; benchmark scores alone do not establish the conditional-error premise.Reused evaluation data can become effective search feedback even when evaluator code stays fixed.Source: §D.2 · p. 26