Skip to main content
Back to top
Ctrl
+
K
Zhongkui Ma - Personal Website
News
Contents:
Publications
Activities
My Research Journey
Projects
WraLU: Fast and Precise ReLU Hull Approximation
WraAct: Convex Hull Approximation for General Activation Functions
Blogs
2026 Blog Posts
PropDAG: A Template Framework for Bound Propagation on Neural Network DAGs
ShapeONNX: Solving ONNX’s Dynamic Shape Problem
SlimONNX: A Story of Optimizing Neural Networks for Verification
TorchONNX: A Compiler for ONNX-to-PyTorch Conversion
TorchVNNLIB: A Story of Fast VNN-LIB Property Loading
Wraact: Polytope Approximation for Sound Neural Network Verification
A Guide to NNV
Phase 1: Foundations & Problem Formulation
Why Neural Network Verification?
Learn NNV in 3 Minutes
Threat Models in Neural Network Verification
The Verification Problem: Mathematical Formulation
Soundness and Completeness
Verification Taxonomy: A Systematic View
Theoretical Barriers in Neural Network Verification
Phase 2: Core Verification Techniques
Neural Network Decomposition: The Unary-Binary Framework
Beyond ReLU: Modern Activation Functions
Bound Propagation Approaches
Linear Programming for Verification
Multi-Neuron Relaxation and PRIMA
SDP-Based Verification: Semi-Definite Programming for Tighter Bounds
Lipschitz Bounds and Curvature-Based Verification
SMT and MILP Solvers for Verification
Marabou and Reluplex: Extended Simplex for Verification
Branch-and-Bound Verification
Phase 3: Robust Training & Practical Implementation
Formal Specifications
Falsifiers and Verifiers
Verification Benchmarks
Robustness Testing Guide
Regularization-Based Robust Training
Certified Adversarial Training
Phase 4: Advanced Topics & Frontiers
Training Robust Networks
Certified Defenses and Randomized Smoothing
Verification Scalability
Beyond
\(\ell_p\)
: Alternative Threat Models
Verifying Diverse Architectures
Real-World Applications
Index