On the Impossibility of Universal LLM Halting Prediction

As large language models are proposed for fact-checking and for detecting machine-written text, a tempting goal comes into view: a single, trusted program that reads any text and returns a verdict on whether it is true and on whether a machine or a person wrote it. This paper asks whether such a universal judge can exist at all, setting aside accuracy on benchmarks and asking the sharper question of infallibility on every possible input.

The setting is deliberately austere. An LLM is modeled simply as a partial computable function G mapping prompts to outputs, identified with a Gödel index in a standard enumeration of Turing machines. Deterministic decoding is assumed, since randomness only makes prediction harder. Two judgment tasks are formalized precisely: authorship, deciding whether a given model on a given prompt produces a given string, and truth, deciding whether an encoded sentence is true in an intended model such as first-order arithmetic. The claim to be proven is that no total computable procedure can settle either task for all inputs.

The first two impossibility results are direct reductions from the Halting Problem. For authorship, the paper defines L_out as the set of triples where model m on prompt p halts with output x. This set is recursively enumerable: one simply simulates the model and accepts if it halts with the right output. But it is not decidable. Given any halting instance (e,w), one effectively builds a program m' that ignores its prompt, simulates φ_e(w), and emits a fixed string x_0 only if that simulation halts. Then the triple lies in L_out exactly when (e,w) halts, so deciding authorship would decide halting.

Truth judgment falls the same way. Because computable predicates are representable in arithmetic, the statement that φ_e(w) halts can be written as a Σ_1 sentence ∃t T(e,w,t), where T is primitive recursive and checks halting within t steps. That sentence is true precisely when the machine halts, so a computable truth predicate would again decide the Halting Problem. The paper notes this is equivalent to Tarski's undefinability of truth: no arithmetical truth predicate is computable.

Text-only AI detectors, which look only at the string and not at any generating model, are defeated by an argument so short it is almost disarming. If a total detector C ever labels some string y_0 as human-authored, then the constant generator that always outputs y_0 is a perfectly legitimate computable AI. It produces y_0, which the detector calls human. The detector errs. No universal, zero-error text-only detector can therefore accept any human writing without being foolable.

This theorem carries an unusually candid correction. An earlier version claimed the result for all total detectors unconditionally, which is false: the trivial detector that labels everything AI never suffers a false negative. The Lean formalization refused to discharge the proof obligation without the hypothesis that the detector labels at least one string human, surfacing the gap. The corrected statement is stronger in practice, since accepting some human text is a minimal requirement for a detector to be useful at all.

The sharpest result targets a meta-judge that attempts both tasks at once, returning a truth label and an authorship label for any text. Using the Kleene Recursion Theorem, the paper constructs from any such judge J a generator D_J that produces a single self-referential sentence S_J. The sentence, in effect, asserts of itself that it is not AI-generated and that its content is true, then queries J on itself and arranges its output so that whichever way J labels it, J is wrong — mislabeling either its authorship or its truth.

The recursion theorem guarantees the required fixed point exists, so the adversarial generator is genuinely constructible. The argument uses no probability: it defeats greedy and temperature-0 decoders exactly as it defeats any other, and probabilistic decoding only adds unpredictability. This is the paper's tightest statement of the thesis — not that judges are usually wrong, but that a single tailored instance breaks any total judge.

The paper confronts recent empirical work head-on. Sultan and colleagues report that frontier models score competitively with specialized verification tools on the SV-Comp 2025 Termination benchmark, and suggest undecidable problems may suit LLMs. The rebuttal is that two different questions are being conflated: whether one program decides halting for all inputs, versus whether a model scores well on a fixed, finite program set. Any finite set is trivially decidable by a lookup table; undecidability concerns the universal algorithm.

The diagonal makes this concrete. Given any model M used as a halting predictor, one builds a specific program D_M that does the opposite of M's own prediction on its own index, and M is provably wrong on it. That program is in no benchmark because it is built from M itself, so scaling, more data, and more test-time compute cannot fix it — the counterexample adapts to every improvement. The paper observes that even GPT-5 reaches only about 41% witness validity for non-termination proofs, precisely the prediction-versus-proof gap the theory predicts, and cites evidence that transformers fail to learn even decidable structural recursion, reinforcing that they act as heuristics rather than universal deciders.

The diagonal argument and its consequences are formalized in Lean 4 using Mathlib's computability library. The development includes an explicit construction of the diagonal program independent of Mathlib's built-in halting result, the propositional core that a proposition equivalent to its own negation is impossible, the fixed-point engine behind every such argument, the reduction defeating output oracles, the authorship undecidability slice, and the corrected human-accepting-detector theorem. All 11 theorems compile with zero warnings against Lean 4 v4.29.0.

The paper is careful about what it does not claim. It does not deny the value of restricted detectors or fact-checkers; it argues only that any practical system must be distribution-bounded and error-tolerant. For safety-critical use it points to provenance such as cryptographic signatures, constrained languages, and human oversight. It also separates itself from prior self-prediction impossibility results: those concern whether a model can predict its own output, whereas this work concerns an external meta-judge, and the two are complementary rather than the same. The bottom line is stated plainly — there is no path to a total, zero-error, distribution-agnostic universal judge, and these limits are as fundamental as the Halting Problem and Gödel incompleteness.