TorchVNNLIB: A Story of Fast VNN-LIB Property Loading

Introduction

A verification run that checks one model against a thousand properties should not parse those same thousand properties again on the next run. That is the whole observation this tool is built on, and it is worth stating precisely because the asymmetry it exploits is not obvious.

Verification workflows load a model once and then verify it repeatedly, once per property. The model is a multi-megabyte ONNX file with thousands of operations, and it loads quickly because it is a binary format designed for the purpose. The properties are small text files specifying input bounds and output constraints — and each one gets parsed from scratch, every time, for every run.

So the large artefact is handled well and the small one is handled badly, and the reason is that “small” was allowed to imply “cheap to re-read”.

The performance gap was striking:

Neural Network Loading (ONNX):
├─ Model: Multi-megabyte binary file
├─ Loading: Fast (binary format)
└─ Format: Protocol Buffers

Property Loading (VNN-LIB):
├─ Properties: Text files
├─ Loading: Slow (parse every time)
└─ Format: Text-based SMT-LIB

Convert the properties once, into the format the model already uses, and the per-run cost becomes deserialisation rather than parsing.

That’s what TorchVNNLIB does. It converts VNN-LIB specification files into binary formats (PyTorch .pth or NumPy .npz) and leaves the deserialisation to whoever verifies. Convert once, load many times—just like how we handle ONNX models.

But building a fast VNN-LIB converter wasn’t just about picking a binary format. The real challenge was handling the diversity of VNN-LIB files in the wild. Some properties are simple (just input bounds and a few output constraints). Others are complex (nested OR/AND logic, multiple constraint groups, non-standard operators). A naive parser would be correct but slow. An optimized parser would be fast but fragile.

The solution? A two-tier processing architecture:

1. Fast Type Detection: Pattern-match against 5 common VNN-LIB structures (Types 1-5) using lightweight regex. Handles the common shapes without ever building a syntax tree.
2. AST Fallback: For complex cases that don’t match the patterns, fall back to a full Abstract Syntax Tree parser. Slower but handles anything.

This design follows the 90/10 rule: optimize for the common case (fast path), but handle the general case correctly (AST fallback). That phrase is my own shorthand rather than the project’s — the tool never names it. What is worth stating precisely is the mechanism underneath it, skipping tokenization and syntax-tree construction entirely, because any speedup is a ratio against some particular text parser, and a better parser moves that denominator without touching the numerator.

TorchVNNLIB also introduces a dual backend design. Some verification tools use PyTorch (and benefit from GPU acceleration). Others prefer lightweight dependencies. So TorchVNNLIB supports both:

• PyTorch Backend: Saves properties as .pth files with GPU-ready tensors
• NumPy Backend: Saves properties as .npz files with no PyTorch dependency

The backends share the same core processing logic through an abstraction layer. Choose your backend at initialization, and everything else just works.

In this post, I’ll walk through the design and implementation of TorchVNNLIB:

• Part 1: Understanding the problem—what is VNN-LIB, and why is text parsing a bottleneck?
• Part 2: Design philosophy—the 90/10 rule and two-tier architecture
• Part 3: Fast type detection—pattern matching with regex for optimized processing
• Part 4: AST-based general parser—handling complex cases correctly
• Part 5: Dual backend design—PyTorch vs NumPy, and what the choice costs
• Part 6: Code quality and usability—the API surface and how it fails
• Part 7: Real-world validation—VNN-COMP 2024 conversion results

By the end, you’ll understand not just how TorchVNNLIB works, but why certain design decisions matter for building fast, reliable verification tools.

Let’s start by understanding the problem.

Part 1: Understanding the Problem — VNN-LIB and the Parsing Bottleneck

1.1 What is VNN-LIB?

VNN-LIB (Verification of Neural Networks Library) is a standardized format for specifying verification properties for neural networks. It’s based on SMT-LIB syntax and is widely used in the neural network verification community, particularly for the annual VNN-COMP competition.

A VNN-LIB file describes constraints on a neural network’s inputs and outputs. Here’s a simple example:

; Declare input and output variables
(declare-const X_0 Real)
(declare-const X_1 Real)
(declare-const Y_0 Real)
(declare-const Y_1 Real)

; Input constraints: bounds on inputs
(assert (>= X_0 -0.5))
(assert (<= X_0 0.5))
(assert (>= X_1 -0.3))
(assert (<= X_1 0.3))

; Output constraint: Y_0 should be greater than Y_1
(assert (>= Y_0 Y_1))

This property says: “For all inputs where X_0 in [-0.5, 0.5] and X_1 in [-0.3, 0.3], the first output Y_0 must be greater than or equal to the second output Y_1.”

The verification task is to prove (or find a counterexample) that this property holds for a given neural network.

VNN-LIB supports more complex properties too:

• Disjunctions (OR): Multiple alternative constraint groups
• Conjunctions (AND): Multiple constraints that must all hold
• Linear inequalities: General form $a_1X_1 + a_2X_2 + ... + b \geq 0$
• Nested logic: Arbitrary nesting of OR/AND operators

For example, a property might say: “Either (input bounds A and output constraint B) OR (input bounds C and output constraint D).” This creates multiple sub-properties to verify.

Why VNN-LIB matters: It’s the standard format for VNN-COMP, meaning any serious verification tool needs to parse it. The format is flexible and expressive, but that flexibility comes with a cost: parsing complexity.

1.2 The Parsing Bottleneck

The typical loop is: load the model once, then for each of the benchmark’s hundred or thousand properties, parse it, run the verifier, repeat. Everything except the parsing happens once; the parsing happens every time.

Why is text parsing slow?

1. Tokenization overhead: Split text into tokens (parentheses, operators, numbers, identifiers)
2. Syntax tree construction: Build a parse tree from tokens
3. Semantic analysis: Extract variable declarations, constraints, logical structure
4. No caching: Parse from scratch every time (no intermediate representation)

Binary formats avoid all of it: the data is already structured, so deserialising it is the whole job. How large a difference that makes is a property of the pair — this text parser against these files — rather than of binary formats in general, because a faster parser changes only the denominator.

Integration friction: Most modern verification tools use PyTorch for GPU acceleration or NumPy for numerical operations. But VNN-LIB is text-based, so there’s an impedance mismatch:

# Current workflow (slow)
for property_file in vnnlib_properties:
    # Parse VNN-LIB text -> extract constraints -> convert to PyTorch tensors
    constraints = parse_vnnlib(property_file)  # Slow!
    input_bounds = torch.tensor(constraints['input'])
    output_constrs = torch.tensor(constraints['output'])
    verify(model, input_bounds, output_constrs)

# Ideal workflow (fast)
for property_file in converted_properties:
    # Directly load the two stored entries: no tokenizer, no tree
    data = torch.load(property_file)  # Fast!
    verify(model, data['input'], data['output'])

The converted workflow eliminates the parse-extract-convert pipeline. Just load and go.

1.3 Why Not Existing Solutions?

Before building TorchVNNLIB, I surveyed existing approaches:

Approach 1: Parse every time

• What most tools do: Parse VNN-LIB from scratch for each verification run
• Pros: Simple, no dependencies, always up-to-date
• Cons: Slow, repeated work, no caching

Approach 2: Custom verification-tool-specific parsers

• Some tools (alpha,beta-CROWN, ERAN) have built-in VNN-LIB parsers
• Pros: Optimized for that specific tool
• Cons: Not reusable, duplicated effort, inconsistent behavior across tools

Approach 3: General SMT-LIB libraries

• Use existing SMT-LIB parsers (e.g., pysmt, z3)
• Pros: Handles full SMT-LIB syntax, well-tested
• Cons: Overkill for neural network properties (slow), not optimized for our use case, awkward conversion to tensors

What’s missing: A tool that:

1. Converts once, loads many times: Binary caching for repeated use
2. GPU-ready: Direct PyTorch tensor output (no conversion needed)
3. Lightweight option: NumPy arrays for tools without PyTorch
4. Standardized constraint format: Consistent representation across tools
5. Handles diverse VNN-LIB patterns: Works on real-world benchmarks (not just toy examples)

That’s what TorchVNNLIB provides.

Design Goals:

1. Performance: per-run cost becomes deserialisation instead of parsing
2. Correctness: Full conversion coverage on the tested VNN-COMP benchmark set
3. Flexibility: Support both PyTorch and NumPy backends
4. Usability: Simple API (convert once, load anywhere)
5. Robustness: Handle both common patterns (fast) and edge cases (correct)

In the next section, I’ll show you how the two-tier architecture achieves these goals.

Part 2: Design Philosophy and Two-Tier Architecture

The core insight behind TorchVNNLIB is simple: most VNN-LIB files follow predictable patterns. If we can detect these patterns quickly and handle them with optimized code paths, we can achieve significant speedups without sacrificing correctness.

This is the 90/10 rule in action: 90% of files match common patterns (fast path), 10% are edge cases (general path). Optimize for the common case, but don’t break on the edge cases.

2.1 The 90/10 Rule — Fast Path Optimization

After analyzing hundreds of VNN-LIB files from VNN-COMP benchmarks, I noticed a pattern. While the VNN-LIB specification allows arbitrary complexity, real-world properties cluster around a few common structures:

Type 1: Simple input bounds + simple output constraints

; Just bounds and a few constraints--no OR groups
(assert (>= X_0 -1.0))
(assert (<= X_0 1.0))
(assert (>= Y_0 Y_1))

This is the most common shape. The structure is straightforward: bounds on inputs, a handful of output constraints, all combined with AND.

Type 2: Simple input bounds + OR-grouped output constraints

(assert (>= X_0 -1.0))
(assert (<= X_0 1.0))
(assert (or
    (>= Y_0 Y_1)
    (>= Y_0 Y_2)
))

Output constraints are wrapped in an OR, creating multiple sub-properties to verify. Also common.

Type 3: OR-grouped input bounds + simple output constraints

(assert (or
    (and (>= X_0 -1.0) (<= X_0 0.0))
    (and (>= X_0 0.0) (<= X_0 1.0))
))
(assert (>= Y_0 Y_1))

Input space is divided into regions (OR groups), each with its own bounds.

Type 4: OR-grouped input bounds + OR-grouped output constraints

Both inputs and outputs have OR groups—creates a Cartesian product of sub-properties.

Type 5: Top-level OR wrapping complete properties

(assert (or
    (and (>= X_0 -1.0) (<= X_0 0.0) (>= Y_0 Y_1))
    (and (>= X_0 0.0) (<= X_0 1.0) (>= Y_1 Y_0))
))

Each OR branch is a complete property specification.

The key observation: these 5 shapes are the whole vocabulary of the matcher. A file that uses complex nested logic, non-standard operators, or unusual constraint forms matches none of them — and matching none of them is not a failure, it is the signal to use the general parser.

Strategy: Build specialized processors for Types 1-5 that use lightweight pattern matching (regex). For everything else, fall back to a full AST parser.

2.2 Two-Tier Processing Pipeline

Here’s how the processing pipeline works:

Input: VNN-LIB File
     |
+----------------------------+
|  Preprocess                | <-- Extract variable declarations
|  (declare-const X_0 Real)  |   Count inputs/outputs
+----------------------------+
     |
+----------------------------+
|  Fast Type Detection       | <-- Regex pattern matching
|  (Scan for Types 1-5)      |   Structural analysis (no parsing!)
+----------------------------+
     |
     +--- Type Detected (1-5)
     |         |
     |    +---------------------------+
     |    |  Fast Processor           | <-- Direct regex extraction
     |    |  - Regex for bounds       |   Optimized path
     |    |  - Regex for constraints  |
     |    |  - Build tensors          |
     |    +---------------------------+
     |         |
     |    Constraint Tensors (b + Ax >= 0)
     |
     +--- Complex/Unknown
               |
          +---------------------------+
          |  AST Processor            | <-- Full parsing pipeline
          |  1. Tokenize              |   Slower but handles anything
          |  2. Parse (build AST)     |
          |  3. Optimize              |
          |  4. Flatten (to DNF)      |
          |  5. Convert to tensors    |
          +---------------------------+
               |
          Constraint Tensors (b + Ax >= 0)

Why this works:

1. Fast type detection is cheap: a regex scan does no tokenization and builds no tree. The project’s own architecture notes put these processors an order of magnitude or two ahead of the AST path, and this note does not re-measure that — the ratio depends on the corpus and on what the AST path costs, both of which are properties of the pair rather than of the matchers. Even when detection fails, all that was wasted is one scan.
2. Fast processors are fast: No tokenization, no AST construction—just regex and tensor building. Significantly faster than AST parsing.
3. AST fallback ensures correctness: If a file doesn’t match Types 1-5, we don’t fail—we just use the slower (but general) AST parser.
4. Graceful degradation: Performance degrades gracefully for complex files, but we never sacrifice correctness.

In practice: a file matching one of the five takes the fast path. Anything else takes the AST fallback, which is slower and still correct.

2.3 Backend Abstraction

TorchVNNLIB needs to support two different backends: PyTorch and NumPy. But the core conversion logic (parsing VNN-LIB, extracting constraints, building matrices) should be the same regardless of backend.

The solution is a backend abstraction layer:

from abc import ABC, abstractmethod

class Backend(ABC):
    """Abstract interface for tensor backends."""

    @abstractmethod
    def zeros(self, shape, dtype="float64"):
        """Create a zero-initialized tensor."""
        pass

    @abstractmethod
    def tensor(self, data, dtype="float64"):
        """Create a tensor from Python data."""
        pass

    @abstractmethod
    def stack(self, tensors, axis=0):
        """Stack tensors along an axis."""
        pass

    @abstractmethod
    def save(self, data, file_path):
        """Save data to file."""
        pass

This interface defines the operations we need for tensor manipulation. Now we implement it twice:

PyTorch Backend:

import torch

class TorchBackend(Backend):
    def zeros(self, shape, dtype="float64"):
        torch_dtype = torch.float64 if dtype == "float64" else torch.float32
        return torch.zeros(shape, dtype=torch_dtype)

    def tensor(self, data, dtype="float64"):
        torch_dtype = torch.float64 if dtype == "float64" else torch.float32
        return torch.tensor(data, dtype=torch_dtype)

    def stack(self, tensors, axis=0):
        return torch.stack(tensors, dim=axis)

    def save(self, data, file_path):
        torch.save(data, file_path)

NumPy Backend:

import numpy as np

class NumpyBackend(Backend):
    def zeros(self, shape, dtype="float64"):
        return np.zeros(shape, dtype=dtype)

    def tensor(self, data, dtype="float64"):
        return np.array(data, dtype=dtype)

    def stack(self, tensors, axis=0):
        return np.stack(tensors, axis=axis)

    def save(self, data, file_path):
        np.savez_compressed(file_path, **data)

The core conversion logic uses the abstract interface:

class TorchVNNLIB:
    def __init__(self, output_format="torch"):
        if output_format == "torch":
            self.backend = TorchBackend()
        elif output_format == "numpy":
            self.backend = NumpyBackend()

    def build_constraint_matrix(self, constraints):
        # This code works with BOTH backends!
        n_constraints = len(constraints)
        matrix = self.backend.zeros((n_constraints, n_vars + 1))

        for i, constr in enumerate(constraints):
            matrix[i, 0] = constr.bias
            for var, coef in constr.coefficients.items():
                matrix[i, var_index[var]] = coef

        return matrix

Notice how build_constraint_matrix() doesn’t know or care which backend it’s using. It just calls self.backend.zeros(), and the right implementation is invoked.

Benefits:

1. No code duplication: Core logic is shared between backends
2. Easy to add new backends: Implement the Backend interface (TensorFlow? JAX?)
3. Type safety: Static analysis can check that all backends implement the interface
4. Testability: Can swap backends during testing

2.4 Constraint Representation: b + Ax >= 0

VNN-LIB allows many ways to express constraints:

(>= X_0 -1.0)          ; Lower bound
(<= X_0 1.0)           ; Upper bound
(>= Y_0 Y_1)           ; Output comparison
(>= (+ (* 2.0 Y_0) (* -1.5 Y_1)) 3.0)  ; Linear inequality

TorchVNNLIB converts all of these to a canonical form: $b + Ax \geq 0$, where:

• $b$ is a bias term (scalar)
• $A$ is a coefficient matrix (1D array, one entry per variable)
• $x$ is the variable vector

Example conversions:

VNN-LIB: (>= X_0 -1.0)
Canonical: -1.0 + 1.0*X_0 >= 0
Vector form: b = -1.0, A = [1.0, 0, 0, ...]

VNN-LIB: (<= X_0 1.0)
Canonical: 1.0 + (-1.0)*X_0 >= 0
Vector form: b = 1.0, A = [-1.0, 0, 0, ...]

VNN-LIB: (>= Y_0 Y_1)
Canonical: 0.0 + 1.0*Y_0 + (-1.0)*Y_1 >= 0
Vector form: b = 0.0, A = [..., 1.0, -1.0, ...]

VNN-LIB: (>= (+ (* 2.0 Y_0) (* -1.5 Y_1)) 3.0)
Canonical: -3.0 + 2.0*Y_0 + (-1.5)*Y_1 >= 0
Vector form: b = -3.0, A = [..., 2.0, -1.5, ...]

Why this representation?

1. Uniform: All constraints have the same structure (easy to stack into matrices)
2. Verification-friendly: Most verification algorithms expect this form
3. Efficient: Matrix operations are fast on GPUs ($Ax$ is a single matrix-vector multiply)
4. Composable: Easy to combine constraints (just stack rows)

Storage format:

For input bounds (always axis-aligned boxes), we use a compact (n_inputs, 2) array:

input_bounds = np.array([
    [lower_0, upper_0],  # Bounds for X_0
    [lower_1, upper_1],  # Bounds for X_1
    # ...
])

For output constraints (general linear inequalities), each constraint contributes one row to a (n_constraints, 1 + n_vars) matrix:

output_constrs = np.array([
    [b_0, a_0_Y0, a_0_Y1, ...],  # Constraint 0: b_0 + a_0_Y0*Y_0 + a_0_Y1*Y_1 + ... >= 0
    [b_1, a_1_Y0, a_1_Y1, ...],  # Constraint 1
    # ...
])

This format is what verification tools expect, so no conversion is needed after loading.

Property structure: VNN-LIB properties can have OR groups. TorchVNNLIB preserves this structure in the output directory:

output/
+-- or_group_0/          <-- First OR alternative
|   +-- sub_prop_0.pth   <-- First AND group within this OR
|   +-- sub_prop_1.pth   <-- Second AND group
+-- or_group_1/          <-- Second OR alternative
    +-- sub_prop_0.pth

Each .pth file contains exactly two keys:

{
    'input': tensor([[lower_0, upper_0], ...]),   # (n_inputs, 2)
    'output': (                                   # one tensor per constraint
        tensor([b_0, a_00, a_01, ...]),           # (1 + n_outputs)
        ...,
    ),
}

Nothing else is serialised. n_inputs and n_outputs exist as parameters and as fields of the converter’s stats, and both are recoverable from the arrays themselves — a reader does not need them written down to use the file.

This structure matches the logical structure of the VNN-LIB file, making it easy to iterate over OR groups and sub-properties during verification.

In the next section, I’ll show you how the fast type detection system works under the hood.

Part 3: The Fast Type Detection System

The fast type detection system is where TorchVNNLIB achieves its performance gains for common cases. By using lightweight regex patterns instead of full parsing, we can quickly identify the structure of a VNN-LIB file and extract constraints directly—no AST needed.

3.1 Pattern Recognition with Regex

The challenge: Given a VNN-LIB file, determine its type (1-5 or complex) without building a full syntax tree.

The solution: Scan the file looking for structural markers—specific patterns that distinguish one type from another.

Here are the regex patterns we use:

# Simple input bound: (assert (>= X_0 -1.0))
SIMPLE_INPUT_BOUND_PATTERN = re.compile(
    r"^\s*\(\s*assert\s+\(\s*(<=|>=|=)\s+(X_)(\d+)\s+"
    r"([-+]?(?:\d+\.\d*|\.\d+|\d+)(?:[eE][-+]?\d+)?)\s*\)\s*\)\s*$"
)

# Simple output constraint: (assert (>= Y_0 Y_1))
SIMPLE_OUTPUT_CONSTRAINT_PATTERN = re.compile(
    r"^\s*\(\s*assert\s+\(\s*(<=|>=)\s+(Y_)(\d+)\s+(Y_)(\d+)\s*\)\s*\)\s*$"
)

# Simple output bound: (assert (>= Y_0 0.5))
SIMPLE_OUTPUT_BOUND_PATTERN = re.compile(
    r"^\s*\(\s*assert\s+\(\s*(<=|>=|=)\s+(Y_)(\d+)\s+"
    r"([-+]?(?:\d+\.\d*|\.\d+|\d+)(?:[eE][-+]?\d+)?)\s*\)\s*\)\s*$"
)

These patterns match the simplest VNN-LIB assertions—the building blocks of Types 1-5.

Type detection algorithm:

def fast_detect_type(lines: list[str], verbose: bool = False) -> VNNLIBType:
    """Fast type detection without parsing - classify VNN-LIB structure."""

    # Pattern flags to track what we've seen
    pattern_flags = {
        "has_simple_input": False,
        "has_simple_output": False,
        "has_or_and_input": False,
        "has_or_and_output": False,
        "has_or_and_mixed": False,
        "has_output_info": False,
    }

    # Full scan to avoid false negatives when inputs/outputs are interleaved
    for line in lines:
        stripped = line.strip()

        if stripped.startswith("(assert (or (and"):
            has_x = "X_" in stripped
            has_y = "Y_" in stripped

            if has_x and has_y:
                pattern_flags["has_or_and_mixed"] = True
                break
            elif has_x:
                pattern_flags["has_or_and_input"] = True
            elif has_y:
                pattern_flags["has_or_and_output"] = True
                pattern_flags["has_output_info"] = True

        elif stripped.startswith("(assert"):
            has_x = "X_" in stripped
            has_y = "Y_" in stripped

            if has_x and not has_y:
                pattern_flags["has_simple_input"] = True
            elif has_y and not has_x:
                pattern_flags["has_simple_output"] = True
                pattern_flags["has_output_info"] = True

    return _classify_type_by_patterns(
        pattern_flags["has_simple_input"],
        pattern_flags["has_simple_output"],
        pattern_flags["has_or_and_input"],
        pattern_flags["has_or_and_output"],
        pattern_flags["has_or_and_mixed"],
    )

The key insight: We don’t need to parse the entire file. Just scan for structural markers (assert, or, and, X_, Y_), count what we see, and classify accordingly.

Why a full forward scan? The loop walks every line from the top, and the code’s own comment gives the reason: a partial scan produces false negatives on files whose input bounds and output constraints are interleaved. The one early exit is a single line mixing X_ and Y_ inside an (or (and block, which has already crossed the boundary between TYPE5 and the general case — nothing later in the file can change the answer, so the rest of the scan would be wasted work.

3.2 Type Coverage in VNN-COMP 2024

Classification here is a lookup, not a score. The five booleans the scan collected are the key, and the table has exactly five accepted combinations; anything else returns COMPLEX. There is no threshold to tune and no percentage to quote — a file either matches one of the five shapes or it does not, and the second case is a documented outcome rather than a miss.

Which is also why this detector cannot report coverage over a corpus. It answers one question about one file — which shape is it — and a distribution over many files is a property of the corpus rather than of the matcher. The benchmark suite asks a different question of each file instead, and Part 7 comes back to it: does the fast path produce what the general parser produces?

Part 4: AST-Based General Parser

The fast type detection system handles those five shapes. But what about a file that matches none of them? These are the complex cases—files with nested OR/AND logic, unusual operators, non-standard constraint forms. For these, we need a general-purpose parser that can handle anything VNN-LIB throws at us.

4.1 The 5-Stage AST Pipeline

The AST parser has 5 stages:

Stage 1: Tokenization
Stage 2: Parsing (Build AST)
Stage 3: Optimization (Simplify, Flatten, Deduplicate)
Stage 4: Flattening (to DNF - Or of ANDs)
Stage 5: Tensor Conversion

4.2 AST Node Design

The AST is built from expression nodes:

class Expr:
    """Base class for all expression nodes."""

class Cst(Expr):
    """Constant value (e.g., -1.0, 3.5)."""
    def __init__(self, value: float):
        self.value = value

class Var(Expr):
    """Variable (e.g., X_0, Y_1)."""
    def __init__(self, name: str):
        self.name = name
        self.var_type = name[0]  # 'X' or 'Y'
        self.index = int(name[2:])

class Geq(BinaryOp):
    """Greater-than-or-equal: a >= b."""
    pass

class And(NaryOp):
    """Logical AND: and(a, b, c, ...)."""
    pass

class Or(NaryOp):
    """Logical OR: or(a, b, c, ...)."""
    pass

Key optimization: Use a deque instead of a list for tokens. Popping from the left of a deque is O(1), while popping from a list is O(n). For large files, this makes a significant difference.

Part 5: Dual Backend Design, and What It Costs

5.1 Why Two Backends?

5.2 Numerical Precision

Both backends use float64 by default to ensure numerical precision, and they build the same constraint rows through the same shared helpers — the backend is an allocator, not a second implementation. Exact equality is asserted where the suite can hold both sides to it: fast path against AST path, per file, per row. Cross-backend equality is not asserted with exact equality anywhere, because the suite’s tolerance-based comparison is what a .pth/.npz pair actually gets.

Part 6: Code Quality and Usability — the API Surface

6.1 API Design — Simplicity First

The API has one main entry point:

from torchvnnlib import TorchVNNLIB

# Initialize converter (choose backend)
converter = TorchVNNLIB(output_format="torch")  # or "numpy"

# Convert a VNN-LIB file
converter.convert("property.vnnlib", "output_dir")

That’s it. Two lines to convert a VNN-LIB file to binary format.

Loading the converted property:

# PyTorch backend
import torch
data = torch.load("output_dir/or_group_0/sub_prop_0.pth")
input_bounds = data['input']        # (n_inputs, 2)
output_constrs = data['output']     # one tensor per constraint, (1 + n_outputs)

# NumPy backend
import numpy as np
# allow_pickle is required: 'output' is a tuple of tensors, so savez stores it
# as an object array
data = np.load("output_dir/or_group_0/sub_prop_0.npz", allow_pickle=True)
input_bounds = data['input']
output_constrs = data['output']

Part 7: Real-World Validation — VNN-COMP 2024

7.1 Conversion Success Rate

There is no property that fails outright because the matcher did not recognise it, and that is a structural property rather than a lucky result. A type processor that raises is caught, the reason is recorded in the converter’s per-file stats, and the file is re-run through the AST path. The fallback is reachable by construction: a top-level (assert (or with no (and block raises inside the detector itself, and that exception travels the same route.

What the suite does not claim is that recognition is cheap or that the fast path is usually taken. Both are properties of the corpus, and the corpus is not part of the tool.

7.2 Performance Results

Per-property loading time is a property of the format rather than of this tool. Both binary backends skip tokenization and tree construction, so what remains is a file read and a tensor construction. The ratio that comes out of that depends on how expensive the text parser being compared against happens to be, and that denominator moves as soon as somebody writes a faster parser — which is a reason to hold on to the mechanism rather than to the multiplier.

7.3 Numerical Equivalence Validation

The benchmark suite converts each file twice, once with detect_fast_type=True and once with detect_fast_type=False, then compares the two output trees entry by entry: the input tensor with torch.equal, and every constraint row with np.array_equal. Exact equality, no tolerance, checked per file and per row rather than in aggregate — which is what makes a divergence reportable as a specific property instead of a percentage.

Conclusion

The bottleneck this tool removes was not the verification. It was that a workflow verifies one model against a thousand properties and re-parses all thousand of them on every run, while the model it loaded once was handled well the whole time. The large artefact was being treated as expensive and the small one as free.

Fixing it is a two-tier parse — exploit the structure when it is there, fall back to a general parser when it is not — behind a backend interface, with the conversion done once. The 90/10 rule is not a performance heuristic here; the 10% is what makes the 90% trustworthy. A matcher that guessed at unrecognised input would produce silently wrong constraints, and a parser that rejected what it did not recognise would fail on valid properties, so neither shortcut is available.

Worth saying what this does not argue. It does not argue that VNN-LIB should stop being text: a property written by a person and stored in a repository is better off human-editable, and that format is where specifications get written and reviewed. The argument is only that the same property should not be re-parsed on every one of a thousand runs, and conversion is how a reader gets both.

Repository: https://github.com/ZhongkuiMa/torchvnnlib

Related projects, which together make up a verification pipeline: SlimONNX optimises the model, ShapeONNX infers its shapes, TorchONNX compiles it to the program a verifier analyses, and TorchVNNLIB converts the properties it will be checked against.