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

11–20 of 182 posts

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

#11

Post by barthelomew »

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…

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

If you ever feel like chatting and discussing more details, happy to chat!

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

#12

Post by viraptor »

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…

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

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

#13

Post by jssmith »

sigmoid10 wrote: post #3

I 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 sche…

I see JSON parse errors on occasion when using OpeanAI structured outputs that resolve upon retry. It seems it’s giving instructions to the LLM but validation is still up to the caller. Wondering if others see this too.

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

#14

Post by barthelomew »

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…

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

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

#15

Post by aSanchezStern »

measurablefunc wrote: post #5

This is proof of verifiable logic. Computers can not think so calling it proof of thought misrepresents what's actually happening.

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 that isn't useful.

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

#16

Post by CuriouslyC »

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.

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

#17

Post by nakamoto_damacy »

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

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

#18

Post by barthelomew »

sigmoid10 wrote: post #3

I 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 sche…

Hey there! I mostly designed and wrote most of the actual interpreter during my internship at Microsoft Research last summer. Constrained decoding for GPT-4 wasn’t available when we started designing the DSL, and besides, creating a regex to constrain this specific DSL is quite challenging.

When the grammar of the language is better defined, like SMT (https://arxiv.org/abs/2505.20047) - we are able to do this with open source LLMs.

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

#20

Post by barthelomew »

jssmith wrote: post #13
sigmoid10 wrote: post #3

I 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 sche…

I see JSON parse errors on occasion when using OpeanAI structured outputs that resolve upon retry. It seems it’s giving instructions to the LLM but validation is still up to the caller. Wondering if others see this too.

Hey, yes! This is because the DSL (Domain Specific Language) is pretty complex, and the LLM finds it hard. We prototype a much more effective version using SMT in our NeurIPS 2025 paper (https://arxiv.org/abs/2505.20047). We shall soon open source that code!
Post reply on HN