Writing and Checking a VNN-LIB Specification

A specification is not only a file the parser accepts. It determines which question the verifier answers. The first useful test is therefore semantic: does a known good input satisfy the intended property, and does a known bad input violate it?

Decide whether the file describes good or bad behaviour

Suppose the intended claim is

A counterexample query asks whether

The output inequality has changed direction because the property was negated. Under an exact encoding of this bad-event query, sat means a violating case exists and unsat means none exists. This interpretation comes from the query, not from a universal convention that the letters SAT mean safe or unsafe in every tool.

A complete small specification

Use the scalar-output network from the verification problem:

The following is a legacy VNN-COMP-style VNN-LIB specification with scalar X_0 and Y_0 variables. The model is supplied separately, and Y_0 denotes its scalar output.

; Input and output variables; the network is a separate model file.
(declare-const X_0 Real)
(declare-const Y_0 Real)

; Input region: -1 <= x <= 1, in RAW model-input units.
; This file does not normalise; the last section of this chapter says why that
; has to be written down rather than assumed.
(assert (>= X_0 (- 1.0)))
(assert (<= X_0 1.0))

; Bad event for the strict property g(x) > 0.
(assert (<= Y_0 0.0))

This example deliberately labels the dialect. The VNN-LIB site now also documents newer syntax with explicit network declarations. A parser that accepts one dialect does not automatically accept the other. Record the file format and the verifier version used in an experiment.

The true network output is $1/4$, so the bad-event query is unsatisfiable under its exact real-valued semantics. A loose LP relaxation may make the same bad event feasible; that establishes UNKNOWN for the original property unless a real input is recovered and checked.

Check classification logic carefully

For reference class $y$, unique-highest-score robustness requires $f_y(x)>f_j(x)$ for every $j\ne y$. A bad event is therefore a disjunction: at least one rival score is greater than or equal to the reference score.

; Example: class 0 must strictly beat both other outputs.
(assert (or (>= Y_1 Y_0) (>= Y_2 Y_0)))

Replacing or with and asks for a much smaller bad-event set. Proving that this smaller set is empty would not prove the intended classification property. This is why a parser’s tensor representation must preserve Boolean grouping rather than concatenate every output inequality into one conjunction.

Verify the input pipeline too

State whether the bounds refer to raw values or normalised values, because the same digits mean different things. Under per-channel normalisation $x_{\text{norm}}=(x_{\text{raw}}-\mu)/\sigma$ with positive $\sigma$, a perturbation of size $\delta$ in normalised space is a perturbation of size $\sigma\delta$ in raw space — so a normalised bound multiplied by $\sigma$ gives the raw one, and a raw bound divided by $\sigma$ gives the normalised one, and the direction is the part that is easy to get backwards. Say which one the file is written in. State any clipping to the valid raw domain before converting, since $\sigma$ scaling is only meaningful inside the range where normalisation applies.

A model export with a different channel order, preprocessing convention or output interpretation is a different verification object. Keep the model hash, property file, configuration and tool version together.

Test the specification before a long run

Check that the input domain is nonempty. Evaluate a few known inputs to catch sign and label mistakes; this is a specification sanity check, not a proof over the domain. Include an intentionally wrong or/and or sign variant and make sure your expected behaviour changes.

When a tool returns a witness, verify every input constraint and evaluate the intended model. When it returns UNKNOWN, do not rewrite the output condition until the instance becomes easy without recording that the claim has changed.

Key Takeaways

A solver answers the encoded query. Specify whether you encoded the desired property or its negation.

Preserve Boolean structure. A disjunction of bad cases is not the same as their conjunction.

Pin the format and model semantics. A valid file is not enough if it refers to the wrong input or output interpretation.