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

61–70 of 182 posts

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

#61

Post by anotherpaulg »

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…

I really like LLM+sympy for math. I have the LLM write me a sympy program, so I can trust that the symbolic manipulation is done correctly.

The code is also a useful artifact that can be iteratively edited and improved by both the human and LLM, with git history, etc. Running and passing tests/assertions helps to build and maintain confidence that the math remains correct.

I use helper functions to easily render from the sympy code to latex, etc.

A lot of the math behind this quantum eraser experiment was done this way.

https://github.com/paul-gauthier/entangled-pair-quantum-eras...

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

#62

Post by jonplackett »

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.

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…

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

#63

Post by measurablefunc »

supern0va wrote: post #53
measurablefunc wrote: post #26

Earlier quoted context omitted.

If you believe computers can think then you must be able to explain why a chain of dominoes is also thinking when I convert an LLM from transistor relay switches into the domino equivalent. If you don't fall for the marketing hype & study both the philosophical & mathematical literature on computation then it is obvious that computers (or any mechanical gadget for that matter) can not qualify for any reasonable defin…

>If you believe computers can think then you must be able to explain why a chain of dominoes is also thinking when I convert an LLM from transistor relay switches into the domino equivalent. Sure, but if you assume that physical reality can be simulated by a Turing machine, then (computational practicality aside) one could do the same thing with a human brain. Unless you buy into some notion of magical thinking as pe…

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.

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

#64

Post by barthelomew »

tannhaeuser wrote: post #52

LLMs are statistical language models (d'uh) not reasoners after all. I found generating logic programs, and Prolog source specifically, to work unreasonably well, though [1], maybe because Prolog was introduced for symbolic natural language processing and there's a wealth of translation examples in the training set. Might be worth checking out Z3's alternative Datalog syntax [2] instead of its Lisp-ish SMTLib syntax.…

Yep! Datalog syntax for Z3 is pretty neat! We used SMT [1] in our grammars paper because it allowed the most interoperability with solvers, but our technique also works with PROLOG; as tested our at the behest of reviewers at NeurIPS. I would assume that this should also work with datalog [2].

[1] https://arxiv.org/abs/2505.20047 [2] https://github.com/antlr/grammars-v4/blob/master/datalog/dat...

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

#65

Post by zwnow »

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.

Experts are adamant about this. Just take a look at https://youtu.be/iRqpsCHqLUI

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

#67

Post by moffkalast »

zwnow wrote: post #65
moffkalast wrote: post #60

Earlier quoted context omitted.

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

Experts are adamant about this. Just take a look at https://youtu.be/iRqpsCHqLUI

No such thing as an expert consensus on anything about LLMs these days, just different forms of grift.

My point is, the question if an LLM reasons the same way a human does is about as useful as "does a submarine swim" or "can a telephone talk". The results speak for themselves.

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

#69

Post by zwnow »

moffkalast wrote: post #67
zwnow wrote: post #65

Earlier quoted context omitted.

Experts are adamant about this. Just take a look at https://youtu.be/iRqpsCHqLUI

No such thing as an expert consensus on anything about LLMs these days, just different forms of grift. My point is, the question if an LLM reasons the same way a human does is about as useful as "does a submarine swim" or "can a telephone talk". The results speak for themselves.

LLMs do not reason. Not hard to understand.

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

#70

Post by Terr_ »

aSanchezStern wrote: post #15
measurablefunc wrote: post #5

This is proof of verifiable logic. Computers can not think so calling it proof of thought misrepresents what's actually happening.

I agree that "proof of thought" is a misleading name, but this whole "computers can't think" thing is making LLM skepticism seem very unscientific. There is no universally agreed upon objective definition of what it means to be able to "think" or how you would measure such a thing. The definition that these types of positions seem to rely upon is "a thing that only humans can do", which is obviously a circular one th…

> this whole "computers can't think" thing is making LLM skepticism seem very unscientific.

It's just shorthand for "that's an extraordinary claim and nobody has provided any remotely extraordinary evidence to support it."

Post reply on HN