3 ms·

Beginners in computer science need to understand that there's no such thing as a computer programming method or discipline that "blocks AI mistakes via proof."

by lutusp 15d ago

Beginners in computer science need to understand that there's no such thing as a computer programming method or discipline that "blocks AI mistakes via proof." This is not a position or opinion, it is a fundamental constraint called the "Halting Problem," originally identified by Alan Turing in 1936. What applies to computer programming also applies to AI, for a reason that should be obvious. Lean, a widely used theorem prover, its everyday description notwithstanding, is Turing-complete and is therefore subject to the Halting Problem as well. This is not meant to disparage one person's project. It is meant to identify a limit that applies to all such projects.

zamadatix 15d ago
Graybeards in computer science sometimes need to remember the halting problem only states you cannot make a general algorithm which answers the halting question for all possible program+input pairs. Importantly, it does not state it's impossible to make an algorithm which can check if the given program+possible inputs will halt (or even if a given subset of all possible programs will - e.g., trivially, finitely long ones not given a means of recursion or allowed infinitely long inputs). Separately, the halting problem would not apply in the first place. The claim and goal is only to approve programs for which the given proof can be shown to work and then accept it when it does, not to guarantee every possible bend program and condition set will be able to have a working proof. Practically, this means if the proofing mechanism can not do that in the time+space bounds the solver is given then thats just treated as a rejection of the given proof (regardless whether the proposed program does or does not actually fit the requirements) and the LLM is back at trying to create a program which is feasibly provable.
- lutusp 15d ago
  > Separately, the halting problem would not apply in the first place. The halting problem applies to all systems able to perform Peano arithmetic. Therefore it applies to all non-trivial programs -- the program being tested, the program performing the test, and the program verifying the result. > The claim and goal is only to approve programs for which the given proof can be shown to work and then accept it when it does ... Yes, but that's not what's being claimed. My objection was to the original claim, not this restatement. > ... and the LLM is back at trying to create a program which is feasibly provable. No non-trivial computer program is "feasibly provable." That's what the Halting Problem makes impossible.
  - zamadatix 15d ago
    The halting problem applying to all systems is not the same as the halting problem being relevant to all claims about halting of systems (unless those claims can also be rigorously proven to match the conditions of the generalized halting problem first). I.e. I'm not trying to say the halting problem does not apply to these systems in general, I'm saying it doesn't apply to the specific claims being made about these systems. As an example of the type of thing I'm saying: one can show an algorithm which multiplies a real number by 2 cannot guarantee the output will be an even number for all inputs. Separately, one can create and prove a algorithm which takes an integer number greater than 0 and multiplies it by 2 will always meet the very same guarantee. In this scenario it clearly did not matter the first proof of lack of guarantee applied to all algorithms using real numbers, the more restricted subset of real numbers could make a guarantee. Specifically to the halting problem and Bend again: It's not about an algorithm which can definitely answer yes or no for any program+input. The given claim/condition from Bend is simpler: it blocks mistakes (because it only accepts provably valid proofs, not because it can prove every input one way or the other). > Yes, but that's not what's being claimed. My objection was to the original claim, not this restatement. It blocks AI mistakes, it only accepts ones able to be proven. Nothing in that claim says it will prove every input one way or the other, that's just an assumption which you rightly showed could not be a reasonable interpretation of the title. It might also be prudent to ask the author if they really mean they interpretation you take before declaring the problem as beginner's lacking understanding of a foundational theory in computer science. > No non-trivial computer program is "feasibly provable." That's what the Halting Problem makes impossible. What's your definition of "non-trivial" here and how did you derive that definition as the one used by the claim? As a side note, I have no affiliation or ecen prior knowledge of the project/author prior to reading this post, I just get nerd sniped by overly broad claims about the halting problem.
    - lutusp 15d ago
      > It blocks AI mistakes, it only accepts ones able to be proven. This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation. > It might also be prudent to ask the author if they really mean they interpretation you take How the original author chose to express himself is not my problem, it is his. I have the simple responsibility to take him at his word. Anything else would be disrespectful. > What's your definition of "non-trivial" here and how did you derive that definition as the one used by the claim? I didn't define it, Alan Turing did, in 1936. It's not a debating point, it's a fundamental limitation. All Turing-complete code sources have this limitation. Read more here: https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem .
skew 14d ago
You are the one being insufficiently precise here. There would only be fundamental obstacles if there was an additional claim "allows all correct programs". The Halting problem states only that is no computable function that takes another P program as input and always terminates with a correct answer of whether P halts. It's certainly possible to write a program that always terminates with an answer of either HALTS or UNKNOWN, and only says HALT when that's true, it's just that it will also return UNKNOWN for some (or all) programs that do actually halt.
- lutusp 13d ago
  > It's certainly possible to write a program that always terminates with an answer of either HALTS or UNKNOWN, and only says HALT when that's true, it's just that it will also return UNKNOWN for some (or all) programs that do actually halt. Any program running in a Turing-complete environment is subject to the Halting Problem. So, given that constraint, your example program cannot be relied on to do any specific thing. That's the meaning of the Turing Halting Problem. https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem : "Alan Turing proved in 1937 that the halting problem is undecidable, meaning that no general algorithm exists that can correctly solve the problem for all possible program–input pairs." Focus your attention on the word "undecidable".

by lutusp 15d ago

zamadatix 15d ago

Graybeards in computer science sometimes need to remember the halting problem only states you cannot make a general algorithm which answers the halting question for all possible program+input pairs. Importantly, it does not state it's impossible to make an algorithm which can check if the given program+possible inputs will halt (or even if a given subset of all possible programs will - e.g., trivially, finitely long ones not given a means of recursion or allowed infinitely long inputs). Separately, the halting problem would not apply in the first place. The claim and goal is only to approve programs for which the given proof can be shown to work and then accept it when it does, not to guarantee every possible bend program and condition set will be able to have a working proof. Practically, this means if the proofing mechanism can not do that in the time+space bounds the solver is given then thats just treated as a rejection of the given proof (regardless whether the proposed program does or does not actually fit the requirements) and the LLM is back at trying to create a program which is feasibly provable.

lutusp 15d ago
> Separately, the halting problem would not apply in the first place. The halting problem applies to all systems able to perform Peano arithmetic. Therefore it applies to all non-trivial programs -- the program being tested, the program performing the test, and the program verifying the result. > The claim and goal is only to approve programs for which the given proof can be shown to work and then accept it when it does ... Yes, but that's not what's being claimed. My objection was to the original claim, not this restatement. > ... and the LLM is back at trying to create a program which is feasibly provable. No non-trivial computer program is "feasibly provable." That's what the Halting Problem makes impossible.
- zamadatix 15d ago
  The halting problem applying to all systems is not the same as the halting problem being relevant to all claims about halting of systems (unless those claims can also be rigorously proven to match the conditions of the generalized halting problem first). I.e. I'm not trying to say the halting problem does not apply to these systems in general, I'm saying it doesn't apply to the specific claims being made about these systems. As an example of the type of thing I'm saying: one can show an algorithm which multiplies a real number by 2 cannot guarantee the output will be an even number for all inputs. Separately, one can create and prove a algorithm which takes an integer number greater than 0 and multiplies it by 2 will always meet the very same guarantee. In this scenario it clearly did not matter the first proof of lack of guarantee applied to all algorithms using real numbers, the more restricted subset of real numbers could make a guarantee. Specifically to the halting problem and Bend again: It's not about an algorithm which can definitely answer yes or no for any program+input. The given claim/condition from Bend is simpler: it blocks mistakes (because it only accepts provably valid proofs, not because it can prove every input one way or the other). > Yes, but that's not what's being claimed. My objection was to the original claim, not this restatement. It blocks AI mistakes, it only accepts ones able to be proven. Nothing in that claim says it will prove every input one way or the other, that's just an assumption which you rightly showed could not be a reasonable interpretation of the title. It might also be prudent to ask the author if they really mean they interpretation you take before declaring the problem as beginner's lacking understanding of a foundational theory in computer science. > No non-trivial computer program is "feasibly provable." That's what the Halting Problem makes impossible. What's your definition of "non-trivial" here and how did you derive that definition as the one used by the claim? As a side note, I have no affiliation or ecen prior knowledge of the project/author prior to reading this post, I just get nerd sniped by overly broad claims about the halting problem.
  - lutusp 15d ago
    > It blocks AI mistakes, it only accepts ones able to be proven. This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation. > It might also be prudent to ask the author if they really mean they interpretation you take How the original author chose to express himself is not my problem, it is his. I have the simple responsibility to take him at his word. Anything else would be disrespectful. > What's your definition of "non-trivial" here and how did you derive that definition as the one used by the claim? I didn't define it, Alan Turing did, in 1936. It's not a debating point, it's a fundamental limitation. All Turing-complete code sources have this limitation. Read more here: https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem .

skew 14d ago

You are the one being insufficiently precise here. There would only be fundamental obstacles if there was an additional claim "allows all correct programs". The Halting problem states only that is no computable function that takes another P program as input and always terminates with a correct answer of whether P halts. It's certainly possible to write a program that always terminates with an answer of either HALTS or UNKNOWN, and only says HALT when that's true, it's just that it will also return UNKNOWN for some (or all) programs that do actually halt.

lutusp 13d ago
> It's certainly possible to write a program that always terminates with an answer of either HALTS or UNKNOWN, and only says HALT when that's true, it's just that it will also return UNKNOWN for some (or all) programs that do actually halt. Any program running in a Turing-complete environment is subject to the Halting Problem. So, given that constraint, your example program cannot be relied on to do any specific thing. That's the meaning of the Turing Halting Problem. https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem : "Alan Turing proved in 1937 that the halting problem is undecidable, meaning that no general algorithm exists that can correctly solve the problem for all possible program–input pairs." Focus your attention on the word "undecidable".