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

ProofOfThought: LLM-based reasoning using Z3 theorem proving

github.com

Post reply on HN
Print view View original

101–110 of 182 posts

Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving

#101

Post by raspasov »

moffkalast wrote: post #73
zwnow wrote: post #69

Earlier quoted context omitted.

LLMs do not reason. Not hard to understand.

Idk, before this people from your camp were saying LLMs can't even understand anything. Always moving the goalposts. Then it'll be they can't feel or can't something else just to be pointlessly contrarian. Anyway, wrong idea. There have been enough cases of models providing novel results that it's clear that whatever human trait they supposedly lack they don't really need. A car does not need legs, it does things dif…

What is "novel results"? A random UUID generator also gives "novel result", every time.

Even if we're to humor the "novel" part, have they actually come up with anything truly novel? New physics? New proofs of hard math problems that didn't exist before?

Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving

#102

Post by c-hendricks »

Barbing wrote: post #99
psadri wrote: post #86

Earlier quoted context omitted.

Watch the movie “The Thirteenth Floor”

This is somewhat unusual: 28% on the Tomatometer, but 7 out of 10 on IMDb. Beyond its relevancy to the parent comment, would you consider it a good movie yourself? (for a random/average HN commenter to watch)

It didn't do well critically, but audience scores on many platforms are 60-70%. It came hot on the heels of The Matrix, has similar themes, but nowhere near as ... everything compared to Matrix. I'd bet the only reason it did so poorly critically is due to the timing of the release.

It's a fine movie though.

Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving

#103

Post by emporas »

TrainedMonkey wrote: post #57
chrchr wrote: post #54

I had a surprising interaction with Gemini 2.5 Pro that this project reminds me of. I was asking the LLM for help using an online CAS system to solve a system of equations, and the CAS system wasn't working as I expected. After a couple back and forths with Gemini about the CAS system, Gemini just gave me the solution. I was surprised because it's the kind of thing I don't expect LLMs to be good at. It said it used P…

Just like humans... we are not so good at hard number crunching, but we can invent computers that are amazing at it. And with a lot of effort we can make a program that uses a whole lot of number crunching to be ok at predicting text but kind of bad at crunching hard numbers. And then that program can predict how to create and use programs which are good at number crunching.

Small steps of nondeterministic computation, checked thoroughly with deterministic computation every so often, and the sky is the limit.

That's when A.I. starts advancing itself and needs humans in the loop no more.

Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving

#104

Post by emp17344 »

moffkalast wrote: post #60
zwnow wrote: post #19

Reasoning? LLMs can not reason, why is it always assumed they reason? They mimic reasoning.

It's so funny to me that people are still adamant about this like two years after it's become a completely moot point.

Moot point? As far as I know, it’s still intensely debated, and there are some excellent papers out there providing evidence that LLMs truly are just statistical prediction machines. It’s far from an unreasonable position.

Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving

#105

Post by eru »

emporas wrote: post #103
TrainedMonkey wrote: post #57

Earlier quoted context omitted.

Just like humans... we are not so good at hard number crunching, but we can invent computers that are amazing at it. And with a lot of effort we can make a program that uses a whole lot of number crunching to be ok at predicting text but kind of bad at crunching hard numbers. And then that program can predict how to create and use programs which are good at number crunching.

Small steps of nondeterministic computation, checked thoroughly with deterministic computation every so often, and the sky is the limit. That's when A.I. starts advancing itself and needs humans in the loop no more.

Your checks don't have to be deterministic either.

Eg randomised quicksort works really well.

Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving

#106

Post by bhk »

barthelomew wrote: post #29
ivanbakel wrote: post #4

The repo is sparse on the details unless you go digging, which perhaps makes sense if this is just meant as the artifact for the mentioned paper. Unless I’m wrong, this is mainly an API for trying to get an LLM to generate a Z3 program which “logically” represents a real query, including known facts, inference rules, and goals. The “oversight” this introduces is in the ability to literally read the logical statement…

Yep. The paper was written last year with GPT-4o. Things have become a lot better since then with newer models. E.g. https://arxiv.org/pdf/2505.20047 Tab 1, we compare the performance on text-only vs SMT-only. o3-mini does pretty well at mirroring its text reasoning in its SMT, vs Gemini Flash 2.0. Illustration of this can be seen in Fig 14, 15 on Page 29. In commercially available products like AWS Automated Reasoni…

Re: "99% of the time" ... this is an ambiguous sample space. Soundness of results clearly depends on the questions being asked. For what set of questions does the 99% guarantee hold?

Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving

#107

Post by emporas »

eru wrote: post #105
emporas wrote: post #103

Earlier quoted context omitted.

Small steps of nondeterministic computation, checked thoroughly with deterministic computation every so often, and the sky is the limit. That's when A.I. starts advancing itself and needs humans in the loop no more.

Your checks don't have to be deterministic either. Eg randomised quicksort works really well.

Couldn't disagree more.

Sorting a finite number of elements in a sequence, is a very narrow application of AI, akin to playing chess. Usually very simple approaches like RL work totally fine for problems like these, but auto-regression/diffusion models have to take steps that are not well defined at all, and the next step towards solving the problem is not obvious.

As an example, imagine a robot trying to grab a tomato from a table. It's arm extends across 1 meter maximum, and the tomato is placed 0.98 meters away. Is it able to grab the tomato from the point it stands, or it needs to move closer, and only then try to grab the tomato?

That computation should better be calculated deterministically. Deterministic computation is faster, cheaper and more secure. It has to prove that: $tomato_distance + $tomato_size From the paper:

> Our system employs a custom interpreter that parses "LLM-Thoughts" (represented as DSL code snippets) to generate First Order Logic programs, which are then verified by a Z3 theorem prover.

Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving

#108

Post by horacemorace »

moffkalast wrote: post #73
zwnow wrote: post #69

Earlier quoted context omitted.

LLMs do not reason. Not hard to understand.

Idk, before this people from your camp were saying LLMs can't even understand anything. Always moving the goalposts. Then it'll be they can't feel or can't something else just to be pointlessly contrarian. Anyway, wrong idea. There have been enough cases of models providing novel results that it's clear that whatever human trait they supposedly lack they don't really need. A car does not need legs, it does things dif…

This will be the exact same argument in 20 years when we’ve got examples of robots that some fraction of people claim are conscious.

Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving

#109

Post by visarga »

emporas wrote: post #103
TrainedMonkey wrote: post #57

Earlier quoted context omitted.

Just like humans... we are not so good at hard number crunching, but we can invent computers that are amazing at it. And with a lot of effort we can make a program that uses a whole lot of number crunching to be ok at predicting text but kind of bad at crunching hard numbers. And then that program can predict how to create and use programs which are good at number crunching.

Small steps of nondeterministic computation, checked thoroughly with deterministic computation every so often, and the sky is the limit. That's when A.I. starts advancing itself and needs humans in the loop no more.

> That's when A.I. starts advancing itself and needs humans in the loop no more.

You got to put the environment back in the loop though, it needs a source of discovery and validity feedback for ideas. For math and code is easy, for self driving cars doable but not easy, for business ideas - how would we test them without wasting money? It varies field by field, some allow automated testing, others are slow, expensive and rate limited to test.

Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving

#110

Post by galaxyLogic »

emporas wrote: post #103
TrainedMonkey wrote: post #57

Earlier quoted context omitted.

Just like humans... we are not so good at hard number crunching, but we can invent computers that are amazing at it. And with a lot of effort we can make a program that uses a whole lot of number crunching to be ok at predicting text but kind of bad at crunching hard numbers. And then that program can predict how to create and use programs which are good at number crunching.

Small steps of nondeterministic computation, checked thoroughly with deterministic computation every so often, and the sky is the limit. That's when A.I. starts advancing itself and needs humans in the loop no more.

The question is where should AI advance itself? Which direction? There are an infinite number of theorems that can be derived from a set of axioms. Infinite. AI can't prove them all. Somebody needs to tell it what it needs to do, and that is us.
Post reply on HN