News for hackers. Stuff that matters.

A comment on ProofOfThought: LLM-based reasoning using Z3 theorem proving.

Re:ProofOfThought: LLM-based reasoning using Z3 theorem proving by tannhaeuser on Saturday October 04, 2025 @04:51PM (#45476590)
LLMs 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

[2]: https://microsoft.github.io/z3guide/docs/fixedpoints/syntax

[ Parent | on HN ]
Re:ProofOfThought: LLM-based reasoning using Z3 theorem proving by barthelomew on Saturday October 04, 2025 @05:16PM (#45476784)
Yep! 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 [2] https://github.com/antlr/grammars-v4/blob/master/datalog/dat...

[ Parent | on HN ]
Re:ProofOfThought: LLM-based reasoning using Z3 theorem proving by larodi on Sunday October 05, 2025 @02:55AM (#45479414)
Neuralsymbolic systems are very likely the future as so many times mentioned here already.
[ Parent | on HN ]
Re:ProofOfThought: LLM-based reasoning using Z3 theorem proving by a3w on Sunday October 05, 2025 @12:43PM (#45483044)
I 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.

[ Parent | on HN ]