Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

LLMs don't do formal reasoning

garymarcus.substack.com

Post reply on HN
Print view View original

71–80 of 128 posts

Re: LLMs don't do formal reasoning

#71

Post by zero_k »

zero_k wrote: post #44

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…

Correction, Lean4 [1] is sponsored by Amazon, the lead developer, Leonardo de Moura is at AWS now [2]. He was previously at Microsoft Research [3]. Meeting him is a real ride, I only had the chance to talk with him once.

[1] https://lean-lang.org/

[2] https://leodemoura.github.io/about.html

[3] https://www.microsoft.com/en-us/research/blog/the-inner-magi...

Re: LLMs don't do formal reasoning

#72

Post by bartread »

apwell23 wrote: post #56
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…

> Large numbers of people and businesses are extracting huge value from the use of LLMs every single day No they aren't. If they really did we would see those number in qtrly reports.

The impact of LLMs for many sectors is deflationary, which means you specifically won't see those numbers in quarterly reports. Doesn't mean that value isn't being extracted with LLMs but rather that it's being eroded elsewhere. What you'll see is companies that don't leverage the benefits gradually being left behind.

Re: LLMs don't do formal reasoning

#73

Post by jumploops »

> There is just no way you can build reliable agents on this foundation, where changing a word or two in irrelevant ways or adding a few bits of irrelevant info can give you a different answer.

LLMs are not magic bullets for every problem, but that doesn't preclude them from being used to build reliable systems or "agents."

It's clear that we don't yet have the all-encompassing AGI architecture, especially with the transformer model alone, but adding steps beyond the transformer leads to interesting results, as we've seen with current coding tools and the new o1-series models by OpenAI.

For example, the featured article calls out `o1-mini` as failing a kiwi-counting test prompt, however the `o1-preview` model gets the right answer[0].

I also built a simple test using gpt-4o, that prompts it to solve the problem in parts, and it reliably returns the correct answer using only gpt-4o and code generated by gpt-4o[1].

Furthermore, there's still a ton of research being done on models that are specific to formal theorem proving that show promise[2] (even if `o1-preview` already beats them for e.g. IMO problems[3]).

I'm of the opinion that we still have a ways to go until AGI, but that doesn't mean LLMs can't be used in reliable ways.

[0]https://chatgpt.com/share/e/67098356-ce88-8001-a2e1-9857064a...

[1]https://magicloops.dev/loop/30fb3c1a-8e40-47ae-8611-91554faf...

[2]https://arxiv.org/pdf/2408.08152

[3]https://openai.com/index/introducing-openai-o1-preview/

Re: LLMs don't do formal reasoning

#74

Post by bartread »

lewhoo wrote: post #31
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…

> Yet in the face of this we still see a population of naysayers who appear intent on rubbishing LLMs at any cost. What was the cost in this case ? It's just an experiment and I think your reaction is way too emotional for some reason.

It's not emotional: it's bored. This is boring me and therefore I'm becoming irritated with it.

Re: LLMs don't do formal reasoning

#75

Post by grey-area »

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-...

Great article which really explores why we fall for llms and think they are doing a lot more thinking than they are.Thanks.

Re: LLMs don't do formal reasoning

#76

Post by yunwal »

exe34 wrote: post #11
ak_111 wrote: post #7

Earlier quoted context omitted.

Are you suggesting Humans can't do formal reasoning? Because you can easily teach a four year old not to make illegal moves in chess with very little instructions, and by 10 geniuses like Terence Tao were discussing open math problems with Erdos. If anything this article adds further evidence that whatever the architecture of the human brain it is very different to an LLM architecture.

> Are you suggesting Humans can't do formal reasoning? most of them can't. they actively vote against their own interests and everybody else around them. if you confront them with facts and figures, they ignore it and resort to emotional appeals. just because you can find one child that can play chess at age 4 doesn't mean that the rest won't just eat the pieces and shit on the board.

It would be practically, if not literally, impossible to formally prove that you voted for/against your own interests, if you could even define what that means. Formal reasoning means a specific thing.

Re: LLMs don't do formal reasoning

#77

Post by zero_k »

dmonitor wrote: post #68
zero_k wrote: post #44

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…

> 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 Why would an LLM trained on human language patterns be good at this? If anything, I would expect it to follow the same pattern that humans do.

It doesn't need to be good at solving the problem. It only needs to be good at translating the problem of "If the unknown x is divided by 3 it has the same value as if I subtracted 9 from it" into "x/3 == x-9 && x is an Real number". The formal method tool will do the rest.

Note that if the LLM gets the implicit assumptions wrong, the solution will be unsatisfactory, and the query can be refined. This is exactly what happens with actual human experts, as per the anecdote I shared in [3]. So the LLM can replace some of the human-in-the-loop that makes it so hard to use formal methods tools. Humans are good at explaining the problem in human language, but have difficulty formulating them in ways that a formal tool can deal with. Humans, i.e. consultants, help with formalizing them in e.g. SMT. We could skip some of that, and make formal methods tools much more accessible.

Re: LLMs don't do formal reasoning

#78

Post by andrewla »

Like many other commenters, I was unable to reproduce the behavior cited in the link. I do like that this is attempting to make explicit the specific form of "formal reasoning" that is being used here, even if I do not necessarily agree that we have a clean separation between the ideas of "pattern matching" and "formal reasoning", or even any real evidence that humans are capable of one and not the other.

The idea that "LLMs have difficulty ignoring extraneous and irrelevant information" is not really dispositive to their effectiveness, since this statement obviously applies to humans as well.

Re: LLMs don't do formal reasoning

#79

Post by obmelvin »

robterrell wrote: post #49
obmelvin wrote: post #23

Earlier quoted context omitted.

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.

Yes, I'm not claiming that is true formal reasoning, but it is certainly more of a chain of thought than was previously being done and does indicate that some questions require more and less "thought"

Re: LLMs don't do formal reasoning

#80

Post by grey-area »

rahimnathwani wrote: post #50
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.

It does talk about openai explicitly instruction tuning the llm to try to constrain the output and the limitations of such approaches.
Post reply on HN