TorchVNNLIB: A Story of Fast VNN-LIB Property Loading

Introduction

I still remember the frustration of waiting for verification tools to load properties. Not the actual verification—that part was fine. The bottleneck was the property loading itself.

During my work on neural network verification for the VNN-COMP 2024 competition, I found myself running the same workflow hundreds of times: load a neural network model once, then verify it against hundreds or even thousands of different properties specified in VNN-LIB format. Each property file needed to be parsed from scratch, every single time. For benchmarks with many properties, the parsing overhead became significant.

This seemed backwards. The neural network model—a multi-megabyte ONNX file with thousands of operations—loaded quickly using binary formats. But the properties—simple text files specifying input bounds and output constraints—had to be parsed from scratch every time.

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

Something had to change. If we could convert VNN-LIB properties to binary format once and reuse them, we could eliminate this bottleneck entirely.

That’s what TorchVNNLIB does. It converts VNN-LIB specification files into binary formats (PyTorch .pth or NumPy .npz) that load 10-100x faster. Converting 100 ACAS Xu properties takes just 2-3 seconds, and subsequent loads are 10-100x faster than text parsing. 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 ~90% of real-world files with significantly faster processing.
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). The result? 100% success rate on VNN-COMP 2024 (1000+ properties across 23 benchmarks) with 10-100x faster loading times.

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 the abstraction layer
• Part 6: Code quality and usability—API design, error handling, testing
• Part 7: Real-world validation—VNN-COMP 2024 results (100% success rate)
• Part 8: Lessons learned—what worked, what didn’t, and why

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 has become the de facto standard 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

Here’s the typical verification workflow:

1. Load neural network model (ONNX file)—done once
2. Load property specification (VNN-LIB file)—done many times (100-1000+ properties per benchmark)
3. Run verification algorithm
4. Repeat steps 2-3 for each property

The asymmetry is striking: we load the model once but parse properties hundreds of times. And since verification tools typically parse VNN-LIB from scratch each time, the parsing overhead accumulates.

Binary formats solve this problem. TorchVNNLIB converts VNN-LIB text files into binary formats (PyTorch .pth or NumPy .npz) that load 10-100x faster than parsing text—a typical property that takes ~152ms to parse from text loads in just ~1.4ms from binary (100x speedup for PyTorch, ~70x for NumPy). For benchmarks with hundreds of properties, this difference becomes substantial—what once took minutes now takes seconds.

The speedup comes from eliminating the parsing overhead entirely. Binary formats store data in a structured, ready-to-use representation. No tokenization, no syntax tree construction, no semantic analysis—just deserialize and you’re done.

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 this. The data is already structured—just deserialize and you’re done.

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_bounds)
    output_matrix = torch.tensor(constraints.output_matrix)
    verify(model, input_bounds, output_matrix)

# Ideal workflow (fast)
for property_file in converted_properties:
    # Directly load PyTorch tensors
    data = torch.load(property_file)  # Fast!
    verify(model, data['input_bounds'], data['output_matrix'])

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: 10-100x faster loading through binary formats
2. Correctness: 100% success rate on VNN-COMP benchmarks
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 case (~58% of VNN-COMP 2024 properties). 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. Still common (~24% of files).

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 types cover ~97% of real-world VNN-LIB files. The remaining 3% use complex nested logic, non-standard operators, or unusual constraint forms.

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: Regex scanning is ~100x faster than full parsing. Even if we fail to detect the type, we’ve only wasted a few milliseconds.
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: 97% of files use the fast path (optimized processing), 3% use the AST fallback (still correct, just slower).

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), we use the (n_constraints, 1 + n_vars) matrix:

output_matrix = 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:

{
    'input_bounds': tensor([[lower_0, upper_0], ...]),  # (n_inputs, 2)
    'output_matrix': tensor([[b_0, a_00, a_01, ...], ...]),  # (n_constraints, 1+n_outputs)
    'n_inputs': int,
    'n_outputs': int,
}

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,
    }

    # Reverse scan - outputs typically at end, inputs at beginning
    for line in reversed(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 reverse scan? VNN-LIB files typically have input bounds first, output constraints last. By scanning in reverse, we find output patterns first—and for many types, seeing the output pattern is enough to classify the file.

3.2 Type Coverage in VNN-COMP 2024

Distribution of VNN-LIB types:

Type	Files	Processing Path	Coverage
Type 1	580	Fast (regex)	58%
Type 2	245	Fast (regex)	24%
Type 3	92	Fast (regex)	9%
Type 4	34	Fast (regex)	3%
Type 5	21	Fast (regex)	2%
Complex	28	AST fallback	3%
Total	1000	97% fast path	100%

Key observations:

1. High fast path coverage: 97% of files use optimized regex-based processing
2. AST fallback works: Remaining 3% handled correctly by general parser
3. No failures: 100% success rate across all file types

Part 4: AST-Based General Parser

The fast type detection system handles 97% of files. But what about the other 3%? 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

5.1 Why Two Backends?

Aspect	PyTorch Backend	NumPy Backend
File format	.pth (torch.save)	.npz (np.savez_compressed)
Dependencies	PyTorch (600+ MB install)	NumPy (15 MB install)
GPU support	Yes (.cuda())	No (CPU only)
File size	Uncompressed	Compressed (.savez_compressed)
Use cases	GPU verification tools	Lightweight deployments, CPU-only

5.2 Numerical Precision

Both backends use float64 by default to ensure numerical precision. Both backends produce bit-identical outputs, confirmed through exact-equality testing across 100+ test files.

Part 6: Code Quality and Usability

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_bounds']  # (n_inputs, 2)
output_matrix = data['output_matrix']  # (n_constraints, 1+n_outputs)

# NumPy backend
import numpy as np
data = np.load("output_dir/or_group_0/sub_prop_0.npz")
input_bounds = data['input_bounds']  # (n_inputs, 2)
output_matrix = data['output_matrix']  # (n_constraints, 1+n_outputs)

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

7.1 Conversion Success Rate

Result: 100% success rate across 1000+ properties from 23 VNN-COMP 2024 benchmarks.

• Fast processor: 972 properties (97%)
• AST fallback: 28 properties (3%)
• Failures: 0 properties (0%)

7.2 Performance Results

Format	Load Time (avg per property)	Speedup
VNN-LIB Text (baseline)	~152ms	1x
PyTorch .pth (binary)	~1.4ms	~100x faster
NumPy .npz (binary)	~2.1ms	~70x faster

7.3 Numerical Equivalence Validation

For files matching Types 1-5, fast processor outputs exactly match AST outputs (972 properties tested, 100% exact match with no tolerance).

Part 8: Lessons Learned

Lesson 1: The 90/10 Rule Works — But You Need the 10%. Optimize for the common case (fast path), but handle the general case correctly (AST fallback). Graceful degradation beats incomplete coverage.

Lesson 2: Backend Abstraction is Worth the Complexity. Abstraction cost is small (~100 lines), flexibility benefit is large.

Lesson 3: Fallback Paths Prevent Edge Case Failures. Fast path with AST fallback achieved 100% coverage with zero failures.

Lesson 4: Property Structure Drives Output Format. File structure should reflect data semantics.

Lesson 5: Verification Needs Binary Formats. Text is human-friendly, binary is machine-friendly. Convert once, load many times.

Conclusion and Future Directions

Where We Are Today

TorchVNNLIB is a production-ready tool for converting VNN-LIB properties to binary formats:

• 100% success rate on VNN-COMP 2024 (1000+ properties, 23 benchmarks)
• 10-100x faster loading than text parsing
• Dual backend support: PyTorch (GPU-ready) and NumPy (lightweight)
• Two-tier architecture: Fast path (optimized) + AST fallback (100% coverage)

Try It Yourself

Installation:

pip install torchvnnlib

Basic usage (PyTorch backend):

from torchvnnlib import TorchVNNLIB
import torch

# Convert VNN-LIB to PyTorch format
converter = TorchVNNLIB(output_format="torch")
converter.convert("property.vnnlib", "output_dir")

# Load converted property
data = torch.load("output_dir/or_group_0/sub_prop_0.pth")
input_bounds = data['input_bounds']  # (n_inputs, 2)
output_matrix = data['output_matrix']  # (n_constraints, 1+n_outputs)

# Use in verification
result = verify(model, input_bounds, output_matrix)

Basic usage (NumPy backend):

from torchvnnlib import TorchVNNLIB
import numpy as np

# Convert VNN-LIB to NumPy format
converter = TorchVNNLIB(output_format="numpy")
converter.convert("property.vnnlib", "output_dir")

# Load converted property
data = np.load("output_dir/or_group_0/sub_prop_0.npz")
input_bounds = data['input_bounds']  # (n_inputs, 2)
output_matrix = data['output_matrix']  # (n_constraints, 1+n_outputs)

# Use in verification
result = verify(model, input_bounds, output_matrix)

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

Related Projects

TorchVNNLIB is part of a broader ecosystem of neural network verification tools:

• SlimONNX: ONNX model optimizer and simplifier
• TorchONNX: ONNX to PyTorch compiler for verification
• ShapeONNX: Shape inference for ONNX models

Together, these tools form a complete verification pipeline: model optimization (SlimONNX) → model compilation (TorchONNX) → shape inference (ShapeONNX) → property conversion (TorchVNNLIB) → verification.

Final Thoughts

Verification workflows need fast property loading. Text parsing is convenient for humans but slow for machines. Binary formats bridge this gap—convert once, load many times.

TorchVNNLIB shows that performance optimization doesn’t require sacrificing correctness. The two-tier architecture (fast path + AST fallback) achieves both: optimized processing for common cases, 100% coverage for all cases.

If you’re building verification tools or running large-scale verification benchmarks, give TorchVNNLIB a try. It might save you minutes (or hours) of property loading time.