# Probabilistic Model Checking of Autoregressive Neural Sequence Models

arXiv: https://arxiv.org/abs/2609.00838 · HTML: https://mlsanity.com/paper/2609.00838/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 15 of its 34 references that are in the map.
- First posted on arXiv 1 Sep 2026.

## Builds on (most cited first, 15 of 15)

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [The Curious Case of Neural Text Degeneration](https://mlsanity.com/paper/1904.09751/) (2019)
- [Survey of Hallucination in Natural Language Generation](https://mlsanity.com/paper/2202.03629/) (2022)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [On the Planning Abilities of Large Language Models : A Critical Investigation](https://mlsanity.com/paper/2305.15771/) (2023)
- [DeepXplore: Automated Whitebox Testing of Deep Learning Systems](https://mlsanity.com/paper/1705.06640/) (2017)
- [Conformal Risk Control](https://mlsanity.com/paper/2208.02814/) (2022)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Conformal Language Modeling](https://mlsanity.com/paper/2306.10193/) (2023)
- [DeepGauge: Multi-Granularity Testing Criteria for Deep Learning Systems](https://mlsanity.com/paper/1803.07519/) (2018)
- [Language Models with Conformal Factuality Guarantees](https://mlsanity.com/paper/2402.10978/) (2024)
- [Extracting Automata from Recurrent Neural Networks Using Queries and Counterexamples](https://mlsanity.com/paper/1711.09576/) (2017)
- [Probabilistic Guarantees for Safe Deep Reinforcement Learning](https://mlsanity.com/paper/2005.07073/) (2020)
- [Safety-Oriented Pruning and Interpretation of Reinforcement Learning Policies](https://mlsanity.com/paper/2409.10218/) (2024)
- [Bounded PCTL Model Checking of Large Language Model Outputs](https://mlsanity.com/paper/2509.18836/) (2025)

## Abstract (arXiv)

Test-set accuracy is silent on two issues that matter when deploying autoregressive neural sequence models: how much probability mass the system under test (SUT) places on constraint-violating alternatives that are reachable under sampling and what fraction of the input population satisfies a domain requirement. We answer both with probabilistic model checking. The pipeline extracts a discrete-time Markov chain (DTMC) from the SUT's token-by-token generation, verifies formal PCTL specifications with the PRISM model checker, and aggregates the per-input verdicts into a coverage curve over the input space. A soundness theorem establishes the DTMC as an under-approximation, so every verdict yields a certified interval on the SUT's true reachability probability. The coverage built from those verdicts is, therefore, conservative by construction. A counterexample-guided abstraction refinement (CEGAR) loop adaptively tightens the interval, and a maximum-likelihood algorithm extracts the most probable falsifying trace. Two case studies exercise the pipeline. On a GPT-2 computer-aided process-planning (CAPP) model with 100% test accuracy, the pipeline quantifies the probability mass greedy decoding hides, but that is reachable with sampling; and identifies the smallest training fraction at which an ordering requirement holds population-wide, neither of which test accuracy can report. We then verify the SMILES molecular generator with a 50x larger vocabulary. The only change is an external chemical-validity oracle, and the pipeline identifies the gap between structural completeness and chemical validity.