ProofOfThought: LLM-based reasoning using Z3 theorem proving • Hacker News Board

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

#111

Post by galaxyLogic » Sun, Oct 05, 2025, 4:45 AM UTC

tomcloyd wrote: post #95

pstoll wrote: post #88

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

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.

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

#112

Post by eru » Sun, Oct 05, 2025, 4:48 AM UTC

emporas wrote: post #107

eru wrote: post #105

Earlier quoted context omitted.

Your checks don't have to be deterministic either. Eg randomised quicksort works really well.

Couldn't disagree more. Sorting a finite number of elements in a sequence, is a very narrow application of AI, akin to playing chess. Usually very simple approaches like RL work totally fine for problems like these, but auto-regression/diffusion models have to take steps that are not well defined at all, and the next step towards solving the problem is not obvious. As an example, imagine a robot trying to grab a toma…

> Sorting a finite number of elements in a sequence, is a very narrow application of AI, [...]

Sorry, I did not suggest you should use AI to sort numbers. I was solely replying to this:

> Small steps of nondeterministic computation, checked thoroughly with deterministic computation every so often, and the sky is the limit.

You don't necessarily need your checks to be deterministic.

In fact, it's often better for them to be not deterministic.

I don't understand your claim about 'Deterministic computation is faster, cheaper and more secure.' That's not true at all.

In fact, for many problems the fastest and simplest known solutions are non-deterministic. And in eg cryptography you _need_ non-determinism to get any security at all.

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

#113

Post by jaggederest » Sun, Oct 05, 2025, 5:00 AM UTC

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…

Simulation is the answer. You just need a model that's decent at economics to independently judge the outcome, unless the model itself is smart enough. Then it becomes a self-reinforcing training environment.

Now, depending on how good your simulation is, it may or may not be useful, but still, that's how you do it. Something like https://en.wikipedia.org/wiki/MuZero

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

#114

Post by chandureddyvari » Sun, Oct 05, 2025, 5:14 AM UTC

LASR wrote: post #2

This is an interesting approach. My team has been prototyping something very similar with encoding business operations policies with LEAN. We have some internal knowledge bases (google docs / wiki pages) that we first convert to LEAN using LLMs. Then we run the solver to verify consistency. When a wiki page is changed, the process is run again and it's essentially a linter for process. Can't say it moved beyond the p…

For anyone curious about what LEAN is, like me, here’s the explanation: Lean Theorem Prover is a Microsoft project. You can find it here: https://www.microsoft.com/en-us/research/project/lean/

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

#115

Post by baq » Sun, Oct 05, 2025, 5:31 AM UTC

0xWTF wrote: post #59

Am I reading this right? Statistical LLM outputs pushed through a formal logic model? Wouldn't that be a case of "crap in, crap out"?

You assume it’s all crap when it clearly isn’t often enough to be useful.

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

#116

Post by fnordpiglet » Sun, Oct 05, 2025, 5:38 AM UTC

CuriouslyC wrote: post #16

nextos wrote: post #8

This is a very interesting area of research. I did something similar a couple of years ago using logic and probabilistic logic inference engines to make sure conclusions followed from premises. I also used agents to synthesize, formalize, and criticize domain knowledge. Obviously, it is not a silver bullet, but it does ensure some degree of correctness. I think introducing some degree of symbolism and agents-as-a-jud…

Agent/LLM as a judge is biased and only good for bootstrapping. As capabilities get better LLM as a judge will artificially cap your performance, you need to graduate to either expert human judges or deterministic oracles.

LLMs display a form of abductive reasoning which is not the same as judgement. The only thing in the universe we know that can display judgement is a human. However many tasks we presume to require human judgement do not and abductive reasoning will perform as well as a human. This in theory acts as a filter if used right reducing the tasks of human judgement to those that can’t be automated with similar or better precision and recall. The trick then is using LLMs and other techniques to reduce the problem space for the human to the kernel of quandary that requires human judgement and to isolate the salient information to reduce the cognitive load as much as possible. Many many mundane tasks can be automated in this way, and many complex tasks can be facilitated to greatly magnify the effectiveness of the human in the middle’s time.

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

#117

Post by baq » Sun, Oct 05, 2025, 5:40 AM UTC

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.

Hard to argue with religious beliefs.

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

#118

Post by Terr_ » Sun, Oct 05, 2025, 5:46 AM UTC

moffkalast wrote: post #67

zwnow wrote: post #65

Earlier quoted context omitted.

Experts are adamant about this. Just take a look at https://youtu.be/iRqpsCHqLUI

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.

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

#119

Post by staplers » Sun, Oct 05, 2025, 5:46 AM UTC

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…

  doable but not easy, for business ideas

That requires a lot of human psychology and advanced hard economic theory (not the fluffy academic kind). With human controlled monetary supply and most high-level business requiring illegal and immoral exploitation of law and humans in general, it's not a path machines can realistically go down or even want machines treading down.

Think scams and pure resource extraction. They won't consider many impacts outside of bottom line.

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

#120

Post by moffkalast » Sun, Oct 05, 2025, 5:58 AM UTC

raspasov wrote: post #101

moffkalast wrote: post #73

Earlier quoted context omitted.

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…

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