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
51–60 of 182 posts
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#52[1]: https://quantumprolog.sgml.net/llm-demo/part1.html
[2]: https://microsoft.github.io/z3guide/docs/fixedpoints/syntax
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#53Earlier quoted context omitted.
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 th…
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…
Sure, but if you assume that physical reality can be simulated by a Turing machine, then (computational practicality aside) one could do the same thing with a human brain.
Unless you buy into some notion of magical thinking as pertains to human consciousness.
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#54Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#55I 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
#56Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#57I 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 P…
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#58Earlier quoted context omitted.
> What are you talking about? Please edit out swipes like this from your HN comments—this is in the site guidelines: https://news.ycombinator.com/newsguidelines.html . It comes across as aggressive, and we want curious conversation here. Your comment would be fine without that bit.
This is not meant as snide, I'm literally confused if I might have misunderstood the problem here. Because the solution would be so obvious.
Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#59Re: ProofOfThought: LLM-based reasoning using Z3 theorem proving
#60Reasoning? LLMs can not reason, why is it always assumed they reason? They mimic reasoning.