RHEL knife-edge rolling kernel distribition for the proof of concept.
ProofOfThought: LLM-based reasoning using Z3 theorem proving
121–130 of 182 posts
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#122Earlier quoted context omitted.
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.
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 a few more nuclear power plants & a few more GPU clusters is all that's needed.
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#123Earlier quoted context omitted.
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…
> this whole "computers can't think" thing is making LLM skepticism seem very unscientific. It's just shorthand for "that's an extraordinary claim and nobody has provided any remotely extraordinary evidence to support it."
Lots of people consider company valuations evidence of a singularity right around the corner but it requires a very specific kind of mindset to buy into that as "proof" of anything other than very compelling hype by people who have turned financial scams into an art form.
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#124Interesting. I wonder if you could implement tool calling with this approach so the LLM calls the tool with the formal specification and gets back the result. Just like a coding agent can run a compiler, get back errors and then self-correct.
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#125What industrial problems would this solve?
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#126[deleted]
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#127Earlier quoted context omitted.
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 intelligenc…
[dead]
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#128Earlier quoted context omitted.
This is not meant as snide, I'm literally confused if I might have misunderstood the problem here. Because the solution would be so obvious.
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.
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#129LLMs are statistical language models (d'uh) not reasoners after all. I found generating logic programs, and Prolog source specifically, to work unreasonably well, though [1], maybe because Prolog was introduced for symbolic natural language processing and there's a wealth of translation examples in the training set. Might be worth checking out Z3's alternative Datalog syntax [2] instead of its Lisp-ish SMTLib syntax.…
Neuralsymbolic systems are very likely the future as so many times mentioned here already.
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#130Earlier 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.
> just different forms of grift That sounds like a false "both sides"-ing. It's not symmetrical, there's a lot more money (and potential to grift) hyping things up as miracle machines. In contrast, most of the pessimists don't have a discernible profit motive.
Well yes the corporate accelerationists are certainly pushing for it the most, shoehorning the tech into things it doesn't belong in to see if they can somehow come up on top, which that in turn makes lots of people resentful towards it in a reactionary way.
You have artists who've lost work due to diffusion models, teachers who can't assign homework essays anymore, people who hate Microsoft Copilot, just anyone not wanting to be replaced by a bot or being forced to use the tech to avoid being outcompeted, people set in their ways who don't want change or imagine it being destructive, etc. It's a large crowd that one can appeal to for personal gain, politics 101. Anyone with half believable credentials can go on a talk show and say the things people want to hear, maybe sell a book or two afterwards.
Are today's models on the brink of some exponential self perpetuating shot towards superintelligence? Obviously not. Are they overhyped glorified lookup tables? Also no. Are there problems? Definitely. But I don't think it's entirely fair to dismiss a tech based on someone misappropriating it in monopolistic endeavours instead of directing dismissal towards those people themselves.
Like, similar to how Elon's douchebaggery has tainted EVs for lots of people for no practical reason, the same has Altman's done for LLMs.