Hi, I'm Zhongkui Ma
Diving deep into my PhD journey at The University of Queensland.
News
Recent paper acceptances and publications
Our paper Re-Key-Free, Risky-Free: Adaptable Model Usage Control is accepted by Euro S&P'26. Congrats, Zihan!
Our paper Mitigating Gradient Inversion Risks in Language Models via Token Obfuscation is accepted by AsiaCCS'2026. Congrats, Xinguo!
Our paper Convex Hull Approximation for Activation Functions is accepted by OOPSLA'25 within SPLASH'25. Happy!
Our paper AI Model Modulation with Logits Redistribution is accepted by WWW'25. Congrats, Zihan!
Our paper Uncovering Gradient Inversion Risks in Practical Language Model Training is accepted by CCS'24. Congrats, Xinguo!
Our paper CORELOCKER: Neuron-level Usage Control is accepted by S&P'24. Congrats, Zihan! [Live Video]
Our paper [ReLU Hull Approximation](/projects/wralu) is accepted by POPL'24.
Guides & Tutorials
Comprehensive guides on neural network verification and recent blog posts
Recent Blogs
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.
Featured NNV Guides
Neural Network Decomposition: The Unary-Binary Framework
The foundational unary-binary operation decomposition that enables neural network verification, explaining why activation functions drive computational complexity.
Multi-Neuron Relaxation and PRIMA
Multi-neuron relaxation techniques including PRIMA, k-ReLU, and the convex barrier theorem for tighter neural network verification bounds beyond single-neuron methods.
Marabou and Reluplex: Extended Simplex for Verification
The Reluplex algorithm and Marabou verifier for complete neural network verification using extended simplex methods specialized for ReLU networks.
Open Source
Tools and libraries for neural network verification and ONNX workflows
Featured Verification Tools
Supporting Libraries
wraact
Python LibraryA unified Python library to approximate activation function hull with convex polytopes. Supports ReLU, Sigmoid, Tanh, and GeLU.
View on GitHubshapeonnx
ONNX ToolA tool to infer missing tensor shapes in ONNX models for inspection and downstream tooling.
View on GitHubslimonnx
ONNX ToolA tool to optimize and simplify your ONNX models by removing redundant operations.
View on GitHub