On: Looming Liability Machines (LLMs)

[llm_trw]

The same is true of computers, in fact it has been mathematically proven that it is impossible to answer the general question if a computer program is correct.

But that hasn't stopped the last 40 years from happening because computers made fewer mistakes than the next best alternative. The same needs to be true of LLMs.

[mrcode007 → llm_trw]

The theory you’re alluding to says it is impossible to create a general algorithm that decides any non-trivial property of any computer program.

There is nothing in the theory that prevents you creating a program that verifies a particular specific program.

There is an entire field dedicated to doing just that.

[llm_trw → mrcode007]

The issue is there to verify a program you need to have a spec. To generate a spec you need to solve the general problem.

This is what gets swept under the rug whenever formal methods are brought up.

[mrcode007 → llm_trw]

That is not true at all. You do not need to generate a spec. All you need to do is prove a property. This can be done in many ways.

For example, many things can be proven about the following program without having to solve any general problem at all:

echo “hello world”

Similarly for quick sort, merge sort, and all sort of things. The degree of formality doesn’t have to go to formal methods which are only a very small part of the whole field

[llm_trw → mrcode007]

>echo “hello world”

Congratulations, you just launched all the worlds nuclear missiles.

This is to spec since you didn't provide one and we just fed the teletype output into the 'arm and launch' module of the missiles.

[mrcode007 → llm_trw]

What you’re saying is equivalent to throwing out all of mathematics due to the incompleteness theorem and start praying to fried egg jellyfish on full moon

[llm_trw → mrcode007]

No that's what OP is saying about LLMs.