LLMs don't do formal reasoning • Hacker News Board

Re: LLMs don't do formal reasoning

#41

Post by rahimnathwani » Fri, Oct 11, 2024, 7:52 PM UTC

The paper (published 4 days ago) has this on page 10, and says that o1-mini failed to solve it correctly:

   Oliver picks 44 kiwis on Friday. Then he picks 58 kiwis on Saturday. On Sunday, he picks double the number of kiwis he did on Friday, but five of them were a bit smaller than average. How many kiwis does Oliver have?

I pasted it into ChatGPT and Claude, and all four models I tried gave the correct answer:

4o mini: https://chatgpt.com/share/6709814f-9ff8-800e-8aab-127b6f952d...

4o: https://chatgpt.com/share/6709816c-3768-800e-9eb1-173dfbb5d8...

o1-mini: https://chatgpt.com/share/67098178-4088-800e-ba95-9731a75055...

3.5 sonnet: https://gist.github.com/rahimnathwani/34f93de07eb7510d57ec1e...

Re: LLMs don't do formal reasoning

#42

Post by lukev » Fri, Oct 11, 2024, 7:53 PM UTC

ajross wrote: post #13

It seems like the needle is now swinging too far back, pointing to "LLMs will NEVER work". And I don't think that's very grounded either. All these criticisms are valid for human beings too . That kind of question trickery trips up school kids all the time. It's hard to use our brains to reason. It takes practice, and the respresentation of the "reasoning" always ends up being alien to our actual cognitive experience…

I don't even think that's what this is doing, though. As technologists, the point isn't to be bullish or bearish on LLMs... we should be focused on empirically understanding what they can do, and why, so that we can design systems to leverage them most effectively and work around their areas of weakness.

This article is important for that because it helps articulate the limit of what (current) LLMs can do. Even if you're an AI maximalist, it's essential to understand the current areas of weakness to design better models or build systems that compensate.

Re: LLMs don't do formal reasoning

#43

Post by pton_xd » Fri, Oct 11, 2024, 7:54 PM UTC

hackinthebochs wrote: post #16

Getting tired of seeing this guy's bad arguments get signal boosted. I posted this comment on another LLM thread on the front page today, and I'll just repost it here: LLMs aren't totally out of scope of mathematical reasoning. LLMs roughly do two things, move data around, and recognize patterns. Reasoning leans heavily on moving data around according to context-sensitive rules. This is well within the scope of LLMs.…

Some problems are computationally bounded (computational complexity theory). LLMs may theoretically have unbounded pattern matching capabilities with increasingly large data sets and training, but what is the realistic limit here? When we utilize all of the currently available power on Earth for training, what does that LLM look like? Is that LLMs pattern matching replacing humans and solving all of physics?

Re: LLMs don't do formal reasoning

#44

Post by zero_k » Fri, Oct 11, 2024, 7:55 PM UTC

Yes, we should use LLMs to translate human requirements that are ambiguous and have a lot of hidden assumptions (e.g. that football matches should preferably be at times when people are not working & awake [3]), and use them to create formal requirements, e.g. generating SMT [1] or ASP [2] queries. Then the formal methods tool, e.g. Z3/cvc5 or clingo can solve these now formal queries. Then we can translate back the solution to human language via the LLM. This does not solve some problems, e.g. the LLM not correctly guessing the implicit requirements. But it does go around a bunch of issues.

We do need to pump up the jam when it comes to formal methods tools, though. And academia is still rife with quantum and AI buzzword generators if you wanna get funding. Formal methods doesn't get enough funding from Academia. Amazon has put a bunch of money into it (hiring all good talent :sadface:), and Microsoft is funding both Z3 and Lean4. Industry is ahead of the game, again. This is purely failure of Academic leadership, nothing else.

[1] https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

[2] https://en.wikipedia.org/wiki/Answer_set_programming

[3] Anecdotal, but this was a "bug" in a solution offered by a tool that optimally schedules football matches in Spain.

Re: LLMs don't do formal reasoning

#45

Post by SpicyLemonZest » Fri, Oct 11, 2024, 7:55 PM UTC

pier25 wrote: post #24

bartread wrote: post #5

This trope of proclaiming some critical flaw in the functioning of LLMs with the implication that they therefore should not be used is getting boring. LLMs are far from perfect but they can be a very useful tool that, used well, can add significant value in spite of their flaws. Large numbers of people and businesses are extracting huge value from the use of LLMs every single day. Some people are building what will b…

It's probably the other way around actually. The average person assumes LLMs are intelligent and all this AI thing will end up replacing them. This has created a distorted perception of the tech which has had multiple consequences. It's necessary to change this perception so that it better adjusts with reality.

But I don’t think this result is relevant to that question at all. There’s quite a lot of people in the world who can’t consistently apply formal mathematical reasoning to word problems or reliably multiply large numbers.

Re: LLMs don't do formal reasoning

#46

Post by anon291 » Fri, Oct 11, 2024, 7:55 PM UTC

Current LLMs are one-shot. They are forced to produce an output without thinking, leading to the preponderance of hallucinations and lack of formal reasoning. Human formal reasoning is not instinctual. Unlike 'aha!' moments, it requires us to think. Part of that thinking process is turning our attention inwards into our own mind and using symbolic manipulations that we do not utter in order to 'think'.

LLMs broadly are capable of this, but we force them to not do it by forcing the next token to be the final output.

The human equivalent would be to solve a problem and show all your steps including steps that are wrong but that you undertook anyway. Hence why chain of reasoning works.

The 'fix' is to allow LLMS to pause, generate tokens that are not transliterated into text, and then signal when they want to unpause. Training such a system is left as an exercise to the reader, although there have been attempts

Re: LLMs don't do formal reasoning

#47

Post by lr4444lr » Fri, Oct 11, 2024, 7:55 PM UTC

hackinthebochs wrote: post #16

Getting tired of seeing this guy's bad arguments get signal boosted. I posted this comment on another LLM thread on the front page today, and I'll just repost it here: LLMs aren't totally out of scope of mathematical reasoning. LLMs roughly do two things, move data around, and recognize patterns. Reasoning leans heavily on moving data around according to context-sensitive rules. This is well within the scope of LLMs.…

I don't know what his other bad arguments are, but nothing you're describing disputes the point about formal reasoning, which is that getting it wrong is susceptible to parameter fitting. This has been a problem with AI models ever since the perceptron, which can still converge to the wrong classifications even when it's fed enough training data.

Re: LLMs don't do formal reasoning

#48

Post by adamc » Fri, Oct 11, 2024, 7:56 PM UTC

ajross wrote: post #13

It seems like the needle is now swinging too far back, pointing to "LLMs will NEVER work". And I don't think that's very grounded either. All these criticisms are valid for human beings too . That kind of question trickery trips up school kids all the time. It's hard to use our brains to reason. It takes practice, and the respresentation of the "reasoning" always ends up being alien to our actual cognitive experience…

I struggle to see the use of this comment. Many human beings have jobs where they reason about problems far more complex than this every day. Sure, not every human is great at this. But the interest in using LLMs as agents does kind of require that they can routinely get this right -- the author of the blog post mentions this explicitly.

Re: LLMs don't do formal reasoning

#49

Post by robterrell » Fri, Oct 11, 2024, 7:56 PM UTC

obmelvin wrote: post #23

wkat4242 wrote: post #12

One of the things that kinda illustrate this for me, is that an LLM always uses the same time to process a prompt of the same length. No matter how complicated the problem is. Obviously the complexity of the problem is not actually taken into account.

the o1 model definitely has a somewhat big variance in how long the task takes depending on what you ask it to do

You don't see the majority of tokens it is generating.

Re: LLMs don't do formal reasoning

#50

Post by rahimnathwani » Fri, Oct 11, 2024, 7:57 PM UTC

tj-teej wrote: post #2

If anyone is curious, a Meta Data Scientist published a great piece about how the facts about what LLMs are actually doing (and therefore able to do) and how it's papered over by using chat bots. It's a long but very engaging read. https://medium.com/@colin.fraser/who-are-we-talking-to-when-...

This article is long but doesn't mention key concepts like instruction tuning.

I'd suggest the Llama paper as a more worthwhile source.