PaperlayerView exact revision on arXiv

Source-linked AI summary

Probabilistic Model Checking of Autoregressive Neural Sequence Models

Helge Spieker, Dennis Gross, Arnaud Gotlieb

arXiv:2609.00838v1cs.SEcs.AI

TL;DR

Test-set accuracy leaves uncertainty about sampled constraint violations and population-wide domain compliance. The paper addresses both with DTMC extraction, PCTL verification, certified conservative coverage, refinement, and counterexample analysis, then evaluates CAPP and SMILES generators across substantially different settings.

  • Problem

    Test-set accuracy does not report probability mass on sampled alternatives, domain constraints absent from references, or the fraction of inputs satisfying a requirement.

  • Method

    The pipeline extracts a DTMC from token generation, verifies PCTL specifications with PRISM, aggregates per-input verdicts into coverage, and refines abstractions with CEGAR.

  • Results

    The pipeline exposes hidden sampled probability mass and population-level ordering behavior in CAPP, and identifies structural-versus-chemical validity gaps in SMILES generation.

  • Takeaways & Limitations

    Certified coverage and best-of-N analysis inform decoder choice and training-data budgets during development and model selection.

  • Takeaways & Limitations

    SMILES coverage is not a population guarantee because its 200 prompts are not a random deployment sample, and the methodology has not exercised long-horizon generation, non-GPT architectures, or diverse samplers.

Abstract

from arXiv · show

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.

1 Introduction

Test-set accuracy cannot reveal sampled probability mass on constraint-violating alternatives or the population-wide prevalence of domain compliance. The paper addresses these gaps with probabilistic model checking, certified coverage, refinement, and counterexample extraction.

  • 1 Introduction: Deployment evaluation needs probability-mass, domain-constraint, and population-coverage evidence beyond reference-matching accuracy.These questions concern alternatives sampling may reach, constraints absent from the ground-truth signal, and the fraction of inputs satisfying a criterion.
  • 1 Introduction: 9% of probability mass remains on completions hidden by greedy decoding for the smallest 15%-training CAPP checkpoint with 100% test accuracy.On data-starved checkpoints, the most probable hidden trace can also violate manufacturing phase ordering.
  • 1 Introduction: Sampling exposes distributional behavior that greedy decoding omits, while verifier filtering can recover correct plans greedy decoding misses.The pipeline predicts this recovery frequency without rerunning the model; a slightly sharpened sampler does so on the most data-starved checkpoint.
  • 1 Introduction: The pipeline extracts a DTMC from token generation, verifies PCTL specifications with PRISM, and aggregates per-input verdicts into a population coverage curve.The approach also uses certified probability intervals, adaptive CEGAR refinement, and maximum-likelihood falsifying traces.
  • 1 Introduction: The methodology comprises a DTMC abstraction, domain-specific PCTL specifications, population coverage, a soundness theorem, CEGAR refinement, and counterexample extraction.Experiments apply it to CAPP and SMILES molecule generation.

2 Related Work

Related work verifies neural systems through probabilistic, statistical, deterministic, population-level, and coverage-guided techniques. This pipeline targets autoregressive generation distributions and adds sound population aggregation with domain-specific specifications.

  • 2 Related Work: Prior probabilistic model checking abstracts neural controllers or policies, whereas this work models autoregressive generation as a DTMC and aggregates over inputs.The comparison distinguishes generation stochasticity from environment stochasticity represented by MDPs.
  • 2 Related Work: Unlike simulation-based verification, the pipeline computes exact per-input reachability with PRISM and uses aggregation only to combine those verdicts across the population.DTMC extraction is also characterized as symbolic execution, threshold pruning as abstract interpretation, and refinement as CEGAR.
  • 2 Related Work: Compared with model-agnostic population claims and activation-space coverage, the method accesses token probabilities and supports domain-specific PCTL specifications with soundness guarantees.The related-work comparison gives phase ordering as an example of a domain-specific property.
  • 2 Related Work: The pipeline overview connects per-input DTMC verification, population coverage aggregation, CEGAR re-expansion, and on-demand counterexample extraction.These components are presented as a single verification workflow.

3 Verification Pipeline

The verification pipeline converts token probabilities into a pruned DTMC, checks PCTL properties, and aggregates certified per-input probabilities into conservative coverage curves. Soundness bounds account for diverted mass, while CEGAR tightens intervals.

  • 3 Verification Pipeline: Token-prefix states and conditional transitions form an acyclic DTMC, enabling reachability probabilities through backward induction.The autoregressive sequence distribution is factorized left to right, with temperature scaling defining the stepwise categorical distributions.
  • 3 Verification Pipeline: Three independently operable stages perform DTMC abstraction, PRISM specification verification, and population coverage aggregation.A CEGAR loop and counterexample extractor operate alongside these stages.
  • 3 Verification Pipeline: Threshold pruning routes omitted transition mass to low_prob, low-probability paths to low_prob, and depth-limited unfinished paths to truncated.A hard depth limit guarantees termination.
  • 3 Verification Pipeline: The extractor additionally sends structurally invalid prefixes to an absorbing invalid state and annotates near-ties using a top-1/top-2 probability-gap criterion.The default critical-state threshold is g(s) < 10%, with τ = 0.5%, ρ = 10^-4, and dmax = 20.
  • 3 Verification Pipeline: Coverage is the fraction of inputs whose verified property probability reaches threshold θ, producing a curve that underestimates true coverage.The reported population statement can be compared with an application-specific deployment level c.
  • 3 Verification Pipeline: The soundness theorem bounds true reachability between explicit success probability and that probability plus diverted low_prob and truncated mass.Prefix-closed structural invalidity removes invalid mass from the tightened upper bound.
  • 3 Verification Pipeline: Every explicit path preserves its model probability, while diverted mass creates the abstraction interval and sink masses sum to one.The four sinks are success, low_prob, invalid, and truncated.
  • 3 Verification Pipeline: For violation properties, a nonzero verdict proves that a violation exists, but a zero verdict does not certify its absence.The conservative direction applies directly to properties holding at success terminals.

4 Evaluation

The evaluation tests specification informativeness, population coverage, counterexamples, refinement, and portability across CAPP and SMILES settings. CAPP provides an enumerable input space and a 53-token GPT-2 model whose accuracy reaches 100% from 15% training onward.

  • 4 Evaluation: The evaluation asks whether the pipeline exposes failures missed by accuracy, supports population deployment guarantees, yields counterexamples, tightens intervals, and transfers across vocabularies and oracles.Case study 1 addresses RQ1–3, while case study 2 focuses on portability and revisits RQ1.
  • 4.1 Case Study 1: CAPP: 7,840 enumerable CAPP parts map six discrete features to ordered manufacturing-operation sequences using a 53-token, four-layer GPT-2 model.The released checkpoints span 1% to 70% training fractions, reaching 100% held-out sequence accuracy from 15% onward.
  • 4.1 Case Study 1: CAPP: The CAPP phase-ordering requirement enforces Primary →Secondary*→Finishing* with exactly one Primary operation and no backward transition.This domain constraint is external to the neural model and its training signal.
  • 4.1 Case Study 1: CAPP: 37,554 per-input DTMCs and 262,878 checking runs covered eight training fractions with zero solver failures.Seven of eight specifications were verified with PRISM for every test sample.
  • 4.1 Case Study 1: CAPP: Training configurations are evaluated jointly through accuracy and DTMC structural statistics.The table organizes the CAPP comparison by training configuration.

RQ1: Failure Modes Invisible to Accuracy

Verification reveals failure modes that test accuracy misses: probability mass can remain on valid alternatives, while structural validity may still be preserved. DTMC diagnostics further show how training data changes distributional concentration and decision-boundary proximity.

  • From 15% training onward, test-set sequence accuracy is 100%, while mean P(success) ranges from 0.907 to 0.974.For the 70% model, Theorem 1 certifies true reachability in [0.974, 1.000].
  • P(invalid) = 0 in every configuration except 1% training, where it is 0.009.The verified structural property indicates syntactic well-formedness is preserved even under severe data starvation.
  • P(success) rises from 0.949 at 30% training to 0.974 at 70%, then changes little across thresholds until τ = 0.01%.At τ = 0.01%, P(success) reaches 0.981 and low_prob falls from 2.5% to 1.9%.
  • A residual ≈1.9% remains at τ = 10^-4 and ρ = 10^-6 because probability is dispersed across valid alternatives below the threshold.This dispersion is strongest with scarce data: canonical-target concentration is 36% at 1% training, 79% at 5%, and above 99.5% from 10% onward.
  • DTMC structure changes from 934 mean states and 100% multi-branch inputs at 1% training to 18 states and 0% multi-branch inputs at 70%.Inputs with at least one critical state fall from 97.9% at 1% training to none observed from 15% onward.

RQ2: Population Coverage and Operating Envelope

The pipeline converts per-input ordering probabilities into conservative population coverage and decoder operating-envelope claims. It also provides certifiable sampling, inspectable counterexamples, and adaptive interval refinement.

  • Per-input ordering: From 10% training onward, PD(misordered) = 0 across the test set, although pruned sub-threshold mass remains uncertified.At 1% training, only 0.3% of retained probability mass is misordered.
  • Population coverage: Coverage rises from ˆµ = 0.252 at 10% training to ˆµ = 0.971 at 30%, the smallest fraction covering the population at c = 0.90.From 50% training onward, every test input meets the threshold with ˆµ = 1.000.
  • Operating envelope: Coverage stays at ˆµ ≥0.97 for T ≤1.0 in the 30% and 70% models but drops sharply at T = 1.3.The 1% model never reaches ˆµ = 0.90, even at T = 0.5, where coverage is 0.789.
  • Best-of-N decoding: At T = 0.5, best-of-10 achieves pass@10(ordered) = 1.00 for every input and surfaces 1.87 distinct valid plans per input versus greedy’s one.The ordered result is deployable because ordering validity is checkable at runtime; correct performance is an oracle upper bound.
  • Counterexamples: The maximum-likelihood counterexample has joint probability 3.5×10^-3 and emits a Finishing operation before any Primary operation.Greedy decoding never selects this violating trace, but the algorithm produces it as an inspectable artifact.
  • Adaptive refinement: Five CEGAR rounds contract dispersion, with 30%-model samples improving by 25–35%, while 1% medians improve by only a few percent.In data-starved settings, irreducible sub-threshold dispersion limits what bounded top-K refinement can reclaim.

4.2 Case Study 2: SMILES Molecular Generation

The second case study applies the unchanged pipeline to SMILES generation using a much larger vocabulary and an external chemical-validity oracle. It tests whether structural completion and semantic validity can be separated.

  • Purpose: The case study stresses the methodology with larger DTMCs and semantic constraints rather than only grammar-level validity.Its motivation is to test portability beyond the favorable, small-vocabulary CAPP setting.
  • Setup: SMILES generation uses approximately 2,700 BPE tokens, roughly 50× the CAPP vocabulary, with one DTMC built per prompt.The evaluated inputs are 200 short SMILES prefixes drawn from the ZINC alphabet.

System Under Test

The SMILES system produces substantially larger DTMCs than CAPP, yet the pipeline completes all verification instances. Extraction, rather than PRISM solving, dominates runtime, and depth truncation widens the certified interval.

  • Scale: SMILES DTMCs average 13,150 states and reach 37,397 states, compared with 53 tokens and 16-state DTMCs for CAPP.The mean SMILES extraction time is 485 s and PRISM verification time is 43 s per prompt.
  • Verification: All 200 PRISM instances completed without solver failure, matching CAPP’s 0% error rate.Extraction dominates runtime, with mean 485 s versus 43 s for verification.
  • Portability: The pipeline is vocabulary-agnostic: no component assumes a fixed token set or small state space, and the soundness theorem and CEGAR loop carry over unchanged.This supports portability from CAPP to the much larger SMILES vocabulary.
  • Limitation: Mean PD(truncated) = 0.018 across 200 SMILES inputs, widening the certified soundness interval.The truncated term, rather than diffuse low_prob dispersion, is the main scale-related gap and is most reducible through CEGAR or a larger dmax.

RQ4+RQ1: Specification Informativeness

The SMILES case study reveals a structural-versus-semantic validity gap that exact-match accuracy and structural completion do not capture. An external chemical-validity oracle integrates without changing the pipeline and makes this discrepancy measurable.

  • Mean P(valid_smiles) = 0.084 versus mean P(success) = 0.248 among prompts producing at least one chemically valid terminal.Conditional on structural completion, roughly 66% of probability mass corresponds to invalid molecules.
  • 181 of 200 prompts produce at least one chemically invalid but structurally complete terminal, including 94 with only invalid structurally complete terminals.A further 16 prompts produce no structurally complete terminal, while 110 produce no chemically valid SMILES.
  • The gap between P(success) and P(valid_smiles) formally measures the discrepancy between structural completion and chemical validity.In contrast, CAPP has P(invalid) ≈0 from 5% training onwards because its token grammar encodes well-formedness.
  • RDKit’s MolFromSmiles serves as an external pass/fail oracle for semantic constraints absent from the SMILES grammar.Integrating this oracle required no change to extraction, PRISM export, or coverage aggregation.

5 Threats to Validity

The validity analysis is bounded by specification, sampling, and generality assumptions. CAPP’s ordering property omits richer manufacturing constraints, SMILES coverage lacks a population guarantee, and the two studies support portability rather than broad generality.

  • The critical-state gap threshold is diagnostic only and does not enter the soundness theorem.Critical-state rankings were qualitatively stable for thresholds of 5%, 10%, and 20% in the tested non-trivial configuration.
  • The CAPP ordering specification omits resource contention, tool-change costs, and batch-dependent process choice.
  • SMILES coverage is not a population coverage guarantee because its 200 prompts are not a random sample of a deployment distribution.The study therefore reports raw P(success) and P(valid_smiles) without a population layer.
  • The CAPP and SMILES studies support portability across 53 versus ≈2,700-token vocabularies and different specification types, not generality across all autoregressive transformers.The studies have DTMC sizes differing by 800× and use no source-code change between systems.
  • The evaluation has not exercised long-horizon generation (d ≫20), non-GPT architectures, or diverse sampling schemes.

6 Conclusion

The paper presents probabilistic model checking as a way to quantify autoregressive models’ off-trajectory probability mass and domain-constraint gaps beyond test-set accuracy. Its conclusion frames deployment evaluation around whether the gap between confident outputs and domain specifications is acceptable.

  • The pipeline combines a DTMC abstraction, a soundness theorem, exact PCTL verification, and population coverage over the input space.
  • Test-set accuracy scores one greedy trajectory against a reference but is silent on probability mass elsewhere and domain constraints absent from the reference.
  • The deployment question becomes whether the gap between a model’s confident output and a domain specification is acceptable.
Loading 2609.00838v1…