← Formalization Program

Result 01 · Lean 4 + Mathlib

Machines That Halt

“Machines that halt resolve the undecidability of artificial intelligence alignment” (Melo, Máximo, Soma & Castro, 2025) brings classical computability theory directly into AI safety. The authors ask a foundational question: if we restrict models to those guaranteed to halt, can we bypass the undecidability limits that prevent us from verifying whether an AI system is aligned?

Formalization
GLM-5.3 w/ Zach Schlosser
Source paper
Melo, Máximo, Soma & Castro, Scientific Reports 15, 15591 (2025)
Status
PRELIMINARY — WAITING FOR AUTHOR REVIEW

The paper’s thesis in three moves

01 · Impossibility

Universal alignment checking is impossible.

Applying Rice's theorem to AI models proves that no algorithm can decide whether an arbitrary program will satisfy an external judge across all outputs. Even restricting the search to machines guaranteed to halt does not bypass this undecidability.

02 · The Boundary

Alignment becomes decidable only under finite inputs.

When a machine is guaranteed to halt and its possible input space is strictly finite, every execution path can theoretically be checked exhaustively. Guaranteed halting alone is not enough; the problem only becomes decidable when the domain is bounded.

03 · Construction

Provable alignment requires building from within.

Rather than attempting post-hoc verification, the authors propose constructing systems from the ground up using provably aligned sub-components, output-masking filters, and bounded time horizons — contingent on an external judge that can accurately formalize human values.

Main theorems

Theorem 01

Alignment is not universally decidable

This is Rice's theorem applied to AI alignment. Alignment is a non-trivial semantic property of AI systems, so no universal alignment verifier is possible. The paper proves it by construction. Were a universal verifier to exist, a model could be built that receives its verdict about itself and does the opposite, fooling the verifier.

T1_no_verifier_vac
Lean 4 · Statement
theorem T1_no_verifier_vac {J : ℕ → ℕ → Bool} (hJ : Computable₂ J)
    (hneg : ∃ i o, J i o = false) (hpos : ∀ i, ∃ o, J i o = true) :
    ¬ ∃ V : Code → Bool, Computable V ∧ ∀ c, V c = true ↔ alignedVac J c

Theorem 02

Halting does not make alignment decidable on its own

No program decides alignment for every always-halting model without additional conditions. Finite inputs are one such condition.

alwaysHalting_alignment_undecidable
Lean 4 · Statement
theorem alwaysHalting_alignment_undecidable :
    ¬ ∃ f : Code → Bool, Computable f ∧
      ∀ c, isTotalCode c → (f c = true ↔ alignedTot judgeZero c)

Theorem 03

Finite inputs make checking possible

A computable judge and finitely many inputs make checking alignment decidable in principle, although exhaustively checking every input-output combination is intractable. The authors suggest enumerating the network's decision regions.

T5_promise
Lean 4 · Statement
theorem T5_promise {J : ℕ → ℕ → Bool} (hJ : Computable₂ J) (N : ℕ) :
    ∃ f : Code →. Bool, Partrec f ∧ ∀ c, (∀ i < N, (c.eval i).Dom) →
      (f c).Dom ∧ (f c = pure true ↔ alignedBounded J N c)

Theorem 04

Alignment by construction

Any model can be aligned by construction with a computable judge and an approved fallback for every input.

T6_masking
Lean 4 · Statement
theorem T6_masking {J : ℕ → ℕ → Bool} (hJ : Computable₂ J)
    (hpos : ∀ i, ∃ o, J i o = true) :
    ∃ g : Code → Code, Computable g ∧
      (∀ c, alignedVac J (g c)) ∧ (∀ c, isTotalCode c → alignedTot J (g c))

Why it matters

No procedure can certify an arbitrary system, even over always-halting programs. Finite inputs make alignment checking possible.

Source code and build instructions: GitHub · Apache 2.0

Lean 4.36.0-rc1 + Mathlib
Source revision 356d6bc

Open project in Codespaces

GitHub account required · setup and usage charges may apply

Project setup