4 ms·

Total languages do not escape the halting problem – a trinary proof sketch

4 points by user1138 8mo ago

user1138 8mo ago
The formal verification and AI safety literature frequently cite total languages as a solution to the halting problem. This paper argues that this claim relies on a binary reduction of a trinary problem. While total languages provide an exit proof (halting), they cannot provide a correct-exit proof without step-by-step verification, which is itself the halting problem. Using Rice’s Theorem (1953) and Turing’s second proof (1936), I demonstrate that "early termination"—halting at an unintended point with incorrect output—is a non-trivial semantic property and therefore undecidable. The safety guarantees currently being marketed are often just tautologies where "termination" has been swapped for "safety". No novel math here—just a careful reading of the foundational proofs we’ve had for decades.
WCSTombs 8mo ago
First, who is saying "termination implies safety"? There need to be a citations for that, so we can know what specific claim is supposedly being refuted here. Second, Rice's theorem states that no nontrivial property on the set of partial recursive functions is decidable. However, there are subsets of the set of all recursive functions that do have decidable properties, and it's pretty trivial to cook some of them up. Since some of these sub-languages also consist only of total functions, there are "total languages" for which the analogous statement of Rice's theorem is false. To fix this we would need to choose a specific total language. There could be some interesting ones for which the analogous statement of Rice's theorem still holds, but I'm not an expert on that.
- user1138 8mo ago
  While I do have a formal citations there is this https://venturebeat.com/ai/lean4-how-the-theorem-prover-works-and-why-its-the-new-competitive-edge-in https://venturebeat.com/ai/lean4-how-the-theorem-prover-work...
  - WCSTombs 8mo ago
    Not only is this just a random article from the internet, as opposed to something peer-reviewed, but more importantly, nowhere does it even attempt to claim that the mere fact of a program terminating implies its suitability in a safety context.
    - user1138 8mo ago
      Here's your citation — ARIA's Safeguarded AI program, £59M in UK government funding, explicitly claiming mathematical safety guarantees through restricted verifiable models — total languages by another name. The claim exists. It has a budget. Now, do you have a substantive response to the proof, or are we done here?" @techreport{ARIA2024, author = {{Advanced Research and Invention Agency}}, title = {Safeguarded AI: Constructing Guaranteed Safety}, institution = {ARIA}, year = {2024}, url = {https://www.aria.org.uk/programs/safeguarded-ai/ https://www.aria.org.uk/programs/safeguarded-ai/}, abstract = {Outlines a 'Safeguarded AI' program that seeks to build AI systems with 'mathematical guarantees.' It argues that by using restricted, verifiable models—effectively total languages—one can avoid the 'impossible' task of verifying general AI and instead produce 'quantitative safety guarantees.'} }
- user1138 8mo ago
  You're correct on the citations though that will probably be very easy as we have many people claiming exactly that. As to your second point, yes, and the safety claims being made are not restricted to those decidable subsets. The moment you claim general safety guarantees for systems operating beyond those constrained subsets you're back in full Rice territory. If you can name a total language with an early termination guarantee, I'm all ears. You asked for my citations, now show me yours.

4 points by user1138 8mo ago

The formal verification and AI safety literature frequently cite total languages as a solution to the halting problem. This paper argues that this claim relies on a binary reduction of a trinary problem. While total languages provide an exit proof (halting), they cannot provide a correct-exit proof without step-by-step verification, which is itself the halting problem. Using Rice’s Theorem (1953) and Turing’s second proof (1936), I demonstrate that "early termination"—halting at an unintended point with incorrect output—is a non-trivial semantic property and therefore undecidable. The safety guarantees currently being marketed are often just tautologies where "termination" has been swapped for "safety". No novel math here—just a careful reading of the foundational proofs we’ve had for decades.

WCSTombs 8mo ago

First, who is saying "termination implies safety"? There need to be a citations for that, so we can know what specific claim is supposedly being refuted here. Second, Rice's theorem states that no nontrivial property on the set of partial recursive functions is decidable. However, there are subsets of the set of all recursive functions that do have decidable properties, and it's pretty trivial to cook some of them up. Since some of these sub-languages also consist only of total functions, there are "total languages" for which the analogous statement of Rice's theorem is false. To fix this we would need to choose a specific total language. There could be some interesting ones for which the analogous statement of Rice's theorem still holds, but I'm not an expert on that.

user1138 8mo ago
While I do have a formal citations there is this https://venturebeat.com/ai/lean4-how-the-theorem-prover-works-and-why-its-the-new-competitive-edge-in https://venturebeat.com/ai/lean4-how-the-theorem-prover-work...
- WCSTombs 8mo ago
  Not only is this just a random article from the internet, as opposed to something peer-reviewed, but more importantly, nowhere does it even attempt to claim that the mere fact of a program terminating implies its suitability in a safety context.
  - user1138 8mo ago
    Here's your citation — ARIA's Safeguarded AI program, £59M in UK government funding, explicitly claiming mathematical safety guarantees through restricted verifiable models — total languages by another name. The claim exists. It has a budget. Now, do you have a substantive response to the proof, or are we done here?" @techreport{ARIA2024, author = {{Advanced Research and Invention Agency}}, title = {Safeguarded AI: Constructing Guaranteed Safety}, institution = {ARIA}, year = {2024}, url = {https://www.aria.org.uk/programs/safeguarded-ai/ https://www.aria.org.uk/programs/safeguarded-ai/}, abstract = {Outlines a 'Safeguarded AI' program that seeks to build AI systems with 'mathematical guarantees.' It argues that by using restricted, verifiable models—effectively total languages—one can avoid the 'impossible' task of verifying general AI and instead produce 'quantitative safety guarantees.'} }
user1138 8mo ago
You're correct on the citations though that will probably be very easy as we have many people claiming exactly that. As to your second point, yes, and the safety claims being made are not restricted to those decidable subsets. The moment you claim general safety guarantees for systems operating beyond those constrained subsets you're back in full Rice territory. If you can name a total language with an early termination guarantee, I'm all ears. You asked for my citations, now show me yours.