Step 1: solve the halting problem.

soraminazuki 4 hours ago | parent | next [-]

Yep, calling it an "unsolved" problem is a misnomer. We already have mathematical proof that it's impossible.

But that aside, it's such a shame that many drinking the AI Kool-Aid aren't even aware of the theoretical limits of a computer's capabilities.

▲

mjd 4 hours ago | parent [-]

This sort of theoretical result is not always as clear-cut as you suggest.

Computers are finite machines. There is a theorem that although a machine with finite memory can add, multiplication requires unbounded memory. Somehow we muddle along and use computers for multiplication anyway.

More to your point there is a whole field of people who write useful programs using languages in which every program must be accompanied by a proof that it halts on all inputs.

(See for example https://lean-lang.org/ or David Turner's work on Total Functional Programming from about 20 years ago.)

Other examples are easy to find. The simplex algorithm for linear optimization requires exponential time in general, and the problem it solves is NP-hard, but in practice works well on problems of interest and is widely used. Or consider the dynamic programming algorithms for problems like subset-sum.

Theory is important, but engineering is also important.

▲

za_creature 3 hours ago | parent | next [-]

> There is a theorem that (...) multiplication requires unbounded memory

What theorem is that?

The multiplication of any two integers below a certain size (called "words") fits in a "double word" and the naive multiplication algorithm needs to store the inputs, an accumulator and at most another temporary for a grand total of 6*word_size

Sure, you can technically "stream" carry-addition (which is obvious from the way adders are chained in ALU-101) and thus in a strict sense addition is O(1) memory but towards your final point:

> Theory is important, but engineering is also important.

In practice, addition requires unbounded memory as well (the inputs). And it's definitely compute-unbounded, if your inputs are unbounded.

I dislike the term "we muddle along". IEEE 754 has well specified error bars and cases, and so does all good data science. LLMs do not, or at least they do not expose them to the end user

So then, how exactly do we go about proving that the result of chaining prompts is within a controllable margin of error of the intended result? Because despite all the specs, numerical stability is the reason people don't write their own LAPACK.

▲

soraminazuki 4 hours ago | parent | prev [-]

But it's not like these systems make theory go away, they make compromises. So the question is, what's the compromise required for an algorithm that can check the conformance of computer programs to natural language specifications that doesn't involve hoping for the best?

	▲	wizzwizz4 an hour ago \| parent [-]
		Natural language specifications often aren't specifications at all: interpreting them requires context that is not available to the computer, and often not even available to the specification's authors without further research / decision-making. LLMs address this problem by just making things up (and they don't do a great job of comprehending the natural language, either), which I think qualifies as "hoping for the best", but I'm not sure there is another way, unless you reframe the problem to allow the algorithm to request the information it's missing.

▲

wizzwizz4 4 hours ago | parent | prev [-]

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 4 hours ago | parent | next [-]

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 2 hours ago \| parent \| next [-]
		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 2 hours ago \| parent \| prev [-]
		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.

▲

ElectricalUnion 2 hours ago | parent | prev [-]

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.