[sytse]

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