11 ms·
ProofOfThought: LLM-based reasoning using Z3 theorem proving
https://arxiv.org/abs/2409.17270 https://arxiv.org/abs/2409.17270
- LASR 1y agoThis 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 prototyping stage though, since the LEAN conversion does require some engineers to look through it at least. But a promising approach indeed, especially when you have a domain that requires tight legal / financial compliance.
- viraptor 1y agoCould you share an example of such policy? I'm struggling to think of something defined well enough in the real world to apply in Lean.
- barthelomew 1y agoThe autoformalization gap is pretty difficult to bridge indeed. We explored uncertainty quantification of autoformalization on well-defined grammars in our NeurIPS 2025 paper : https://arxiv.org/abs/2505.20047 https://arxiv.org/abs/2505.20047 . If you ever feel like chatting and discussing more details, happy to chat!
- pbronez 1y agoThat’s pretty cool. It would be super useful to identify contradictory guidance systematically.
- chandureddyvari 1y agoFor 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/ https://www.microsoft.com/en-us/research/project/lean/
- ashandoak 1y agoLean has been under development over the last 13 years, part of that while chief architect Leo de Moura was employed by Microsoft Research (he's now at AWS). However, Lean is an open source project, not exclusively a Microsoft project. More accurately, see here: https://lean-lang.org/ https://lean-lang.org/
- sigmoid10 1y agoI always find it amazing how many people seem to fail to use current LLMs to the fullest, even though they apparently work with them in research settings. This benchmark pipeline simply calls the OpenAI API and then painstakingly tries to parse the raw text output into a structured json format, when in reality the OpenAI API has supported structured outputs for ages now. That already ensures your model generates schema compliant output without hallucinating keys at the inference level. Today all the major providers support this feature either directly or at least indirectly via function calling. And if you run open models, you can literally write arbitrary schema (i.e. not limited to json behind the scenes) adhering inference engines yourself with rather manageable effort. I'm constantly using this in my daily work and I'm always baffled when people tell me about their hallucination problems, because so many of them can be fixed trivially these days.
- atrus 1y agoI wouldn't find it amazing, there are so many new models, features, ways to use models that the minute you pause to take a deep dive into something specific, 43 other things have already passed by you.
- sigmoid10 1y agoI would agree if you are a normal dev who doesn't work in the field. But even then reading the documentation once a year would have brought you insane benefits regarding this particular issue. And for ML researchers there is no excuse for stuff like that at this point.
- retinaros 1y agoyes this can also improve the said reasoning.
- sigmoid10 1y agoThe secret the big companies don't want to tell you is that you can turn all their models into reasoning models that way. You even have full control over the reasoning process and can make it adhere to a specific format, e.g. the ones used in legal settings. I've built stuff like that using plain old gpt-4o and it was even better than the o series.
- measurablefunc 1y agoThis is proof of verifiable logic. Computers can not think so calling it proof of thought misrepresents what's actually happening.
- aSanchezStern 1y agoI 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 that isn't useful.
- measurablefunc 1y agoIf 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 definition of "thinking" unless you agree that all functionally equivalent manifestations of arithmetic must be considered "thinking", including cascading dominoes that correspond to the arithmetic operations in an LLM.
- bobxmax 1y ago[flagged]
- measurablefunc 1y agoNot arithmetic or boolean algebra. What's your definition?
- Nevermark 1y ago
- ivanbakel 1y agoThe repo is sparse on the details unless you go digging, which perhaps makes sense if this is just meant as the artifact for the mentioned paper. Unless I’m wrong, this is mainly an API for trying to get an LLM to generate a Z3 program which “logically” represents a real query, including known facts, inference rules, and goals. The “oversight” this introduces is in the ability to literally read the logical statement being evaluated to an answer, and running the solver to see if it holds or not. The natural source of doubt is: who’s going to read a bunch of SMT rules manually and be able to accurately double-check them against real-world understanding? Who double checks the constants? What stops the LLM from accidentally (or deliberately, for achieving the goal) adding facts or rules that are unsound (both logically and from a real-world perspective)? The paper reports a *51%* false positive rate on a logic benchmark! That’s shockingly high, and suggests the LLM is either bad at logical models or keeps creating unsoundnesses. Sadly, the evaluation is a bit thin on the ground about how this stacks up, and what causes it to fall short.
- barthelomew 1y agoYep. The paper was written last year with GPT-4o. Things have become a lot better since then with newer models. E.g. https://arxiv.org/pdf/2505.20047 https://arxiv.org/pdf/2505.20047 Tab 1, we compare the performance on text-only vs SMT-only. o3-mini does pretty well at mirroring its text reasoning in its SMT, vs Gemini Flash 2.0. Illustration of this can be seen in Fig 14, 15 on Page 29. In commercially available products like AWS Automated Reasoning Checks, you build a model from your domain (e.g. from a PDF policy document), cross verify it for correctness, and during answer generation, you only cross check whether your Q/A pairs from the LLM comply with the policy using a solver with guarantees. This means that they can give you a 99%+ soundness guarantee, which basically means that if the service says the Q/A pair is valid or guaranteed w.r.t the policy, it is right more than 99% of the time. https://aws.amazon.com/blogs/aws/minimize-ai-hallucinations-and-deliver-up-to-99-verification-accuracy-with-automated-reasoning-checks-now-available/ https://aws.amazon.com/blogs/aws/minimize-ai-hallucinations-...
- cerved 1y agoWho makes the rules?
- nextos 1y agoThis 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-judge is a promising way ahead, see e.g.: https://arxiv.org/abs/2410.10934 https://arxiv.org/abs/2410.10934
- barthelomew 1y agoYep! I have read your work! Pretty cool! I also worked on a similar deep research agent for autoformalization this summer at AWS ARChecks, building on similar patterns. Although that work is not public, you can play with the generally available product here! [1] https://aws.amazon.com/blogs/aws/minimize-ai-hallucinations-and-deliver-up-to-99-verification-accuracy-with-automated-reasoning-checks-now-available/ https://aws.amazon.com/blogs/aws/minimize-ai-hallucinations-...
- CuriouslyC 1y agoAgent/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.
- jebarker 1y agoWhy 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?
- CuriouslyC 1y agoLLMs 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.
- nakamoto_damacy 1y agoLLMs 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 your theorem prover simply acts as a classifier, ensuring nothing at all.
- barthelomew 1y agoYep, this is a genuine problem, and this is what we term as the autoformalization gap in our follow up paper. (https://arxiv.org/abs/2505.20047 https://arxiv.org/abs/2505.20047) Some LLMs are more consistent between text and SMT, while others are not. (Tab 1, Fig 14,15) You can do uncertainty quantification with selective verification to reduce the "risk", for e.g. shown as the Area Under the Risk Coverage Curve in Tab 4.
- YeGoblynQueenne 1y agoWell, if you understand that this is a "genuine problem" then what have you done to solve it? A quick look at the abstract of your follow up paper does not reveal an answer. And let me be clear that this is a major limitation that fundamentally breaks whatever you are trying to achieve. You start with some LLM-generated text that is, by construction, unrelated to any notion of truth or factuality, and you push it through a verifier. Now you are verifying hot air. It's like research into the efficacy of homeopathic medicine and there's a lot of that indeed, very carefully performed and with great attention to detail. Except all of that research is trying to prove whether doing nothing at all (i.e. homeopathy) has some kind of measurable effect or not. Obviously the answer is not. So what can change that? Only making homeopathy do something instead of nothing. But that's impossible, because homeopathy is, by construction, doing nothing. It's the same thing with LLMs. Unless you find a way to make an LLM that can generate text that is conditioned on some measure of factuality, then you can verify the output all you like, the whole thing will remain meaningless.
- avmich 1y ago
- zwnow 1y agoReasoning? LLMs can not reason, why is it always assumed they reason? They mimic reasoning.
- elcomet 1y agoHow can you know?
- measurablefunc 1y agoBy thinking about what a computer is actually doing & realizing that attributing thought to an arthmetic gadget leads to all sorts of nonsensical consequences like an arrangement of dominoes & their cascade being a thought. The metaphysics of thinking computers is incoherent & if you study computability theory you'll reach the same conclusion.
- elcomet 1y agoI'd say that thoughts and reasoning are two different things, you're moving the goalpost. But what makes the computer hardware fundamentally incompatible with thinking? Compared to a brain
- measurablefunc 1y agoI've already explained it in several places. The burden of proof is on those drawing the equivalence to provide actual evidence for why they believe carbon & silicon are interchangeable & why substrate independence is a valid assumption. I have studied this problem for much longer than many people commenting on this issue & I am telling you that your position is metaphysically incoherent.
- moffkalast 1y agoIt's so funny to me that people are still adamant about this like two years after it's become a completely moot point.
- 1y ago
- dehsge 1y agoLLMs and its output are bounded by Rices theorem. This is not going to ensure correctness it’s just going to validate that the model can produce an undecidable result.
- ogogmad 1y agoErrr, checking correctness of proofs is decidable.
- everdrive 1y agoI'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?
- chpatrick 1y agoEverything happens in an opaque super-high-dimensional numerical space that was "organically grown" not engineered, so we don't really understand what's going on.
- NotGMan 1y agoChat 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.
- everdrive 1y agoWouldn't that mean it's totally impractical for day-to-day usage, but a researcher or team of researchers could solve this?
- 1y ago
- tonerow 1y agoCool 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.
- barthelomew 1y agoHey! Thank you for the interest! I shall do that. Meanwhile, check out Page 11 onwards. We describe a lot of situations! (https://arxiv.org/pdf/2409.17270 https://arxiv.org/pdf/2409.17270)
- pstoll 1y agoUpvoting the comment that the gitrepo would be way more self stand-alone if it had an intro of the DSL.
- sicariomoon 1y ago[dead]
- 0xWTF 1y agoAm I reading this right? Statistical LLM outputs pushed through a formal logic model? Wouldn't that be a case of "crap in, crap out"?
- varispeed 1y agoThat's subjective. One could argue all the things we invented in the past few thousands years were crap. Life would have been much easier in the caves, albeit shorter.
- avmich 1y agoFormal logic serves as a useful filter. In other words, "crap in, filtered crap out" - remember, evolution works with absolutely random, "crap" mutations, which then are "filtered" by the environment.
- baq 1y agoYou assume it’s all crap when it clearly isn’t often enough to be useful.
- tannhaeuser 1y agoLLMs 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. [1]: https://quantumprolog.sgml.net/llm-demo/part1.html https://quantumprolog.sgml.net/llm-demo/part1.html [2]: https://microsoft.github.io/z3guide/docs/fixedpoints/syntax https://microsoft.github.io/z3guide/docs/fixedpoints/syntax
- barthelomew 1y agoYep! Datalog syntax for Z3 is pretty neat! We used SMT [1] in our grammars paper because it allowed the most interoperability with solvers, but our technique also works with PROLOG; as tested our at the behest of reviewers at NeurIPS. I would assume that this should also work with datalog [2]. [1] https://arxiv.org/abs/2505.20047 https://arxiv.org/abs/2505.20047 [2] https://github.com/antlr/grammars-v4/blob/master/datalog/datalog.g4 https://github.com/antlr/grammars-v4/blob/master/datalog/dat...
- larodi 1y agoNeuralsymbolic systems are very likely the future as so many times mentioned here already.
- a3w 1y agoI 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.
- chrchr 1y agoI had a surprising interaction with Gemini 2.5 Pro that this project reminds me of. I was asking the LLM for help using an online CAS system to solve a system of equations, and the CAS system wasn't working as I expected. After a couple back and forths with Gemini about the CAS system, Gemini just gave me the solution. I was surprised because it's the kind of thing I don't expect LLMs to be good at. It said it used Python's sympy symbolic computation package to arrive at the solution. So, yes, the marriage of fuzzy LLMs with more rigorous tools can have powerful effects.
- TrainedMonkey 1y agoJust like humans... we are not so good at hard number crunching, but we can invent computers that are amazing at it. And with a lot of effort we can make a program that uses a whole lot of number crunching to be ok at predicting text but kind of bad at crunching hard numbers. And then that program can predict how to create and use programs which are good at number crunching.
- idiotsecant 1y agoParent post is talking about symbolic manipulation, not rote number crunching, which is exactly what we're supposed to be good at and machines are supposed to be bad at.
- jonplackett 1y agoMaybe the number crunching program the text generation program creates will, with enough effort become good at generating text, an will in turn make another number crunching computer and then…
- Yoric 1y agoThat is exactly the kind of things that I hope LLM will help us achieve before the next AI winter.
- Western0 1y agoI need this same with Mizar https://wiki.mizar.org/ https://wiki.mizar.org/
- sytse 1y agoSo the core idea is to use an LLM to draft reasoning as a structured, JSON domain-specific language (DSL), then deterministically translate that into first-order logic and verify it with a theorem prover (Z3). Interesting that the final answer is provably entailed (or you get a counterexample), instead of being merely persuasive chain-of-thought.
- westurner 1y agoScholarlyArticle: "Proof of thought: Neurosymbolic program synthesis allows robust and interpretable reasoning" (2024) https://arxiv.org/abs/2409.17270 https://arxiv.org/abs/2409.17270 .. https://scholar.google.com/scholar?hl=en&as_sdt=0%2C43&q=%22Proof+of+thought%3A+Neurosymbolic+program+synthesis+allows+robust+and+interpretable+reasoning%22+&btnG= https://scholar.google.com/scholar?hl=en&as_sdt=0%2C43&q=%22...
- nakamoto_damacy 1y agoI posted about my year long development effort of this very method on reddit 25 days ago. My comment elsewhere in this thread provides a cautionary tale, and the authors response to the basic issue I raised is incomplete in that it leaves out that certain problems simply cannot be solved with LLMs (requires logical constraints in the generative process but LLMs lack that layer) So I've pivoted to something else since (also mentioned in my comment elsewhere in this thread) https://www.reddit.com/r/healthIT/comments/1n81e8g/comment/ndapz1r/ https://www.reddit.com/r/healthIT/comments/1n81e8g/comment/n...
- renshijian 1y agoThis is fascinating! An AI that doesn't just think out loud, but keeps a verifiable diary. It's like a philosopher with a cryptographic notary public living in its brain. Amazing work!
- hamonrye 1y agoRHEL knife-edge rolling kernel distribition for the proof of concept.
- derekcheng08 1y agoInteresting. 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.
- maiuki 1y agoWhat industrial problems would this solve?
- deleted 1y ago[deleted]
- jadelcastillo 1y agoInteresting approach, but I guess still lot of work to be done. I tried with this question: "Alice has 60 brothers and she also has 212 sisters. How many sisters does Alice's brother have?" But the generated program is not very useful: { "sorts": [], "functions": [], "constants": {}, "variables": [ {"name": "num_brothers_of_alice", "sort": "IntSort"}, {"name": "num_sisters_of_alice", "sort": "IntSort"}, {"name": "sisters_of_alice_brother", "sort": "IntSort"} ], "knowledge_base": [ "num_brothers_of_alice == 60", "num_sisters_of_alice == 212", "sisters_of_alice_brother == num_sisters_of_alice + 1" ], "rules": [], "verifications": [ { "name": "Alice\'s brother has 213 sisters", "constraint": "sisters_of_alice_brother == 213" } ], "actions": ["verify_conditions"] }