We present \tool, a query-efficient framework for black-box probabilistic verification. Given a fixed, sampleable input distribution and a binary property oracle, \tool assesses the property's violation probability p against a threshold θ. Under independent sampling and stateless oracle behavior, acceptance asserts p≤θ, rejection asserts p>θ+η for a user-specified separation margin, and an inconclusive verdict indicates insufficient evidence for either conclusion. The probability of each type of erroneous verdict is bounded by its specified error budget. To support this three-valued contract efficiently, \tool uses a single sequential test, eliminating the interval family required by the baseline. The test accounts for repeated sampling checks through either corrected exact binomial confidence intervals or an anytime-valid confidence sequence. We apply \tool to probabilistic local model semantic consistency, where the property oracle detects decision-level inconsistencies between reference and compiled executions under a specified perturbation distribution. Our evaluation covers 24 tasks across TorchInductor and TensorRT and examines sampling efficiency, conclusiveness, and diagnostic behavior. For sampling efficiency, we use paired one-model clean-label radius searches: the baseline requires 3.6-4.2 times as many unique samples under matched numerical parameters while providing a weaker decision contract. For model semantic consistency, checks at θ=10−3 yield 817 acceptances, 19 inconclusive verdicts, and 4 rejections across 840 input--backend instances from 21 tasks. Case studies of two documented compiler faults further demonstrate what these local verdicts can diagnose.
Figures & tables
Figure 1: Overview of the workflow of DL compilers.
Symbol
Meaning
M,C
Reference and compiled executions; their outputs denote predicted labels.
D
Fixed, sampleable input distribution.
ψ(x)
Shorthand for the supplied binary oracle ψ(x,C,M) .
Yj,p
Observation Yj=ψ(xj) and unknown probability p=Pr(Yj=1) .
θ,η
Acceptance threshold and separation margin; rejection asserts p>θ+η .
δ
Direction-specific error budget for one verification instance.
Table 1: Notation of ProCerDCL .
Figure 2: Per-input agreement with the flipping budget found by the attack’s heuristic search (a), and the reference-model control (b). Each point is one input; the red dashed line is the least-squares fit.
Model
Dataset
inductor
tensorrt
PROVERO
ProCerDCL
PROVERO
ProCerDCL
LeNet-5
MNIST
408.6
141.5 (2.89 × )
371.3
126.3 (2.94 × )
ResNet-18
CIFAR-10
336.5
111.4 (3.02 × )
354.0
117.2 (3.02 × )
CIFAR-100
317.8
105.0 (3.03 × )
324.5
110.4 (2.94 × )
SVHN
431.2
152.3 (2.83 × )
484.4
167.3 (2.89 × )
ImageNet-1k
572.2
205.0 (2.79 × )
563.3
203.8 (2.76 × )
Table 4: Mean unique samples per input ( ×103 ) to reach a verdict, per task and backend, averaged over every search, whatever it concluded. Each backend gives PROVERO first, then ProCerDCL with its speedup over PROVERO in parentheses.
Table 5
Same verdict
Mean draws
Draws over seeds
Median ϵHard
Per-input ϵHard spread
Within one step
Per-input draw CV
20/20
141.8k (CV 2.3%)
136.1k–147.2k
6.28–6.65
median 0.30, max 1.40
8/20
median 9.2%, max 21.7%
Table 7: Stability across ten random seeds on LeNet-5/MNIST under TensorRT.
Figure 3: Certified hardness of quantized models against the attack’s heuristic flipping budget.
Figure 4: One-model local robustness under hardware and perturbation changes.
varied
value
concl.
radius
draws
default
—
100%
6.05
109,061
θ
0.5%
100%
5.80
199,371
θ
2%
100%
6.40
57,582
θ
5%
100%
7.40
25,978
1−δ
99.9%
100%
6.05
148,694
1−δ
95%
100%
6.05
85,034
Table 8: Parameter sensitivity of one-model clean-label radius searches on ResNet-18/CIFAR-10 under Inductor.
TorchInductor
TensorRT
Conclusive
100/100
99/100
Pearson
0.60
0.79
Spearman
0.80
0.89
Median ϵHard
14.3
16.8
Table 9: Certificates under the patch distribution on LeNet-5/MNIST.
Modern deep learning compilers compile models lazily and cache artifacts across invocations. Retained compiler state can make a later invocation incorrect even when it is correct in isolation. An analysis of 26 publicly reported issues in PyTorch, JAX, and TensorFlow shows that detecting such bugs requires sequences that first establish compiler state and then expose a failure. We present Rondo, a stateful testing method that represents each test case as a model paired with an invocation sequence. Rondo mutates invocation sequences and uses a Markov chain Monte Carlo sampler guided by compilation behavior to favor rarely observed behaviors. Its three-way differential oracle compares execution without compilation, compiled execution with compiler state reset, and compiled execution with state retained. It confirms stateful bugs by replaying the same invocation with state retained and reset while preserving inputs and program state, then shortens sequences while preserving the original bug. We evaluate Rondo on four deep learning frameworks using 24 common model architectures. Rondo detects 117 bugs, including 35 stateful bugs. We submit 39 bug reports, including 18 for stateful bugs; developers confirm 35 reports, including 16 for stateful bugs, and fix 18 bugs, including 11 stateful bugs. Rondo achieves the highest behavior coverage and compiler Python source-line coverage among the compared methods, with 99.26% alarm precision. It shortens 44 of 117 invocation sequences, reducing the lengths of these 44 sequences by 83.34% on average.
Jiatao Ge, Ruixiang Qian, Yibo Hu +5
State Key Laboratory for Novel Software Technology, Nanjing University, China · UNIST, Republic of Korea
Concurrency, parallelism and distributed execution become truly fearless when the compiler tracks wait-for edges, proves multi-threaded work is sound and preserves distributed boundary contracts. In this design, our Composer compiler preserves proofs while lowering Clef directly to native CPU, GPU, NPU and FPGA code, without translation through C or vendor APIs. Our Program Semantic Graph retains the values, relationships and premises that justify BAREWire's unboxed boundary contracts. And C & C++ interfacing is an explicit marshaling boundary, with proofs tied to actual arguments, conversions and returned values. Four verification tiers connect an account of our design. Tier 1 supplies structural inference, founded on principal dimensional types. Tier 2 generates and checks local arithmetic, representation, and computational integrity at the node level. Tier 3 instantiates reusable domain and system lemmas, including distributed proofs supported by Iris, Actris and Aneris. Tiers 1-3 require no developer annotations, with a quotation based lemma library design to extend coverage as use cases expand. Tier 4 admits computational and probabilistic relational proofs, with project annotations identifying the required relations. We extend the same library direction toward recognizing relational constructions from hypergraph structure. A formal composition rule connects arithmetic, ownership, protocol and realization evidence. Our worked distributed reduction preserves one specified result across concurrent workers, reordered arrivals and boundary mappings. Its probabilistic extension carries worker and conversion error with an explicit failure budget. With recent work by Urschel, we show bounds supply a relevant source of reusable proof terms. These constructions make verification a core engineering discipline for truly fearless programs and systems across a variety of hardware targets.
Tensor programs, as used in deep learning models, are a prime target for optimization, as small performance improvements can have a large impact across training or inference workloads. However, such optimizations are complicated and can produce subtle bugs. Traditionally, correctness is assumed when differential testing against a reference on random inputs fails to reveal bugs. However, the inputs to these programs are massive tensors, and finding bugs can require generating extremely low likelihood inputs with precise relationships among their values. We propose a novel way to find bugs more consistently by flipping the quantifiers. Rather than generating a single input and checking all output tensor locations for equivalence, what if you could check a single output tensor location's equivalence for all inputs? We implement this idea in a system, \dirigo, by using a novel symbolic execution strategy. We demonstrate that \dirigo can find bugs effectively in a public dataset of 6,988 AI-written CUDA kernels that are all marked correct by differential testing. Of these, \dirigo finds 600 kernels that are actually buggy, and finds 97.3% of those bugs within two minutes.