[justinpombrio]

Gödel's Incompleteness Theorem places a limit on what you can prove within a formal system. Neither humans nor LLMs are a formal system, so it says nothing about them.

Someone's going to think that, since you can formally model computer programs (and thus formally model how an LLMs runs), that means that Gödel's Incompleteness Theorem applies to computer programs and to LLMs. But that's irrelevant; being model-able doesn't make something a formal system!

"Formal system" has a very technical meaning: it has a set of consistent axioms, and the ability to enumerate formal proofs using those axioms. For example, Zermelo-Fraenkel set theory is a formal system [1]. It has nine formal axioms, which you can see listed in its Wikipedia article. Utterly different kind of thing than humans or LLMs. Comparing an LLM to ZFC is like comparing a particular watermelon to the number 4.

[1] https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...

[jltsiren]

This is unnecessary nitpicking. You can easily derive a logical contradiction of your choice by assuming that a system that can be formally modeled can prove something that cannot be proven within a formal system. If a specific theorem doesn't prove that, a simple corollary will.

If you want to escape the limits of computability, you have to assume that the physical Church–Turing thesis is false. That the reality allows mechanisms that cannot be modeled formally or simulated on any currently plausible computer.

[justinpombrio]

> by assuming that a system that can be formally modeled can prove something that cannot be proven within a formal system

Something that cannot be proven within which formal system? Every true statement can be proven by some formal system. No formal system can prove all true statements.

(This is all about Godel incompleteness. Turing incomputability does apply though, see the sibling comments! It's important to keep them separate, they're saying different things.)

[Tainnor]

I'm confused by this. Why are you talking about Gödel?

LLMs, like any model of computation, are subject to the limits of Turing Machines, so they cannot for example solve the halting problem.

[justinpombrio]

Oof, I pattern matched OP to a different argument I've seen a lot. That's embarrassing.

Yes, that's correct, it's provably impossible to construct an LLM that, if you ask it "Will this program halt? <program>", answers correctly for all programs. Likewise humans, under the assumption that you can accurately simulate physics with a computer. (Note that QM isn't an obstacle, as you can emulate QM just fine with a classical computer with a mere exponential slowdown.)

[ccvannorman]

While it's true that LLMs are not strictly a formal system, they do operate on Turing-complete hardware and software, and thus they are still subject to the broader limitations of computability theory, meaning they cannot escape fundamental constraints like undecidability or incompleteness when attempting formal reasoning.

[loki49152]

LLMs don't do formal reasoning. Not in any sense. They don't do any kind of reasoning - they replay combinatorics of the reasoning that was encoded in their training data via "finding" the patterns in the relationships of the tokens at different scales and then applying those to the generation of some output triggered by the input.

[Tainnor]

That's irrelevant. They have an "input tape" and an "output tape" and whatever goes on inside the LLM could in principle be implemented in a TM (of course that wouldn't be efficient but that's besides the point).