Probabilistic Model Checking of Autoregressive Neural Sequence Models

• URL: http://arxiv.org/abs/2609.00838v1
• Date: Tue, 01 Sep 2026 07:37:55 GMT
• Title: Probabilistic Model Checking of Autoregressive Neural Sequence Models
• Abstract summary: Test-set accuracy is silent on two issues that matter when deploying autoregressive neural sequence models.<n>How much probability mass the system under test places on constraint-violating alternatives that are reachable under sampling.<n>We answer both with probabilistic model checking.
• Score: 4.570003973862485
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• EDGE: a closed-form directed test for the calibration of probabilistic binary classifiers [0.0]
  We propose EDGE, a calibration test for the canonical probabilistic classifier, logistic regression.<n> EDGE reads the same binned predicted-observed table a reliability diagram plots, and projects its standardized bin residuals onto a small pre-specified basis of smooth calibration-distortion.<n>Across link and feature misspecification the pre-specified default led or tied every rival binned test on the fitted index in 19 of 22 detectable scenarios, and stayed computable where the refit-based Stukel score test separates in 20% to 28% of samples.
  arXiv  Detail & Related papers  (2026-08-20T19:06:05Z)
• Auditing Question-Order Effects in Large Language Models with the QQ Equality: Mechanism Characterization and a Saturation Caveat [4.07636450847048]
  Human survey respondents exhibit question-order effects that satisfy the QQ (quantum question) equality.<n>We develop the QQ equality into an audit criterion for sequential judgments of autoregressive large language models.
  arXiv  Detail & Related papers  (2026-07-19T12:22:06Z)
• When RLVR Shrinks the Reasoning Boundary: Diagnosing Pass@k Inversion [0.0]
  Reinforcement learning with verifiable rewards (RLVR) can improve one-sample accuracy while making a model worse under repeated sampling.<n>We study this pass@k inversion: after training, the policy may solve fewer distinct problems than its base model at large $k$.<n>The failure concentrates on boundary prompts, where the base model contains rare correct trajectories that are recoverable by sampling but too sparse to reliably appear in finite RLVR rollout groups.
  arXiv  Detail & Related papers  (2026-07-12T17:17:18Z)
• Federated Language Models Under Bandwidth Budgets: Distillation Rates and Conformal Coverage [12.805268849262243]
  Training a language model on data scattered across bandwidth-limited nodes that cannot be centralized is a setting that arises in clinical networks, enterprise knowledge bases, and scientific consortia.<n>We study the regime in which data must remain distributed across nodes, and ask what statistical guarantees are in principle achievable under explicit bandwidth budgets.
  arXiv  Detail & Related papers  (2026-05-11T05:01:43Z)
• Correction and Corruption: A Two-Rate View of Error Flow in LLM Protocols [51.56484100374058]
  We propose a paired-outcome measurement interface for auditing a single protocol step on exact-match tasks.<n>For each instance, the interface records a baseline correctness bit and a post-step correctness bit.<n>These rates predict accuracy changes and define a reusable empirical interface testable across seeds, mixtures, and pipelines.
  arXiv  Detail & Related papers  (2026-04-20T13:25:40Z)
• Towards Verifiable AI with Lightweight Cryptographic Proofs of Inference [3.3323431541048385]
  We present a verification framework and protocol that replaces full proofs with a lightweight, sampling-based approach.<n>We formalize the conditions under which trace separation between functionally dissimilar models can be leveraged to argue the security of verifiable inference protocols.<n>Our approach reduces proving times by several orders of magnitude compared to state-of-the-art cryptographic proof systems.
  arXiv  Detail & Related papers  (2026-03-19T15:24:27Z)
• Large Language Models Are Bad Dice Players: LLMs Struggle to Generate Random Numbers from Statistical Distributions [50.1404916337174]
  We present the first large-scale, statistically powered audit of native probabilistic sampling in large language models (LLMs)<n>We show that batch generation achieves only modest statistical validity, with a 13% median pass rate, while independent requests collapse almost entirely.<n>We conclude that current LLMs lack a functional internal sampler, necessitating the use of external tools for applications requiring statistical guarantees.
  arXiv  Detail & Related papers  (2026-01-08T22:33:12Z)
• Controllable Generation via Locally Constrained Resampling [77.48624621592523]
  We propose a tractable probabilistic approach that performs Bayesian conditioning to draw samples subject to a constraint. Our approach considers the entire sequence, leading to a more globally optimal constrained generation than current greedy methods. We show that our approach is able to steer the model's outputs away from toxic generations, outperforming similar approaches to detoxification.
  arXiv  Detail & Related papers  (2024-10-17T00:49:53Z)
• Semi-DETR: Semi-Supervised Object Detection with Detection Transformers [105.45018934087076]
  We analyze the DETR-based framework on semi-supervised object detection (SSOD) We present Semi-DETR, the first transformer-based end-to-end semi-supervised object detector. Our method outperforms all state-of-the-art methods by clear margins.
  arXiv  Detail & Related papers  (2023-07-16T16:32:14Z)
• Complex Event Forecasting with Prediction Suffix Trees: Extended Technical Report [70.7321040534471]
  Complex Event Recognition (CER) systems have become popular in the past two decades due to their ability to "instantly" detect patterns on real-time streams of events. There is a lack of methods for forecasting when a pattern might occur before such an occurrence is actually detected by a CER engine. We present a formal framework that attempts to address the issue of Complex Event Forecasting.
  arXiv  Detail & Related papers  (2021-09-01T09:52:31Z)
• Breaking the Sample Size Barrier in Model-Based Reinforcement Learning with a Generative Model [50.38446482252857]
  This paper is concerned with the sample efficiency of reinforcement learning, assuming access to a generative model (or simulator) We first consider $gamma$-discounted infinite-horizon Markov decision processes (MDPs) with state space $mathcalS$ and action space $mathcalA$. We prove that a plain model-based planning algorithm suffices to achieve minimax-optimal sample complexity given any target accuracy level.
  arXiv  Detail & Related papers  (2020-05-26T17:53:18Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.