Cool research! I went to the repo to see what the DSL looked like but it was hard to find a clear example. It would be cool if you added a snippet to the README.
ProofOfThought: LLM-based reasoning using Z3 theorem proving
41–50 of 182 posts
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#42This is proof of verifiable logic. Computers can not think so calling it proof of thought misrepresents what's actually happening.
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.
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#43LLMs 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…
Probabilistic constraints are all around us. You learn that the sine function is the ratio of the length of the side of the right triangle opposite to the angle to the length of the side opposite to the right angle, so obviously the sine is always positive. Yet your thinking should be flexible enough to allow changing the definition to the ordinate of the point on the unit circle where the line corresponding to the g…
You're thinking along the right track but without formalization it goes nowhere fast. By layering of differential geometry on top of probability and then maybe category theoretic logic on top of that, each layer constraining the one below it, and all layers cohering, you get somewhere... There is work that's been done in this area, and I was recently interviewed by a journalist who published a high level article on it on Forbes (Why LLMs are failing) and it links to the actual technical work (at first to my high level presentation then Prof. L. Thorne McCarty's work): https://www.forbes.com/sites/hessiejones/2025/09/30/llms-are...
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#44Earlier quoted context omitted.
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.
Why does this have to be true? For example, if you have a different LLM that is judging than the one being judged then their biases could at least be different. Also, as their reasoning abilities improve wouldn't LLM judges approach the abilities of human judges?
LLMs have positional, response length and hedge word biases (and that's just what's rigorously demonstrated in papers) that wash out differences between high performing answers as you approach the limit of your objective. Imagine if you were trying to optimize a function and the measurement function emitted random biased noise, at some point you wouldn't be able to accurately identify the impact of your changes.
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#45Earlier quoted context omitted.
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.
Why does this have to be true? For example, if you have a different LLM that is judging than the one being judged then their biases could at least be different. Also, as their reasoning abilities improve wouldn't LLM judges approach the abilities of human judges?
Indeed - human judges suck on average. And you can prompt an llm judge to look for particular kinds of problems, then throw the ensemble of judges at an output to nitpick. (Essentially, bake in a diversity of biases through a collection of prompts.)
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#46I'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?
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.
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#47I'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.
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#48I'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, that should be sufficient to explain their color preferences, in that it fully models their brain. But practically, the explanation would be phrased in terms of atomic configurations in a way that makes much less sense to us than "oh, this person likes red because they like roses".
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#49This is proof of verifiable logic. Computers can not think so calling it proof of thought misrepresents what's actually happening.
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 strings, etc. then you must admit that computers are not thinking. If you believe computers are thinking then you must also admit dominoes are thinking when falling in a cascading chain.
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#50Earlier quoted context omitted.
If you believe computers can think then you must be able to explain why a chain of dominoes is also thinking when I convert an LLM from transistor relay switches into the domino equivalent. If you don't fall for the marketing hype & study both the philosophical & mathematical literature on computation then it is obvious that computers (or any mechanical gadget for that matter) can not qualify for any reasonable defin…
[flagged]
Not arithmetic or boolean algebra. What's your definition?