Hi, I'm Zhongkui Ma
Diving deep into my PhD journey at The University of Queensland.
News
Latest updates and announcements
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!
I present our work Convex Hull Approximation for Activation Functions at OOPSLA'25 in Singapore (Thu 16 Oct 2025 16:00-16:15 at Orchid West of Marina Bay Sands Convention Centre).
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!
Prof. Bai and I have a tutorial on Robustness Verification of Neural Networks using WraLU at ADC'24 (Mon 16 Dec 2024, Gold Coast, Australia). The tutorial received the Distinguished Tutorial Speaker award.
Our paper Uncovering Gradient Inversion Risks in Practical Language Model Training is accepted by CCS'24. Congrats, Xinguo!
I gave a presentation on ReLU Hull Approximation at the workshop *Formal Methods in Australia and New Zealand* on 30 May 2024 at the University of Queensland, St Lucia.
I presented our work ReLU Hull Approximation at the FPBench community monthly meeting on 2 May 2024, 9:00-10:00 AM Pacific time.
Our paper CORELOCKER: Neuron-level Usage Control is accepted by S&P'24. Congrats, Zihan! [Live Video]
I present our work, ReLU Hull Approximation at POPL'24 in Kelvin Room of the Institution of Engineering and Technology (IET) at London, UK. [Live Video]
Our paper [ReLU Hull Approximation](/projects/wralu) is accepted by POPL'24.
I participate in ICFEM'23 at Brisbane, Australia. And I present our work, Formalizing Robustness Against Character-Level Perturbations for Neural Network Language Models and my doctoral symposium paper, Verifying Neural Networks by Approximating Convex Hulls.
Guides & Tutorials
Comprehensive guides on neural network verification and recent blog posts
Recent Blogs
PropDAG: A Template Framework for Bound Propagation on Neural Network DAGs
A reusable template framework for bound propagation on directed acyclic graphs, separating algorithm logic from graph traversal infrastructure.
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.
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