Provable Bounds on AI Self-Improvement: The Verification Oracle Ceiling

We establish formally verified bounds on recursive AI self-improvement under a spectral coupling model. An AI system that iteratively trains on its own outputs generates a monotone improvement sequence \(K_0, K_1, K_2, \ldots\) of learnable modes, where mode \(k\) is learnable with \(N\) samples if \(N \cdot g(k) \geq 1\) for a positive decreasing coupling function \(g\). Our main results, all verified in Lean 4 with Mathlib:

(i) Ceiling Theorem. With fixed sample budget \(N\), the improvement sequence converges to a finite ceiling \(K^*(N)\). Self-improvement under fixed compute is provably bounded.

(ii) Divergence Theorem. With growing \(N\), no fundamental ceiling exists. For any target capability level \(K\), there exists a sufficient budget \(N\).

(iii) Rate Bound. The total number of learnable modes satisfies \(K \leq N \cdot \sum_{k<K} g(k)\).

(iv) Asymmetry. Per-step improvement is bounded, but cumulative improvement is unbounded. The wall is real but not permanent.

Under summable coupling — satisfied by Zipfian distributions governing natural language — the FOOM scenario (unbounded recursive self-improvement at fixed compute) is formally ruled out. The scaling exponent \(\alpha = 1/\beta\) connecting coupling decay to ceiling growth is formalized: for power-law \(g(k) \sim k^{-\beta}\), the ceiling grows as \(K^*(N) \sim N^{1/\beta}\). Calibrating to Chinchilla scaling data yields \(\beta \approx 3.25\), predicting that doubling compute grows the ceiling by only ~24%.

The verification oracle — an evaluator that can check but not generate solutions — is the bottleneck determining the ceiling. This maps directly to reward models (RLHF), constitutional evaluators (Constitutional AI), and formal proof checkers (automated theorem proving). All 51 declarations across 13 Lean 4 files are verified with zero sorry axioms.

One-sentence summary: Self-improvement has a ceiling that grows with compute — neither doom nor utopia, but a quantitative bound.