2022
Entered neural network verification
I began working on convex relaxation and bound propagation: how to replace nonlinear reachable sets with tractable enclosures without losing the behaviours that must be covered.
Research Journey
How one question about approximation quality became a three-work doctoral line.
Why approximation quality became the question
Neural network verification asks a bounded question: for a specified input set and property, can every possible network behaviour be accounted for? Testing samples behaviours; a verifier has to reason about the whole set.
Exact reasoning becomes difficult as networks grow, so practical verifiers use sound abstractions. The result can remain correct and still become inconclusive when an approximation discards too much information. That tension between soundness, tightness, and cost became the question behind my doctoral work.
Doctoral research arc
Two foundations, followed by three first-author works that move from local activation geometry to symbolic propagation.
2023
Started the PhD at UQ
The doctoral line narrowed to one recurring problem: retain more useful geometry or symbolic dependence while keeping the resulting verification problem controllable.
2024 · ReLU geometry
ReLU Hull Approximation
Published at POPL'24
Zhongkui Ma, Jiaying Li, Guangdong Bai
Reuse ReLU's own linear pieces to construct cheaper enclosing hull constraints without giving up soundness.
2025 · General activations
Convex Hull Approximation for Activation Functions
Accepted at 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.
2027 · Symbolic propagation
Local Nonlinear Substitution for Bounding Activation Functions
Accepted at ICSE'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.
What the line taught me
Soundness comes first
A tighter approximation is useful only if it still encloses every behaviour required by the specification. The containment argument is part of the method, not a post-hoc check.
Losses propagate through stacked layers
A locally valid relaxation can discard dependence that later layers could have used. Approximation quality therefore has to be judged through propagation, not only at one activation.
Structure needs a stopping rule
Keeping richer symbolic structure can improve a bound, but carrying it indefinitely makes the analysis itself grow out of control. The useful design point is often local and deliberately temporary.
Research practice
Software
Make the abstractions inspectable
The research is accompanied by implementations and small libraries for activation bounds, ONNX graphs, and VNN-LIB properties. They make the representations concrete enough to test, inspect, and reuse.
Research softwareWriting
Expose the reasoning, not another manuscript
Research notes explain the ideas and their limits without reproducing experimental sections. The NNV guide develops the surrounding verification concepts as a separate teaching sequence.
Read the notes and guideNow
Current stage
Preparing my PhD defence
I am consolidating the three-work verification line, maintaining the research software around it, and writing explanations that expose the ideas without turning the site into a second copy of the papers.