WraLUPOPL'24
ReLU Hull Approximation
Approximate ReLU hulls by reusing their linear pieces and constructing enclosing upper faces, rather than building the exact hull.
PhD Student · Trustworthy AI Research
Hi, I'm Zhongkui Ma
Diving deep into my PhD journey at The University of Queensland.
I study how formal methods and convex approximation can provide sound guarantees for neural networks.
Selected research
Two results in convex approximation for neural network verification.
WraActOOPSLA'25
Convex Hull Approximation for Activation Functions
Use double-linear-piece functions to simplify local activation geometry and construct convex over-approximations beyond ReLU.
The rest of the work covers model usage control and privacy in language models. See all publications.
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.
Research software
Supporting tools for working with models and specifications.
Inspect & simplify models
Connect model & specification formats
- torchonnx
A tool for converting ONNX models to PyTorch models (`.pth` for parameters, `.py` for structure).
- torchvnnlib
A tool to convert VNN-LIB files (`.vnnlib`) to PyTorch tensors (`.pth` files) for efficient neural network verification.
For the activation-hull construction behind WraAct, there is the wraact Python library.
News
Acceptances, awards and releases.
📄
Sept. 2026Paper Accepted
Our paper Catch-Only-One: Non-Transferable Examples for Model-Specific Authorization is accepted by NeurIPS'26 as an oral presentation (112 of 30709 submissions, about 0.36%). Congrats, Zihan, Ethan and Zhongkui!
🏆
Aug. 2026Best Paper Award
Our paper Non-Transferable Examples receives the Best Paper Award - Runner Up at the ECCV'26 LifeGenIP Workshop. Congrats, Zihan!
📄
Mar. 2026Paper Accepted
Our paper Re-Key-Free, Risky-Free: Adaptable Model Usage Control is accepted by Euro S&P'26. Congrats, Zihan!
6 earlier entries
📄
Nov. 2025Paper Accepted
Our paper Mitigating Gradient Inversion Risks in Language Models via Token Obfuscation is accepted by Asia CCS'2026. Congrats, Xinguo!
📄
Aug. 2025Paper Accepted
Our paper Convex Hull Approximation for Activation Functions is accepted by OOPSLA'25 within SPLASH'25. Happy!
📄
Jan. 2025Paper Accepted
Our paper AI Model Modulation with Logits Redistribution is accepted by WWW'25. Congrats, Zihan!
📄
Aug. 2024Paper Accepted
Our paper Uncovering Gradient Inversion Risks in Practical Language Model Training is accepted by CCS'24. Congrats, Xinguo!
📄
Apr. 2024Paper Accepted
Our paper CORELOCKER: Neuron-level Usage Control is accepted by S&P'24. Congrats, Zihan! [Live Video]
📄
Nov. 2023Paper Accepted
Our paper ReLU Hull Approximation is accepted by POPL'24.
Writing
Notes on the tools behind the work.
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.
January 2026SlimONNX: 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.
January 2026