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

161–170 of 182 posts

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

#161

Post by a3w »

larodi wrote: post #129
tannhaeuser wrote: post #52

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

I cannot use wolframalpha most of the time since the syntax is not that natural. WolframAlpha is good AI, it never lies.

Calculators are good AI, they rarely lie (due to floating arithmetics rounding). And yes, Wikipedia says calculators are AI tech, since a Computer was once a person, and not it is a tool that shows the intelligent trait of doing math with numbers or even functions/variables/equations.

Querying a calculator or wolfram alpha like symbolic AI system with LLMs seems like the only use for LLMs except for text refactoring that should be feasible.

Thinking LLMs know anything on their own is a huge fallacy.

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

#162

Post by everdrive »

moffkalast wrote: post #47
everdrive wrote: post #39

I'm honestly confused why we can't determine how LLMs come to their decisions in the general sense. Is it not possible to log every step as the neural network / vector db / magic happens? Is it merely impractical, or is it actually something that's genuinely difficult to do?

It would be like logging a bunch of random noise from anyone's perspective except the LLM's.

I guess I'm also just confused. I get that this is _difficult_ to do, but I would think that computer scientists would be utterly dissatisfied that AI was "non-deterministic" and would poke at the problem until it could be understood.

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

#163

Post by everdrive »

konmok wrote: post #48
everdrive wrote: post #39

I'm honestly confused why we can't determine how LLMs come to their decisions in the general sense. Is it not possible to log every step as the neural network / vector db / magic happens? Is it merely impractical, or is it actually something that's genuinely difficult to do?

My understanding is that it's neither impractical nor genuinely difficult, it's just that the "logging every step" approach provides explanations of their "reasoning" that are completely meaningless to us, as humans. It's like trying to understand why a person likes the color red, but not the color blue, using a database recording the position, makeup, and velocity of every atom in their brain. Theoretically, yes, th…

>It's like trying to understand why a person likes the color red, but not the color blue, using a database recording the position, makeup, and velocity of every atom in their brain.

But this is an incredibly interesting problem!

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

#164

Post by [deleted] »

everdrive wrote: post #74
NotGMan wrote: post #46

Earlier quoted context omitted.

Chat GPT-4 has alegedly 1.8 trillion parameters. Imagine having a bunch of 2D matrices with a combined 1.8 trillion total numbers, from which you pick out a blocks of numbers in a loop and finally merge them and combine them to form a token. Good luck figuring out what number represents what.

Wouldn't that mean it's totally impractical for day-to-day usage, but a researcher or team of researchers could solve this?

[deleted]

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

#165

Post by nickpsecurity »

everdrive wrote: post #39

I'm honestly confused why we can't determine how LLMs come to their decisions in the general sense. Is it not possible to log every step as the neural network / vector db / magic happens? Is it merely impractical, or is it actually something that's genuinely difficult to do?

There's people doing both types. Look up survey of mechanistic interpretebility of language models and survey of explainable AI for neural networks. Those will give you many techniques for illustrating what's happening.

You'll also see why their applications are limited compared to what you probably hoped for.

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

#166

Post by zwnow »

NitpickLawyer wrote: post #150
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 are a parrot Those are some mighty parrots there, if they managed to get gold at IMO, IoI, and so on...

Well understood topics... what's so hard to understand?

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

#167

Post by qcnguy »

everdrive wrote: post #163
konmok wrote: post #48

Earlier quoted context omitted.

My understanding is that it's neither impractical nor genuinely difficult, it's just that the "logging every step" approach provides explanations of their "reasoning" that are completely meaningless to us, as humans. It's like trying to understand why a person likes the color red, but not the color blue, using a database recording the position, makeup, and velocity of every atom in their brain. Theoretically, yes, th…

>It's like trying to understand why a person likes the color red, but not the color blue, using a database recording the position, makeup, and velocity of every atom in their brain. But this is an incredibly interesting problem!

Anthropic have done some great work on neural interpretability that gets at the core of this problem.

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

#168

Post by fwip »

galaxyLogic wrote: post #111
tomcloyd wrote: post #95

Earlier quoted context omitted.

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…

Are our brains "analog"? Or are they in fact "digital"? I would think actually more digital than analog. A synapse triggers or it does not trigger. It either triggers or not, not something in between. In this sense it is 0 or 1. Similarly transistor-based logic is based on such thresholds, when current or voltage reaches a certain level then a state-transition happens.

Well, no, synapses aren't binary in response.

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

#169

Post by Nevermark »

measurablefunc wrote: post #146
Nevermark wrote: post #141

Earlier quoted context omitted.

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.

I take your views to be exactly as you state them.

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

#170

Post by Flere-Imsaho »

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.

Would you say it's more memorization than actual calculations? It certainly feels like it, when say riding a bike.
Post reply on HN