3. Verification techniques for model implementation

Model verification asks a deceptively simple question: does the implementation faithfully realize the specification? For AI systems, the "implementation" is a hybrid artifact — Python training code, serialized weights, inference graphs, preprocessing pipelines, and the runtime that executes them. Static analysis, formal methods, symbolic execution, and runtime verification each attack a different slice of this surface. This chapter explains what each technique actually proves, how to apply it to AI code and model artifacts, and where the boundaries lie.

Static Analysis: Cheap, Broad, and Shallow

Static analysis inspects source code or model graphs without executing them. In AI pipelines it catches a surprising number of real defects: shape mismatches, dtype inconsistencies, uninitialized parameters, dead branches in preprocessing, and unsafe deserialization. Tools such as pylint, mypy, ruff, and bandit cover the Python side; onnx.checker and framework-specific graph validators cover the artifact side.

A practical pattern is to run type checking with strict annotations on the model definition and data pipeline. Consider a classifier whose forward pass expects float32 inputs of shape [B, 3, 224, 224]. A static checker will not catch a runtime shape error, but it will catch that a preprocessing function annotated to return np.ndarray is actually returning a PIL.Image, or that a normalization constant is a Python int where a tensor is expected. For serialized artifacts, run structural validation before loading:

import onnx
model = onnx.load("classifier.onnx")
onnx.checker.check_model(model)          # structural + schema validation
print(model.graph.input[0].type)         # confirm expected tensor type/shape

Static analysis is sound in the direction of "reports only what it can prove suspicious" but incomplete — it misses anything requiring value knowledge. Treat it as a fast gate in CI, not as evidence of correctness.

Formal Methods: Properties, Not Anecdotes

Formal methods express desired behavior as mathematical properties and attempt to prove them over all inputs (or all inputs in a bounded domain). For AI code, the tractable properties are usually local: monotonicity of a preprocessing transform, range preservation of a normalization layer, equivalence between two implementations of the same operator, or robustness of a small network to bounded input perturbations.

A concrete and reproducible example is bounded robustness for a tiny ReLU network. Given input domain x ∈ [0,1]² and a perturbation radius ε = 0.01, we want to prove the predicted class never changes. Tools like Marabou or α,β-CROWN encode the network and the property as a satisfiability problem. If the solver returns UNSAT, the property holds for every point in the domain; if it returns SAT, it also returns a concrete counterexample input — which is immediately useful as a regression test.

Formal verification of full-scale models is generally intractable. Scope properties to small subnetworks, individual operators, or bounded input regions where the solver can terminate. A proved property over a restricted domain is still far stronger than random testing.

The main engineering cost is property authoring. A property must be precise enough to be falsifiable and general enough to be meaningful. "The model is fair" is not a property; "for all inputs where feature 7 is unchanged, the output score changes by at most δ" is.

Symbolic Execution: Path-Sensitive Reasoning

Symbolic execution runs code with symbolic rather than concrete inputs, tracking path constraints and using a solver to determine which paths are feasible. Applied to AI code, it excels at preprocessing and postprocessing logic — the hand-written glue where most implementation bugs live. It can prove that a resize-and-crop function never produces out-of-bounds indices, or that a tokenizer's truncation branch is reachable only when sequence length exceeds the limit.

For example, symbolic execution of a bounding-box clipping routine with symbolic coordinates can enumerate the branches where x_min > x_max after clipping and confirm whether an empty-box case is handled. The output is a set of feasible paths with concrete example inputs per path, which doubles as a path-coverage test suite. The classic limitation is path explosion: loops over sequence length or batch size multiply paths exponentially. Mitigate by bounding loop iterations, abstracting tensor operations as uninterpreted functions, and focusing on scalar control flow rather than the numerical kernels themselves.

Runtime Verification: Watching the Deployed System

Runtime verification monitors execution against a specification and raises alarms when behavior deviates. It is the only technique here that observes the actual deployed model with real data. Typical monitors for AI systems include:

  • Input distribution monitors — flag feature vectors outside the training range (e.g., a normalized pixel mean drifting beyond [−3, 3]).
  • Output invariant monitors — assert that a probability vector sums to 1 within tolerance, or that a regression output stays within physically plausible bounds.
  • Temporal properties — using specification languages such as past-time LTL to assert, for instance, that a confidence score never drops below threshold for more than N consecutive frames without triggering a fallback.

A lightweight implementation attaches hooks to the inference path and evaluates predicates per batch, logging violations with the offending sample for offline triage. The key design decision is the response policy: log-only, degrade gracefully (fall back to a conservative model), or hard-fail. Runtime monitors must themselves be cheap and cannot depend on ground-truth labels, which are usually unavailable at inference time.

Verification Techniques Across the AI Artifact Lifecycle ARTIFACT LIFECYCLE Source & training code Serialized weights / graph Pre/post-processing Deployed inference Static Analysis no execution · fast · CI gate • type & dtype checks • shape annotations • dead-code detection • unsafe deserialization • ONNX schema check Proves: structural consistency only Formal Methods all inputs in domain · solver • bounded robustness • operator equivalence • monotonicity proofs • range preservation • UNSAT / SAT + witness Proves: property holds over bounded domain Symbolic Execution path-sensitive · constraint solving • branch feasibility • index bounds proofs • truncation reachability • path-coverage tests • counterexample per path Proves: path feasibility + concrete witnesses Runtime Verification live execution · no labels needed • input drift monitors • output invariants • temporal properties • violation logging • fallback triggers Detects: deviation at inference time Layered assurance: static gate → formal proof of scoped properties → symbolic path tests → runtime monitoring in production

Combining the Techniques

These four techniques are complementary rather than competing, and the diagram above maps each to the lifecycle stage where it is most effective. A defensible verification strategy layers them: static analysis as a mandatory CI gate on every commit; formal methods applied to a curated set of safety-critical properties (bounded robustness, operator equivalence after quantization); symbolic execution targeting preprocessing and postprocessing code where control flow is dense; and runtime monitors on the deployed endpoint to catch distribution shift and invariant violations that no offline technique can anticipate.

Two practical cautions apply. First, each technique produces evidence of a specific kind — a static warning, a proof over a domain, a feasible path, or a runtime alarm — and that evidence must be recorded with its scope. A robustness proof for ε = 0.01 says nothing about ε = 0.05. Second, verification artifacts should be versioned alongside the model. When weights are retrained or a graph is re-exported, previously proved properties must be re-checked; a passing formal proof against an old checkpoint is not evidence about the new one. Wiring these checks into the model registry, so that promotion is blocked when a required proof or monitor configuration is missing, turns verification from a one-off exercise into a property of the delivery pipeline.

Do not treat a clean static-analysis run or a single passing robustness proof as a statement that "the model is verified." Each result is scoped to a technique, a property, and a domain. Credibility claims must carry that scope explicitly.
← Previous 📖 Contents Next →