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

141–150 of 182 posts

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

#141

Post by Nevermark »

measurablefunc wrote: post #122
baq wrote: post #117

Earlier quoted context omitted.

Hard to argue with religious beliefs.

The void created by modernity must be filled somehow so it might as well be the great programmer in the great beyond. Just as childish as religions of pre-modernity but very useful if you're a technocrat building data centers & trying to pump the valuations of companies that can benefit from all that buildout w/ promises of forthcoming utopias approximating the palace of the great programmer in the great beyond. Just…

Ideally it is filled with curiosity and continued exploration.

Not manufactured stop gaps or generic cynicism.

There is no reason more GPUs can’t contribute to further understanding, as one of many tools that have already assisted with relevent questions and problems.

Opt out of serious inquiry, no excuse needed, if you wish. Reframing others efforts is not necessary to do that.

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

#142

Post by QuesnayJr »

measurablefunc wrote: post #122
baq wrote: post #117

Earlier quoted context omitted.

Hard to argue with religious beliefs.

The void created by modernity must be filled somehow so it might as well be the great programmer in the great beyond. Just as childish as religions of pre-modernity but very useful if you're a technocrat building data centers & trying to pump the valuations of companies that can benefit from all that buildout w/ promises of forthcoming utopias approximating the palace of the great programmer in the great beyond. Just…

I think you are misjudging which side of the religion/non-religion divide you are on.

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

#143

Post by afiori »

DrewADesign wrote: post #78
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.

I feel like a better analogy is trying to rent a truck to move to a new apartment and after repeated failures of trucks not working they just hire a moving company for you to get you to leave

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

#144

Post by measurablefunc »

QuesnayJr wrote: post #142
measurablefunc wrote: post #122

Earlier quoted context omitted.

The void created by modernity must be filled somehow so it might as well be the great programmer in the great beyond. Just as childish as religions of pre-modernity but very useful if you're a technocrat building data centers & trying to pump the valuations of companies that can benefit from all that buildout w/ promises of forthcoming utopias approximating the palace of the great programmer in the great beyond. Just…

I think you are misjudging which side of the religion/non-religion divide you are on.

The people who think enough nuclear reactors & silicon chips w/ the right incantation of 0s & 1s will deliver them to an abundant utopia don't leave much room in their ideology for any doubt about the eschatological objective of their quest & mission in life. These people are definitely not on some kind of religious side of a religious vs non-religious divide.

Sure thing buddy, I'm the confused one in this entire millenarian frenzy.

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

#145

Post by 7734128 »

jansan wrote: post #132
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…

How die that work? Did Gemini call sympy on your maschine, or is access to sympy built-in and available through normal chat?

https://cloud.google.com/vertex-ai/generative-ai/docs/multim...

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

#146

Post by measurablefunc »

Nevermark wrote: post #141
measurablefunc wrote: post #122

Earlier quoted context omitted.

The void created by modernity must be filled somehow so it might as well be the great programmer in the great beyond. Just as childish as religions of pre-modernity but very useful if you're a technocrat building data centers & trying to pump the valuations of companies that can benefit from all that buildout w/ promises of forthcoming utopias approximating the palace of the great programmer in the great beyond. Just…

Ideally it is filled with curiosity and continued exploration. Not manufactured stop gaps or generic cynicism. There is no reason more GPUs can’t contribute to further understanding, as one of many tools that have already assisted with relevent questions and problems. Opt out of serious inquiry, no excuse needed, if you wish. Reframing others efforts is not necessary to do that.

I recommend taking your own advice on that one, specifically the part about reframing efforts of strangers.

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

#147

Post by YeGoblynQueenne »

barthelomew wrote: post #32
nakamoto_damacy wrote: post #17

LLMs lack logical constraints in the generative process; they only learn probabilistic constraints. If you apply logic verification post-hoc, you're not "ensuring the correctness of your LLMs reasoning" (I went down this path a year ago); you're classifying whether the LLM's statistically driven pattern generation happens to correspond to correct logic or not, where the LLMs output may be wrong 100% of the time, and…

Yep, this is a genuine problem, and this is what we term as the autoformalization gap in our follow up paper. ( https://arxiv.org/abs/2505.20047 ) Some LLMs are more consistent between text and SMT, while others are not. (Tab 1, Fig 14,15) You can do uncertainty quantification with selective verification to reduce the "risk", for e.g. shown as the Area Under the Risk Coverage Curve in Tab 4.

Well, if you understand that this is a "genuine problem" then what have you done to solve it? A quick look at the abstract of your follow up paper does not reveal an answer.

And let me be clear that this is a major limitation that fundamentally breaks whatever you are trying to achieve. You start with some LLM-generated text that is, by construction, unrelated to any notion of truth or factuality, and you push it through a verifier. Now you are verifying hot air.

It's like research into the efficacy of homeopathic medicine and there's a lot of that indeed, very carefully performed and with great attention to detail. Except all of that research is trying to prove whether doing nothing at all (i.e. homeopathy) has some kind of measurable effect or not. Obviously the answer is not. So what can change that? Only making homeopathy do something instead of nothing. But that's impossible, because homeopathy is, by construction, doing nothing.

It's the same thing with LLMs. Unless you find a way to make an LLM that can generate text that is conditioned on some measure of factuality, then you can verify the output all you like, the whole thing will remain meaningless.

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

#148

Post by drbojingle »

jaggederest wrote: post #113
visarga wrote: post #109

Earlier quoted context omitted.

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

Simulation is the answer. You just need a model that's decent at economics to independently judge the outcome, unless the model itself is smart enough. Then it becomes a self-reinforcing training environment. Now, depending on how good your simulation is, it may or may not be useful, but still, that's how you do it. Something like https://en.wikipedia.org/wiki/MuZero

Electric dreams. Simulation of what?

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

#149

Post by kgeist »

zwnow wrote: post #131
moffkalast wrote: post #73

Earlier quoted context omitted.

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…

If LLMs could reason, they would flourish in barely understood topics, they dont. They repeat after what humans already said over and over again all across the training data. They are a parrot, its really not that hard to understand.

>They repeat after what humans already said

>They are a parrot

Is it really much different from most people? The average Joe doesn't produce novel theories every day - he just rehashes what he's heard. Now the new goalpost seems to be that we can only say an LLM can "reason" if it matches Fields Medalists.

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

#150

Post by NitpickLawyer »

zwnow wrote: post #131
moffkalast wrote: post #73

Earlier quoted context omitted.

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…

If LLMs could reason, they would flourish in barely understood topics, they dont. They repeat after what humans already said over and over again all across the training data. They are a parrot, its really not that hard to understand.

> They are a parrot

Those are some mighty parrots there, if they managed to get gold at IMO, IoI, and so on...

Post reply on HN