Edit: I like this 10 years old blog post in regards to explaining the problem much better than I could do: https://pron.github.io/posts/correctness-and-complexity
The article asserts general guarantees of program correctness have fundamental limits, but it explicitly says those limits apply to humans too. While that suggests neither humans nor LLMs can reliably solve every planning or verification problem, it says nothing about which will do better on the software problems people actually encounter.
It certainly does not present a fundamental problem with LLMs as they exist today.
I do not mean that LLM is a classic symbolic system that generates symbols according to rules, but instead it's a system that generates symbols according to recorded probabilities. The focus here is on symbols: the LLM reasoning starts with <think> token, ends with </think> token, and everything in between is symbols (tokens). Quite different from how human brain works, where symbols are not that much involved in reasoning.
> The article asserts general guarantees of program correctness have fundamental limits, but it explicitly says those limits apply to humans too.
Yep, however I would like to assert that today we have evidence of systems architected by humans and behaving correctly (like Linux kernel), while there are no evidence of systems architected by LLMs that behave correctly. Even the systems which are architected by LLMs with human assistance (such as Claude Code or Codex) routinely have horrendous bugs (you're welcome to search "Claude Code Bug" and "Codex Bug" on this very website).
> It certainly does not present a fundamental problem with LLMs as they exist today.
The article was created 10 years ago that is why it does not address LLMs. However it asserts that mathematics modeling is not that helpful for writing correct programs. As long as LLM reasoning is closer to mathematics modeling than human mental modeling, LLMs will be worse at writing correct programs than humans. Some future technology less focused on symbolic reasoning could change that, but today it's not on sufficient level.
Yes. The combinatorial explosion is a great assessment of the "why".
But the problem is more nuanced than that because one has to assume that LLMs can reason accurately all the time which is demonstrably false.
The current LLMs cannot even state true sentences as true if they sound confident, without hedging.
Future LLMs may mitigate this, though it looks unlikely.