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

81–90 of 182 posts

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

#81

Post by idiotsecant »

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.

Parent post is talking about symbolic manipulation, not rote number crunching, which is exactly what we're supposed to be good at and machines are supposed to be bad at.

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

#82

Post by measurablefunc »

avmich wrote: post #79
measurablefunc wrote: post #63

Earlier quoted context omitted.

No magic is necessary to understand that carbon & silicon are not equivalent. The burden of proof is on those who think silicon can be a substitute for carbon & all that it entails. I don't buy into magical thinking like Turing machines being physically realizable b/c I have studied enough math & computer science to not be confused by abstractions & their physical realizations.

The proof immediately follows from the ability of silicon systems in principle to model carbon ones with arbitrary precision.

I recently wrote a simulation of water molecules & got really confused when the keyboard started getting water condensation on it. I concluded that simulating water was equivalent to manifesting it in reality & immediately stopped the simulation b/c I didn't want to short-circuit the CPU.

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

#83

Post by cerved »

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…

Who makes the rules?

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

#84

Post by pbronez »

LASR wrote: post #2

This is an interesting approach. My team has been prototyping something very similar with encoding business operations policies with LEAN. We have some internal knowledge bases (google docs / wiki pages) that we first convert to LEAN using LLMs. Then we run the solver to verify consistency. When a wiki page is changed, the process is run again and it's essentially a linter for process. Can't say it moved beyond the p…

That’s pretty cool. It would be super useful to identify contradictory guidance systematically.

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

#85

Post by Terr_ »

avmich wrote: post #80
Terr_ wrote: post #71

Earlier quoted context omitted.

The normative importance of a fact may increase when more number of people start willfully ignoring it for shorter-term profit. Imagine somebody in 2007: "It's so funny to me that people are still adamant about mortgage default risk after it's become a completely moot point because nobody cares in this housing market."

Didn't we have economists' consensus then about what's going to happen?

My point is a fact's popularity is not equal to its importance. That was a scenario to highlight how they can even have an inverse relationship.

Diving into how well/badly anybody predicted a certain economic future is a whole different can of worms.

That said: "The market can stay irrational longer than I can stay solvent." :p

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

#86

Post by psadri »

jonplackett wrote: post #62
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.

Maybe the number crunching program the text generation program creates will, with enough effort become good at generating text, an will in turn make another number crunching computer and then…

Watch the movie “The Thirteenth Floor”

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

#87

Post by 29athrowaway »

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.

We do plenty of number crunching all the time, just not consciously.

Like the inverse kinematics required for your arm and fingers to move.

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

#88

Post by pstoll »

29athrowaway wrote: post #87
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.

We do plenty of number crunching all the time, just not consciously. Like the inverse kinematics required for your arm and fingers to move.

I’d argue we aren’t solving those inverse kinematics / kinetics via “number crunching” - but rather that our neuromuscular systems are analog. Which I don’t usually call that “number crunching” in the sense current computers … compute.

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

#89

Post by typpilol »

everdrive wrote: post #74
NotGMan wrote: post #46

Earlier quoted context omitted.

Chat GPT-4 has alegedly 1.8 trillion parameters. Imagine having a bunch of 2D matrices with a combined 1.8 trillion total numbers, from which you pick out a blocks of numbers in a loop and finally merge them and combine them to form a token. Good luck figuring out what number represents what.

Wouldn't that mean it's totally impractical for day-to-day usage, but a researcher or team of researchers could solve this?

Anthropic has a tool that lets them do this but apparently doing it for even one prompt can take an entire day of work.

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

#90

Post by pstoll »

barthelomew wrote: post #51
tonerow wrote: post #41

Cool research! I went to the repo to see what the DSL looked like but it was hard to find a clear example. It would be cool if you added a snippet to the README.

Hey! Thank you for the interest! I shall do that. Meanwhile, check out Page 11 onwards. We describe a lot of situations! ( https://arxiv.org/pdf/2409.17270 )

Upvoting the comment that the gitrepo would be way more self stand-alone if it had an intro of the DSL.
Post reply on HN