Blogs
Technical deep-dives into verification tools, ONNX infrastructure, and neural network research.
Data That Only One Model Can Read
Adversarial examples exploit what a model notices; non-transferable examples use what it does not. How data can remain useful to a designated model without being equally useful to other models.
What Makes a Hull Approximation Useful
Why exact local bounds can still lose joint information, and how the useful precision of an approximation depends on the property and the work needed to use it.
What Gradients and Embeddings Can Reveal
A comparison of reconstruction risks in collaborative training and vector retrieval, and what GRAB, GHOST, and SHAQ change.
Where Control Enters: Weights, Updates, Outputs, and Data
Four places to intervene in the use of models and data, and the different assumptions behind CoreLocker, AdaLoc, AIM, and non-transferable examples.
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
ONNX is already an explicit graph, so compiling it does not make it readable -- it makes it directly consumable by the PyTorch tooling that can analyze it. Why the compilation is worth doing, and what the intermediate representation is actually for.
TorchVNNLIB: A Story of Fast VNN-LIB Property Loading
How a VNN-LIB specification becomes ordered tensors and arrays that keep its logical grouping, so a benchmark with thousands of properties is not re-parsed on every run and a property file can be deserialised instead of parsed.
Activation Hulls: What Makes an Approximation Sound?
The containment contract behind activation-hull approximations, why a sampled hull is not enough, and how the maintained wraact library exposes constraints.
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.