ReLU geometry
ReLU Hull Approximation
POPL'24
Zhongkui Ma, Jiaying Li, Guangdong Bai
Reuse ReLU's own linear pieces to construct cheaper enclosing hull constraints without giving up soundness.
Research
I develop sound abstractions for neural network verification, and collaborate on model and data control and on privacy in learning and retrieval.
The verification line is my doctoral research. The other two lines are collaborative, and every work credits its complete author list.
Neural Network Verification
The doctoral line follows one question through three levels of the verifier: the local geometry of ReLU, a construction for general activation functions, and the symbolic information carried through back-substitution. PdD is related verification work at the specification level rather than a fourth step in that approximation sequence.
PhD focus
Read across this line
- What Makes a Hull Approximation Useful
- Why Linear Bounds Lose Cancellation When They Are Summed
- Why Nonlinear Substitution Has to Stay Local
- Activation Hulls: What Makes an Approximation Sound?
- 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
- Why Reusing ReLU's Own Pieces Makes Hull Approximation Cheap
General activations
Convex Hull Approximation for Activation Functions
OOPSLA'25
Zhongkui Ma, Zihan Wang, Guangdong Bai
Move beyond ReLU by simplifying local activation geometry with double-linear-piece functions and then enclosing it.
Symbolic propagation
Local Nonlinear Substitution for Bounding Activation Functions
AcceptedICSE'27
Zhongkui Ma, Mengdie Huang, Zihan Wang, Elisa Bertino, Guangdong Bai
Preserve nonlinear cancellation during one local back-substitution step, then return to linear form before polynomial degree grows across the network.
Additional verification work
Formalizing Robustness Against Character-Level Perturbations for Neural Network Language Models
ICFEM'23
Zhongkui Ma, Xinguo Feng, Zihan Wang, Shuofeng Liu, Mengyao Ma, Hao Guan, Mark Huasong Meng
Defines a robustness specification for character-level perturbations of neural network language models, built on three metrics for generalizing text perturbations.
Model & Data Control
These approach the goal from different directions rather than as versions of one defence. CoreLocker and AdaLoc control model access and ask how that access survives an update to the model behind it. AIM modulates behaviour without retraining. Non-transferable examples move the intervention to the data, constraining what released data can still mean to a model that was never handed it. The questions are related; the mechanisms are not interchangeable, and they have not been evaluated as one combined system.
Collaborative
Read across this line
CoreLocker: Neuron-level Usage Control
S&P'24
Zihan Wang, Zhongkui Ma, Xinguo Feng, Ruoxi Sun, Hu Wang, Minhui Xue, Guangdong Bai
Proposes CoreLocker, which locks a model behind a small extracted subset of significant weights that acts as the access key.
AI Model Modulation with Logits Redistribution
WWW'25
Zihan Wang, Zhongkui Ma, Xinguo Feng, Zhiyang Mei, Zhiyong Ma, Derui Wang, Minhui Xue, Guangdong Bai
Proposes AIM, redistributing logits so one trained model can serve several stakeholder-specific behaviours without retraining per user.
Re-Key-Free, Risky-Free: Adaptable Model Usage Control
Euro S&P'26
Zihan Wang, Zhongkui Ma, Xinguo Feng, Chuan Yan, Dongge Liu, Ruoxi Sun, Derui Wang, Minhui Xue, Guangdong Bai
Proposes AdaLoc, which keeps key-based model usage control working as the model evolves instead of reissuing keys on every update.
Catch-Only-One: Non-Transferable Examples for Model-Specific Authorization
AcceptedNeurIPS'26
Zihan Wang, Zhiyong Ma, Zhongkui Ma, Shuofeng Liu, Akide Liu, Derui Wang, Minhui Xue, Guangdong Bai
Recoding data in model-specific low-sensitivity directions to preserve designated-model utility, and studying the degradation that comes with misalignment against that subspace.
Privacy in Learning & Retrieval
The shared question is what an intermediate representation gives away while still being useful. GRAB and GHOST work on language-model training, where the representation in question is a gradient: GRAB studies what can be recovered from it, GHOST obfuscates at the token level rather than the gradient level. SHAQ moves the same question to retrieval, where the exposed representation is a stored embedding instead. The threat models are specific to each setting and the results do not transfer between them.
Collaborative
Read across this line
Uncovering Gradient Inversion Risks in Practical Language Model Training
CCS'24
Xinguo Feng, Zhongkui Ma, Zihan Wang, Eu Joe Chegne, Mengyao Ma, Alsharif Abuadbba, Guangdong Bai
Presents GRAB, a gradient inversion attack for language models built on two alternating optimization processes, showing the threat survives realistic training setups.
Mitigating Gradient Inversion Risks in Language Models via Token Obfuscation
Asia CCS'26
Xinguo Feng, Zhongkui Ma, Zihan Wang, Alsharif Abuadbba, Guangdong Bai
Using token-level obfuscation to decouple gradient, embedding and token spaces, reducing gradient-based text reconstruction while preserving training utility in the evaluated settings.
Shadow Queries for Private Retrieval in Vector Databases
PreprintarXiv:2609.04767
Xinguo Feng, Zhongkui Ma, Zihan Wang, Chuan Yan, Guowei Yang, Alsharif Abuadbba, Guangdong Bai
Studying generated shadow-query embeddings as an alternative retrieval representation for reducing document reconstruction risks.
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.
The full bibliography, including the doctoral symposium paper and the earlier work, is on the publications page. Project write-ups are on the projects page.