Writing
A guide to neural network verification, and notes on the tools built alongside it.
NNV Guide · A series in progress
A Guide to Neural Network Verification
Understand what a verifier proves, how bounds and relaxations work, and where their guarantees end.
29 guides · 4 parts · Foundations to advanced topics
- 01
Foundations
7What a verifier is asked to prove, and what its answer means.
- 02
Methods & Tools
10How bounds, relaxations and solver pipelines turn that question into constraints.
- 03
Practice
6Specifications, benchmarks, and the testing that complements a proof.
- 04
Advanced Topics
6Where verification gets expensive, and which architectures and defenses answer it.
Notes
Standalone write-ups, newest first. Each one is readable on its own.
ShapeONNX: Solving ONNX's Dynamic Shape Problem
A dual-track shape inference tool that resolves ONNX's dynamic shapes to concrete static values for neural network verification workflows.
SlimONNX: A Story of Optimizing Neural Networks for Verification
A pure Python toolkit for optimizing ONNX models specifically for verification workflows, validated on the VNN-COMP 2024 benchmark suites.
TorchONNX: A Compiler for ONNX-to-PyTorch Conversion
A pure Python compiler that converts ONNX models to native PyTorch code through a 6-stage pipeline, achieving 100% success on VNN-COMP 2024 benchmarks.
TorchVNNLIB: A Story of Fast VNN-LIB Property Loading
A tool for converting VNN-LIB verification properties to binary formats, achieving 10-100x faster loading with a two-tier processing architecture.
Wraact: Polytope Approximation for Sound Neural Network Verification
A unified framework for tight convex hull approximation of neural network activation functions, supporting 7 core activation types with sub-millisecond performance.
Why Reusing ReLU's Own Pieces Makes Hull Approximation Cheap
Over-approximating the ReLU convex hull is expensive because the hull is hard to describe. Reusing the function's own linear pieces as the lower faces turns the construction into bookkeeping over edges and vertices.
Every post is also listed on the blogs index, which is what the search index points at.