PaperlayerView exact revision on arXiv

Source-linked AI summary

ProCerDCL: Query-Efficient Black-Box Probabilistic Verification of Deep Learning Compiler Optimization

Zexin Li, Weibo Zhang, Linyi Li, Arvind Easwaran, Simin Chen

arXiv:2610.36499v1cs.SEcs.AIcs.PL

TL;DR

Differential testing can reveal individual inconsistencies but does not establish how frequently they occur under a specified perturbation distribution. ProCerDCL uses one sequential test to verify a three-valued probability contract, and its evaluation reports fewer draws than the baseline alongside local consistency verdicts across compiler backends.

  • Problem

    Differential testing finds inconsistencies on tested inputs, but consistency on those cases alone does not establish the violation frequency on unseen inputs under a specified distribution.

    Source: §1 · p. 2

  • Method

    ProCerDCL tests a binary violation oracle sequentially against a threshold, using a single test and bounds that preserve error control across repeated checks.

    Source: §3.2 · p. 6, §7 · p. 24

  • Results

    3.6–4.2 times as many unique draws are required by the baseline at matched parameters, while θ = 10^-3 checks yield 817 acceptances, 19 inconclusive verdicts, and 4 rejections across 840 input–backend instances from 21 tasks.

    Source: §1 · p. 3

  • Takeaways & Limitations

    The two documented compiler-fault case studies show that local verdicts can distinguish affected builds from patched or workaround builds.

    Source: §7 · p. 24

    The guarantees hold for one fixed distribution, and simultaneous claims over multiple seeds or configurations require further error-budget allocation.

    Source: §5 · p. 23

Abstract

from arXiv · show

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 $\theta$. Under independent sampling and stateless oracle behavior, acceptance asserts $p\le\theta$, rejection asserts $p>\theta+\eta$ 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 $\theta=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.

1 Introduction

Compilation can change finite-precision predictions, so developers need to assess how often reference and compiled models disagree under a specified distribution. ProCerDCL uses one sequential test for a three-valued probabilistic contract and evaluates its efficiency and local diagnostic scope.

1 Introduction

  • Decision-level inconsistencies can undermine transfer of developers’ evaluated reference-model behavior to the compiled model.Checking consistency helps assess whether compilation preserves the predictive behavior intended for deployment.Source: §1 · p. 2
  • Differential testing can find inconsistencies on tested inputs, but consistency on those cases alone does not establish violation frequency on unseen inputs.A probabilistic specification defines an input distribution and acceptable violation probability for local regression checks or build comparisons.Source: §1 · p. 2
  • With a 1% true violation probability, 100 independent draws contain no violations with probability about 37%, so no observed failures may still be insufficient evidence.A probabilistic verifier connects observations to an explicit erroneous-verdict risk bound and can return an inconclusive result.Source: §1 · p. 2
  • ProCerDCL accepts when an upper confidence bound establishes p ≤ θ, rejects when a lower bound establishes p > θ + η, and otherwise returns NONE before its finite cap.Under independent sampling and stateless oracle behavior, direction-specific erroneous-decision probabilities are bounded; either decisive verdict in (θ, θ + η] is an error.Source: §1 · p. 2
  • A single sequential test replaces the baseline’s adaptive interval family, while the evaluation distinguishes one-model robustness from paired semantic consistency.The framework’s local verdicts concern the chosen distribution and oracle: acceptance does not establish agreement on every input, and rejection does not prove a compiler bug.Source: §1 · pp. 2–3
  • 3.6–4.2 times as many unique draws are required by the baseline in paired one-model clean-label radius searches at matched numerical parameters, under a weaker decision contract.Across 840 input–backend instances from 21 tasks, checks at θ = 10^-3 yield 817 acceptances, 19 inconclusive verdicts, and 4 rejections.Source: §1 · p. 3

2 Background

DL compilers lower models through intermediate representations and apply transformations to produce hardware-efficient kernels. Since floating-point operations are not associative, these transformations can change predictions, motivating statistical verification of violation probabilities.

2 Background

  • A DL compiler maps a framework model to a high-level intermediate representation, applies platform-independent transformations, then lowers and optimizes it for hardware before emitting machine code.Examples include operator fusion in the frontend and vectorization or loop unrolling in the backend.Source: §2 · pp. 3–4
  • Floating-point reordering or regrouping can change rounding, so a compiled model can diverge at runtime from its mathematically equivalent source model.Such differences are called optimization inconsistency in the cited background discussion.Source: §2 · p. 4
  • Threshold verification assesses whether a violation probability meets a bound rather than estimating that probability to a prescribed accuracy.Ordinary fixed-sample intervals do not automatically retain nominal coverage under repeated, data-dependent checks; checkpoint corrections or anytime-valid confidence sequences address this issue.Source: §2 · p. 4

3.1 Problem Formulation

The formulation measures the probability of a binary semantic-consistency violation under a fixed, sampleable input distribution. Its three-valued verdict applies only to that distribution, oracle, and execution configuration.

3.1 Problem Formulation

  • The semantic-consistency oracle compares reference and compiled predictions on the same input and reports a violation when they differ.The target probability is the chance that compilation changes the reference model’s prediction under D.Source: §3.1 · p. 4
  • The local instantiation samples around a seed input; each radius defines a separate distribution, and a radius search reports the largest tested radius certified YES.The perturbation neighborhood is an ℓq ball restricted to the admissible input domain; other distributions are supported if their sampler produces independent draws.Source: §3.1 · p. 5
  • A verdict is specific to the chosen distribution and oracle and does not establish consistency for every input or global compiler correctness.The local perturbation distribution need not represent deployment traffic.Source: §3.1 · p. 5
  • The verifier consumes a binary stream of independent Bernoulli(p) observations when sampling is independent and the oracle is fixed and stateless.The run fixes the distribution, models, and execution configurations; cost counts sampled oracle observations, including repeated input values.Source: §3.1 · p. 5
  • Acceptance asserts p ≤ θ and rejection asserts p > θ + η, each with its direction-specific error budget; NONE means neither assertion has enough support.Within (θ, θ + η], either decisive verdict is erroneous, but NONE may also occur outside the band; the guarantees do not promise conclusiveness.Source: §3.1 · pp. 5–6

3.2 Challenges and Key Insights

ProCerDCL reduces unnecessary executions by testing threshold assertions sequentially and stops when evidence supports either one. Bounds valid across checkpoints preserve error control during repeated inspection, while a finite cap permits abstention.

3.2 Challenges and Key Insights

  • Sequentially checking threshold assertions avoids estimating p to a prescribed absolute accuracy and stops when evidence establishes either p ≤ θ or p > θ + η.A finite cap bounds sampling cost when neither assertion is established.Source: §3.2 · p. 6
  • Repeated inspection requires bounds whose error control holds across checkpoints because ordinary fixed-sample intervals do not retain nominal coverage under early stopping.The paper implements this with corrected Clopper–Pearson intervals or an anytime-valid confidence sequence.Source: §3.2 · p. 6
  • One observation stream supports both acceptance and rejection tests, with NONE returned if neither condition holds by the cap.This single test supports the three-valued contract without separate tests over an interval family while retaining the direction-specific error budget.Source: §3.2 · pp. 6–7

3.3 Verification Procedure and Guarantees

The main mode applies one sequential test to a fixed distribution and oracle, returning a decisive verdict or NONE at a finite cap. An optional interval-family mode reuses observations across tests.

3.3.1 Main algorithm

  • The main mode runs Algorithm 2 once with fresh observations, returning a decisive result when its probability assertion is established and NONE when the cap is exhausted.The checkpoint batch size B is a statistical schedule and need not equal the runtime GPU batch size.Source: §3.3 · p. 7, §3.3.1 · p. 7
  • The single-test main mode has a finite observation cap of ⌈N/B⌉B; consistency checks require at most twice that many model executions, excluding runtime buffering.The theorem’s soundness and cap apply under A1–A3 for one fixed distribution and oracle.Source: §3.3.1 · p. 7
  • The theorem does not bound the probability of NONE, so the single-test contract bounds erroneous decisive verdicts rather than guaranteeing a decisive outcome.The forced-decision variants satisfy only the weaker indifference-zone guarantee.Source: §3.3.1 · p. 7, §3.3.2 · p. 8

3.3.2 Optional interval-family mode

  • The optional mode visits a predetermined interval family over a shared observation stream, with soundness under A1–A3 and distinct-observation cost equal to the longest visited prefix.Left intervals can return YES, right intervals NO, and the final interval any of the three outcomes.Source: §3.3.2 · pp. 7–8

3.4 Sequential Test and Interval-Family Details

The section develops the sequential tester’s error and cost guarantees, then describes interval scheduling for the optional interval-family mode.

3.4.1 Sequential tester (M3)

  • The CP tester checks exact Clopper–Pearson intervals at predetermined checkpoints, dividing δ_i across T_i checks; no independence between checkpoint intervals is required.It returns NONE if neither stopping condition holds at the last checkpoint.Source: §3.4.1 · p. 9
  • Wrong YES or NO verdicts require checkpoint coverage failure, while NONE asserts neither threshold inequality and incurs no error under the contract.The tester’s error control is stated under A1–A3 for fixed thresholds and an i.i.d. Bernoulli stream.Source: §3.4.1 · pp. 9–10
  • Near or inside the separation band, neither condition may hold before the cap, and checkpoint-corrected CP intervals can increase abstention.The anytime-valid CS variant uses the same δ_i at every checkpoint; forced-decision variants permit decisive answers inside the band and satisfy only the weaker indifference-zone guarantee.Source: §3.4.1 · p. 10

3.4.2 Interval scheduling (M1, optional)

  • The optional scheduler builds left and right intervals toward fixed endpoints, appends only intermediate intervals wider than η, then adds (θ, θ + η) as the final test.Left intervals have upper endpoint θ; right intervals have lower endpoint θ + η.Source: §3.4.2 · p. 10

10 else

The optional interval-family mode combines finite interval construction, error-budget allocation, and observation reuse.

10 else

  • Each interval side contracts by halving widths above η until it reaches the η floor, so the complete family terminates after finitely many calls.Intermediate intervals at or below the floor are omitted from the family.Source: §10 · pp. 10–11

3.4.3 Inverse-width allocation (M2, optional)

  • Inverse-width allocation is a cost heuristic; soundness requires only positive fixed budgets summing to at most δ, and the interval family is not guaranteed to outperform the single test.The global directional error bounds follow by a union bound over the fixed family.Source: §3.4.3 · p. 11

3.4.4 Observation reuse (M4, optional)

  • Reuse preserves direction-specific error bounds when the family and tester parameters are fixed before sampling; the shared pool grows to the longest consumed prefix.Reuse is restricted to the same distribution, oracle, model pair, and execution configuration.Source: §3.4.4 · pp. 11–12

4 Evaluation

The evaluation studies ProCerDCL on compiler-consistency checks, one-model robustness and radius searches, configuration and parameter sensitivity, and an unclipped patch perturbation distribution. It examines sampling cost and the resulting consistency verdicts, certificates, and reported radii.

4.1 Experimental Setup

  • The evaluation uses named perturbation distributions and audits oracle behavior, supporting batch-composition-independent decisions on audited inputs without establishing the assumption for every execution.Experiments include L2 and L∞ balls, text token substitutions, and an image patch; batch-size-1 decisions differed in 5 of 50,688 audited TensorRT decisions and none under Inductor.Source: §4 · p. 12, §4.1 · p. 13

4.2 Consistency Verdicts and Local Robustness

  • 817 of 840 pointwise consistency checks returned YES, 19 returned NONE, and 4 returned NO across 21 tasks at θ = 10^-3.These acceptances bound violation probability on sampled instances; they do not certify builds as semantically correct.Source: §4.2 · pp. 14, 17
  • Two documented Torch-TensorRT faults produced distinct local verdict patterns: the interpolation fault was rejected on 30/30 inputs, while the window-attention fault was rejected on 21/30.The window-attention fault returned NONE on 6 inputs and YES on 3; the two case studies do not establish comparative detection recall.Source: §4.2 · pp. 15–16
  • Across 24 tasks, certified radii agreed positively with attack difficulty in 46 of 48 cells, while reference-model controls correlated at 1.00.The control indicates that the radius measures primarily the model’s noise robustness, rather than a compiler-specific signal.Source: §4.2 · pp. 16–17, Figure 2 · p. 17

4.3 Sampling Cost and Conclusiveness

  • 3.6–4.2 times fewer draws were needed than PROVERO in paired one-model radius searches, at matched numerical parameters but under different decision contracts.The interval-family mode also used more draws than the main test in all four paired settings.Source: Table 6 · p. 18, §4.3 · pp. 19–20

4.4 RQ 3 Local Robustness across Configurations

  • Across evaluated configurations, radii reproduced across GPU generations at correlation 1.000, 397/400 simulated INT8 inputs were conclusive, and L∞ radii correlated with attack budgets at Pearson 0.50–0.86.Moving from an L2 ball to an L∞ box required only changing the sampler; the verifier and its guarantee remained unchanged.Source: Figure 3 · p. 20, Figure 4 · p. 20, §4.4 · pp. 20–21

4.3 Sampling Cost and Conclusiveness

  • Inconclusive probes consumed 61% of the main test’s draws, and the known-density study found one erroneous decisive verdict in 2,000 in-band runs and none in 10,000 outside-band runs.Near the threshold, the certifier abstained on 88–100% of streams; away from the band, all runs answered YES at densities up to θ/2 and NO from 2(θ + η) upward.Source: §4.3 · pp. 19–20

4.5 RQ 4 Parameter Study

  • Across eight parameter settings, every input was conclusive, while the certified radius varied by about a quarter and sampling cost spanned 11.6 times.Increasing θ from 0.5% to 5% raised median radius from 5.80 to 7.40 and changed draws to 1.83, 1, 0.53, and 0.24 times the default. Halving η multiplied draws by 2.76; raising confidence from 99% to 99.9% cost 1.36 times the draws, while lowering it to 95% reduced draws to 0.78 times the default without moving the median radius from 6.05. This sensitivity grid used ResNet-18/CIFAR-10 under Inductor, with 100 inputs per configuration.Source: §4.5 · p. 21, Table 8 · p. 21

4.6 RQ 5 Beyond Norm-Bounded Perturbations

  • The patch experiment shifted only the nine top-left pixels of MNIST independently and uniformly within ±ϵ without clipping, showing that the certificate applies beyond norm-ball perturbations.The protocol used LeNet-5 under both backends, with 100 attack-success inputs per backend; certificates were conclusive when the radius was positive and below the search cap of 400.Source: §4.6 · pp. 21–22
  • On the patch distribution, certificates were conclusive on 100 of 100 TorchInductor inputs and 99 of 100 TensorRT inputs, with Spearman correlations of 0.80 and 0.89 to attack difficulty (p < 10^-9).Pearson correlations were 0.60 and 0.79, and average draws were 165 and 171 thousand. Median radii were 0.91 and 0.87 of the attack budget, while 57% and 64% of radii lay below it; 87% and 85% exceeded the 3.25-unit valid pixel range. Nearly every search ended inconclusively near the boundary, and one TensorRT input was rejected at radius zero because the compiled engine changed the clean prediction.Source: §4.6 · p. 22, Table 9 · p. 22

5 Discussion and Threats to Validity

The discussion limits what the verifier’s verdicts establish: they apply to a specified distribution, oracle, and execution setting, not automatically to global equivalence or deployment behavior. It also identifies statistical assumptions and study-scope constraints that bound the conclusions.

Meaning of a verdict

  • YES permits rare violations and establishes neither global equivalence nor worst-case robustness; decision disagreement is not a semantic error without an additional correctness specification.The reference execution defines the comparison, not ground-truth correctness.Source: §5 · p. 22

Construct validity

  • Clean-label radius is dominated by model sensitivity, so its agreement with attack difficulty is not evidence of compiler correctness; test perturbations may not match deployment traffic.The discussion also notes that token substitutions need not preserve meaning.Source: §5 · p. 22

Internal validity

  • Independent draws and a stateless oracle are proof assumptions; audits support statelessness only for tested settings, and TensorRT certificates depend on execution configuration.The audits found no decision changes under repeated, permuted, or recomposed batches.Source: §5 · pp. 22–23

Conclusion validity

  • Guarantees hold for one fixed distribution; radius-search probes spend δ individually, simultaneous claims need further error allocation, and adaptive distributions require fresh draws.Bisection assumes monotonicity, so the reported radius is the largest tested radius certified YES; NONE may occur on either side of the band.Source: §5 · p. 23

External validity

  • Generalization is limited by differing study populations, attack-success selection, backend cohorts, and sampling seeds; two documented faults illustrate verdict patterns, not detection recall.The deployment-shift experiments concern one-model robustness.Source: §5 · p. 23
  • Near 10^-4, two-model checks still require millions of executions; rare-event estimators are identified as future work.Source: §5 · p. 23

6 Related Work

Related work spans compiler testing, formal and relational verification, and probabilistic robustness. ProCerDCL differs through its probability-threshold contract for explicit input distributions and its single-test procedure.

6 Related Work

  • Compiler fuzzing and differential testing target implementation bugs, while formal tools verify transformations and relational verifiers compare network pairs; their targets and access differ from ProCerDCL’s probability-threshold contract.ProCerDCL observes end-to-end executions through a binary property oracle, comparing decisions without a numerical-output tolerance.Source: §6 · p. 23
  • Explicit input distributions address reliability questions that fixed test sets may not capture, including benchmark-contamination concerns.The cited work notes that fixed-set evaluation can overstate reliability.Source: §6 · p. 23
  • PROVERO is the closest related work: it verifies one neural network’s probabilistic robustness, whereas ProCerDCL also checks paired reference–compiled decision consistency.The paired property requires both models to execute for each sampled input.Source: §6 · p. 23
  • Randomized smoothing yields a worst-case radius for a smoothed classifier, while ϵHard bounds disagreement density for a deployed model; their guarantees are incomparable.These are distinct from ProCerDCL’s probability-threshold contract for compiler-related properties.Source: §6 · p. 24
  • Unlike PROVERO’s interval-family procedure, ProCerDCL uses one sequential test under a stricter three-valued contract, counting decisive answers within (θ, θ + η] as errors and returning NONE when evidence is insufficient.The paper identifies the single-test procedure, its analysis, and compiler-property evaluation as its contribution.Source: §6 · p. 24

7 Conclusion

ProCerDCL provides black-box probabilistic verification for compiler-optimization consistency properties under stated sampling and oracle assumptions. Its evaluation reports lower sample use than PROVERO, consistency verdicts for most tested inputs, and diagnosis of two documented faults.

7 Conclusion

  • 3.6–4.2 times fewer unique samples than PROVERO at matched parameters, and reference–compiled consistency certified on 817 of 840 inputs at θ = 10^-3.The finite cap bounds cost rather than guaranteeing a decisive answer; verdicts remain specific to the chosen distribution, property, and execution configuration.Source: §7 · p. 24
  • Acceptance, rejection, and inconclusive verdicts have direction-specific error control under independent sampling and stateless oracle behavior.The single sequential test supports this contract without PROVERO’s interval family.Source: §7 · p. 24
  • Case studies of two documented compiler faults show that local verdicts can distinguish those faults from correct builds.The conclusion limits verdict interpretation to the chosen distribution, property, and execution configuration.Source: §7 · p. 24

Related papers

Loading 2610.36499v1…