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

151–160 of 182 posts

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

#151

Post by MASNeo »

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

That’s nailing it really well: “willfully ignoring” is precisely what’s happening all around me. Me talking about small focused AI models, there you have everyone raving about AGI. Energy use and privacy issues of cloud vs local inference discussions end on how awesome the power of GPUs are and the jobs too. GPU backed finance with depreciation schedules past useful life seems OK for anyone chasing some short term gain. Even the job market is troubled, you can hardly tell a relevant candidate from an irrelevant one because everyone is an AI expert these days - hallucinations seem to make lying more casual.

It’s pretty clear to me there is a collective desire to ignore the problems to sell more GPU, close the next round, get that high paying AI job.

Part of me wishes humans would show the same dedication to fight climate change…

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

#152

Post by bonoboTP »

Barbing wrote: post #99
psadri wrote: post #86

Earlier quoted context omitted.

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)

If you like Matrix, Memento, Truman Show, Black Mirror (San Junipero, Bandersnatch), Inception, Interstellar, 12 Monkeys etc. you may also like it. These are not necessarily thematically aligned but based on vibes they cluster near it for me.

I definitely enjoyed it many years ago as a younger person.

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

#153

Post by enknee1 »

visarga wrote: post #109
emporas wrote: post #103

Earlier quoted context omitted.

Small steps of nondeterministic computation, checked thoroughly with deterministic computation every so often, and the sky is the limit. That's when A.I. starts advancing itself and needs humans in the loop no more.

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

Simulated environment suggests the possibility of alignment during training but real time, real world, data streams are better.

But the larger point stands: you don't need an environment to explore the abstraction landscape prescribed by systems thinking. You only need the environment at the human interface.

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

#154

Post by self »

Barbing wrote: post #99
psadri wrote: post #86

Earlier quoted context omitted.

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)

Three movies with overlapping themes came out in mid-1999: The Matrix, The Thirteenth Floor, and eXistenZ (probably in that order of box office revenue).

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

#155

Post by [deleted] »

kgeist wrote: post #149
zwnow wrote: post #131

Earlier quoted context omitted.

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.

[deleted]

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

#156

Post by encyclopedism »

kgeist wrote: post #149
zwnow wrote: post #131

Earlier quoted context omitted.

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.

> Is it really much different from most people? The average Joe doesn't produce novel theories every day"

You've presented a false choice.

However the average Joe does indeed produce unique and novel thoughts every day. If it were not the case he would be brain dead. Each decision - wearing blue or red today - every tiny thought, action, feeling, indecision, crisis, or change of heart these are just as important.

The jury maybe out on how to judge what 'thought' actually is. However what it is not is perhaps easier to perceive. My digital thermometer does not think when it tells me the temperature.

My paper and pen version of the latest LLM (quite a large bit of paper and certainly a lot of ink I might add) also does not think.

I am surprised so many in the HN community have so quickly taken to assuming as fact that LLM's think or reason. Even anthropomorphising LLM's to this end.

For a group inclined to quickly calling out 'God of the gaps' they have quite quickly invented their very own 'emergence'.

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

#157

Post by DrewADesign »

afiori wrote: post #143
DrewADesign wrote: post #78

Earlier quoted context omitted.

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

All of those tools are purpose-built for moving people. LLMs are not at all built for doing math.

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

#158

Post by [deleted] »

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…

[deleted]

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

#159

Post by encyclopedism »

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…

The jury maybe out on how to judge what 'thought' actually is. However what it is not is perhaps easier to perceive. My digital thermometer does not think when it tells me the temperature.

My paper and pen version of the latest LLM (quite a large bit of paper and certainly a lot of ink I might add) also does not think.

I am surprised so many in the HN community have so quickly taken to assuming as fact that LLM's think or reason. Even anthropomorphising LLM's to this end.

For a group inclined to quickly calling out 'God of the gaps' they have quite quickly invented their very own 'emergence'.

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

#160

Post by dang »

vasco wrote: post #128
dang wrote: post #58

Earlier quoted context omitted.

I believe you! but when an internet reply leads with "what are you talking about?", it's likely to pattern-match this way for many readers. If that's not your intent, it's best to use an alternate wording.

Not to be rude, but they clarified it's not a snide, why are you trying to control speech to this degree? If we don't like his tone we can downvote him as well anyway and self regulate.

They clarified that their intention was good, but intent doesn't communicate itself—it needs to be disambiguated [1]. What matters in terms of moderation is not intent, but effects, i.e. effects on the system in the general case [2].

Arguably your question reduces to: why does HN have moderators at all? The answer to that is that unfortunately, the system of community + software doesn't function well on its own over time—it falls into failure modes and humans (i.e. mods) are needed to jig it out of those [3]. I say "unfortunately" because, of course, it would be so much better if this weren't needed.

You can't assess this at the level of an individual interaction, though, because it's scoped at the whole-system level. That is, we can (and do) make bad individual calls, but what's important is how the overall system functions. If you see the mods making a mistake, you're welcome to point it out (and HN users are not shy about doing so!), and we're happy to correct it. But it doesn't follow that you don't need moderators for the system to work, or even survive.

[1] https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...

[2] https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...

[3] https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...

Post reply on HN