Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks

Large language models (LLMs) show remarkable promise for democratizing automated reasoning by generating formal specifications. However, a fundamental tension exists: LLMs are probabilistic, while formal verification demands deterministic guarantees.