4 ms·

You're probably thinking of Rice's theorem (a sort of generalised halting problem), but this task is actually way easier than that, since we're not trying to st

You're probably thinking of Rice's theorem (a sort of generalised halting problem), but this task is actually way easier than that, since we're not trying to study arbitrary algorithms: we're trying to study the subset of human-comprehensible algorithms. Most of the things we want computers to do are things that, given enough time, someone can write a program to solve: and generally, those programs are not tricksy or meta, and don't involve unsolved mathematics problems found by studying busy-beaver candidates. If it's possible for a human to understand how a program works (which is a necessary component of writing such a program), it's possible to write a mathematical proof about the program's behaviour, and that means it's in principle possible to automate the construction of that mathematical proof, which is equivalent to the "determine whether code conforms to the spec" task. "Somewhat easier than an impossible task" is not a particularly strong claim about when (or whether) this problem will be solved, though.

soraminazuki 5mo ago
We can't create an algorithm determining whether a computer program halts or not, but we can write one that checks whether it conforms to natural language specifications much more easily? That makes no sense. There's no exception to the halting problem regarding "human comprehensible" computer programs.
- __s 5mo ago
  They're saying most useful programs don't fall in the complete / correct divide. You can get a lot done while restricting yourself to provable programs
- wizzwizz4 5mo ago
  Rice's theorem says that we can't draw a partition between two sets of programs, based on their semantic properties. It says nothing about drawing a partition slightly to one side of the desirable partition, misclassifying some tricksy cases, but correctly classifying all the programs we care about.
- deleted 5mo ago
  [deleted]
ElectricalUnion 5mo ago
I will give you a class of programs humans wrote and they want improved: LLMs. Those were written by humans, and don't involve unsolved mathematics. Is your claim tht you just need to solve comprehensibility of LLMs? Figuring out epistemology and cognition to have a chance to reason about the outputs of a LLM seems to me way harder that traditional attempts to reason directly about algorithms.

soraminazuki 5mo ago

We can't create an algorithm determining whether a computer program halts or not, but we can write one that checks whether it conforms to natural language specifications much more easily? That makes no sense. There's no exception to the halting problem regarding "human comprehensible" computer programs.

__s 5mo ago
They're saying most useful programs don't fall in the complete / correct divide. You can get a lot done while restricting yourself to provable programs
wizzwizz4 5mo ago
Rice's theorem says that we can't draw a partition between two sets of programs, based on their semantic properties. It says nothing about drawing a partition slightly to one side of the desirable partition, misclassifying some tricksy cases, but correctly classifying all the programs we care about.
deleted 5mo ago
[deleted]

ElectricalUnion 5mo ago

I will give you a class of programs humans wrote and they want improved: LLMs. Those were written by humans, and don't involve unsolved mathematics. Is your claim tht you just need to solve comprehensibility of LLMs? Figuring out epistemology and cognition to have a chance to reason about the outputs of a LLM seems to me way harder that traditional attempts to reason directly about algorithms.