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

71–80 of 182 posts

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

#71

Post by Terr_ »

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.

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

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

#72

Post by varispeed »

0xWTF wrote: post #59

Am I reading this right? Statistical LLM outputs pushed through a formal logic model? Wouldn't that be a case of "crap in, crap out"?

That's subjective. One could argue all the things we invented in the past few thousands years were crap. Life would have been much easier in the caves, albeit shorter.

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

#73

Post by moffkalast »

zwnow wrote: post #69
moffkalast wrote: post #67

Earlier quoted context omitted.

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.

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 differently. Having legs would even be a major detriment and would hold it back from achieving its top performance.

That's what those brain simulating projects are conceptually btw: cars with legs or planes with flapping wings. That's why they all fail, the approach makes no sense.

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

#74

Post by everdrive »

NotGMan wrote: post #46
everdrive wrote: post #39

I'm honestly confused why we can't determine how LLMs come to their decisions in the general sense. Is it not possible to log every step as the neural network / vector db / magic happens? Is it merely impractical, or is it actually something that's genuinely difficult to do?

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?

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

#75

Post by sytse »

So the core idea is to use an LLM to draft reasoning as a structured, JSON domain-specific language (DSL), then deterministically translate that into first-order logic and verify it with a theorem prover (Z3).

Interesting that the final answer is provably entailed (or you get a counterexample), instead of being merely persuasive chain-of-thought.

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

#76

Post by avmich »

0xWTF wrote: post #59

Am I reading this right? Statistical LLM outputs pushed through a formal logic model? Wouldn't that be a case of "crap in, crap out"?

Formal logic serves as a useful filter. In other words, "crap in, filtered crap out" - remember, evolution works with absolutely random, "crap" mutations, which then are "filtered" by the environment.

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

#77

Post by patcon »

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.

I love this kind of thought. Thanks.

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

#78

Post by DrewADesign »

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 get having it walk you through figuring out a problem with a tool: seems like a good idea and it clearly worked even better than expected. But deliberately coaxing an LLM into doing math correctly instead of a CAS because you’ve got one handy seems like moving apartments with dozens of bus trips rather than taking the bus to a truck rental place, just because you’ve already got a bus pass.

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

#79

Post by avmich »

measurablefunc wrote: post #63
supern0va wrote: post #53

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

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

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

#80

Post by avmich »

Terr_ wrote: post #71
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.

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?
Post reply on HN