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

131–140 of 182 posts

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

#131

Post by zwnow »

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…

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.

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

#132

Post by jansan »

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?

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

#133

Post by measurablefunc »

elcomet wrote: post #23
zwnow wrote: post #19

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

How can you know?

By thinking about what a computer is actually doing & realizing that attributing thought to an arthmetic gadget leads to all sorts of nonsensical consequences like an arrangement of dominoes & their cascade being a thought. The metaphysics of thinking computers is incoherent & if you study computability theory you'll reach the same conclusion.

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

#134

Post by measurablefunc »

moffkalast wrote: post #120
raspasov wrote: post #101

Earlier quoted context omitted.

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?

Yes, exactly. There are other papers, but Google proved it most definitively imo [0], an LLM now holds the state of the art for the lowest bound on a very specific graph problem. [0] https://research.google/blog/ai-as-a-research-partner-advanc...

That's not an LLM. AlphaEvolve is a variant of genetic search for program synthesis. Very different from the chat bot that answers questions about ingrown toenails.

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

#136

Post by elcomet »

measurablefunc wrote: post #133
elcomet wrote: post #23

Earlier quoted context omitted.

How can you know?

By thinking about what a computer is actually doing & realizing that attributing thought to an arthmetic gadget leads to all sorts of nonsensical consequences like an arrangement of dominoes & their cascade being a thought. The metaphysics of thinking computers is incoherent & if you study computability theory you'll reach the same conclusion.

I'd say that thoughts and reasoning are two different things, you're moving the goalpost.

But what makes the computer hardware fundamentally incompatible with thinking? Compared to a brain

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

#137

Post by measurablefunc »

elcomet wrote: post #136
measurablefunc wrote: post #133

Earlier quoted context omitted.

By thinking about what a computer is actually doing & realizing that attributing thought to an arthmetic gadget leads to all sorts of nonsensical consequences like an arrangement of dominoes & their cascade being a thought. The metaphysics of thinking computers is incoherent & if you study computability theory you'll reach the same conclusion.

I'd say that thoughts and reasoning are two different things, you're moving the goalpost. But what makes the computer hardware fundamentally incompatible with thinking? Compared to a brain

I've already explained it in several places. The burden of proof is on those drawing the equivalence to provide actual evidence for why they believe carbon & silicon are interchangeable & why substrate independence is a valid assumption. I have studied this problem for much longer than many people commenting on this issue & I am telling you that your position is metaphysically incoherent.

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

#138

Post by Nevermark »

measurablefunc wrote: post #50
bobxmax wrote: post #35

Earlier quoted context omitted.

[flagged]

Not arithmetic or boolean algebra. What's your definition?

> Not arithmetic or boolean algebra.

That isn’t a definition or even a coherent attempt.

For starters, what kind of cognition or computation can’t be implemented with either logic or arithmetic?

What is or is not “cognition” is going to be a higher level property than what basic universally capable substrate is used. Given such substrates can easily simulate each other, be substituted for each other.

Even digital and analog systems can be used to implement each other to arbitrary accuracy.

Cognition is a higher level concern.

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

#139

Post by Nevermark »

measurablefunc wrote: post #49
chpatrick wrote: post #42

Earlier quoted context omitted.

Do you understand human thinking well enough to determine what can think and what can't? We have next to no idea how an organic brain works.

I understand computers, software, & the theory of computation well enough to know that there is no algorithm or even a theoretical algorithmic construction that can be considered thought. Unless you are willing to concede that thinking is nothing more than any number of models equivalent to a Turing machine, e.g. lambda calculus, Post systems, context aware grammars, carefully laid out dominoes, permutations of bit s…

You are confusing primitives with things built with those primitives.

Complex phenomena emerge from interactions of things that don’t exhibit that phenomena all the time.

Atoms can’t think. In no sense can you find any thinking in an atom.

They are no different from dominos in that respect.

You can pile atoms to the moon without seeing any thinking.

Yet they can still be arranged so they do think.

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

#140

Post by Nevermark »

measurablefunc wrote: post #94
chpatrick wrote: post #91

Earlier quoted context omitted.

Sure, sufficiently advanced dominoes. https://xkcd.com/505/ We're already at the point where LLMs can beat the Turing test. If we define thinking as something only humans can do, then we can't decide if anyone is thinking at all just by talking to them through text, because we can't tell if they're human any more.

Animals can also think. It's not restricted to one specific type of primate physiology. But it seems like you think you're nothing more than falling cascades of dominoes in which case we don't really have much to discuss. Your metaphysical assumptions are fundamentally at odds with what I consider a reasonable stance on computation & reality.

> Animals can also think

What are you saying?

Are you saying you have a clear definition for thinking, and you can demonstrate that animals pass that definituon?

Then share the definition.

Or are you simply defining thinking as a common property of humans and animals, using animals and human behavior as exemplars?

A useful definition for focusing inquiry. But it does not clarify or constrain what else might or might not be enabled to think.

Or are you defining thinking as an inherent property of animals and humans that other things cannot have because they are not animals or humans?

Fine, but that that’s an exercise in naming. Something we are all free to do however we want. It has no explanatory power.

Post reply on HN