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

91–100 of 182 posts

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

#91

Post by chpatrick »

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…

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.

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

#93

Post by nakamoto_damacy »

I posted about my year long development effort of this very method on reddit 25 days ago. My comment elsewhere in this thread provides a cautionary tale, and the authors response to the basic issue I raised is incomplete in that it leaves out that certain problems simply cannot be solved with LLMs (requires logical constraints in the generative process but LLMs lack that layer) So I've pivoted to something else since (also mentioned in my comment elsewhere in this thread)

https://www.reddit.com/r/healthIT/comments/1n81e8g/comment/n...

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

#94

Post by measurablefunc »

chpatrick wrote: post #91
measurablefunc wrote: post #49

Earlier quoted context omitted.

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…

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.

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

#95

Post by tomcloyd »

pstoll wrote: post #88
29athrowaway wrote: post #87

Earlier quoted context omitted.

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.

As a psychologist, I completely agree. It absolutely is NOT number crunching. Analog computation is primary and dominant in animals. It has to be, for so many reasons. I continue to be amazed at how much IT people do NOT grasp human and animal IT. And that, I would argue, is why so many IT folks keep talking about our supposedly approaching human intelligence in technology. If they really understood human intelligence the absurdity of that statement would keep them quiet. An elegant, artful puppet is still a puppet, and without the personal history context and consciousness we possess, not to mention a vast complex of analogue computation functionality we rely upon, that puppet will only ever be a clever number-cruncher. We are so much more.

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

#96

Post by nakamoto_damacy »

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…

Why is this being down voted? I believe the author acknowledged and responded. Anything wrong?

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

#97

Post by HumanOstrich »

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.

Neurons aren't crunching numbers for inverse kinematics.

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

#98

Post by tymscar »

typpilol wrote: post #89
everdrive wrote: post #74

Earlier quoted context omitted.

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.

That’s so much faster than I expected

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

#99

Post by Barbing »

psadri wrote: post #86
jonplackett wrote: post #62

Earlier quoted context omitted.

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”

This is somewhat unusual: 28% on the Tomatometer, but 7 out of 10 on IMDb.

Beyond its relevancy to the parent comment, would you consider it a good movie yourself? (for a random/average HN commenter to watch)

Post reply on HN