My research covers the verification, security, and privacy of AI systems. Neural network verification and convex approximation are the central themes of my PhD; alongside them I work with collaborators on model and data control, and on privacy in learning and retrieval. These are different questions answered with different forms of evidence, from sound verification bounds to experiments under stated threat models, and the page below keeps them apart rather than presenting one method applied three times.
Every work below is coauthored, and each theme says which papers it leads with. Every work links to its paper and, where one exists, to the original implementation.
What can be proved about a neural network over a specified set of inputs?
These three share a progression rather than a single method. WraLU exploits ReLU's piecewise-linear structure to approximate the shape that bounds have to contain. WraAct extends the study past ReLU to other activation functions, so the approach is not tied to one architecture. PdD sits at the specification level: what a sound bound has to mean for a program to be verified is a separate question from how the bound is built, and it is a separate kind of artifact from a hull approximation.
PhD focus
POPL'24
Zhongkui Ma, Jiaying Li, Guangdong Bai
Proposes WraLU, which over-approximates the ReLU convex hull by reusing the function's own linear pieces, reporting large speedups and fewer constraints on the evaluated benchmarks.
OOPSLA'25
Zhongkui Ma, Zihan Wang, Guangdong Bai
Proposes WraAct, constructing tight over-approximations of activation function hulls efficiently, and evaluates it on Sigmoid, Tanh and MaxPool.
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.
Once a model or its data has been released, how can its capability and their utility still be constrained?
Four points of control, not four 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 approach the same goal from the data side, 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
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.
WWW'25
Zihan Wang, Zhongkui Ma, Xinguo Feng, Zhiyang Mei, Zhiyong Ma, Derui Wang, Jason Xue, Guangdong Bai
Proposes AIM, redistributing logits so one trained model can serve several stakeholder-specific behaviours without retraining per user.
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.
NeurIPS'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.
What information escapes through gradients and embeddings, and how much of it can be taken back?
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
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.
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.
arXiv: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.
Supporting tools for working with models and specifications.
A tool for converting ONNX models to PyTorch models (`.pth` for parameters, `.py` for structure).
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.