UC Berkeley EECS · Formal Methods · Intelligent Systems
Building autonomy
we can reason about.
I am Kevin Chiaming Chang, a Ph.D. candidate advised by Prof. Pierluigi Nuzzo. I develop formal and optimization-based methods that make learning-enabled controllers more verifiable, interpretable, and compositional.
Research agenda
From learned behavior to defensible guarantees
My research asks how we can retain the performance of modern learning systems while recovering the structure needed to analyze, verify, and safely compose them.
Interpretable controllers
Transform neural-network policies into compact decision-tree representations while preserving their input-output behavior.
Compositional verification
Use robustness contracts and assume-guarantee reasoning to separate component-level analysis from system-level safety.
Solver-backed design
Develop SMT- and MILP-based refinement methods that turn formal specifications into scalable design and verification workflows.
Selected work
A research thread from distillation to exact equivalence
Recent work develops a path from learned controllers to representations that are easier to inspect, deploy, and verify.
See all publicationsEquivalent and Compact Representations of Neural Network Controllers With Decision Trees
Exact neural-to-tree transformation with automatic pruning for more practical verification and deployment.
Passivity Tools for Hybrid Learning Rules in Large Populations
A systems-theoretic framework for studying stability under hybrid and discontinuous learning dynamics.
Across theory and practice
Formal reasoning at multiple scales
Contact
Let’s talk about trustworthy intelligent systems.
I welcome conversations about formal verification, learning-enabled autonomy, contract-based design, and research collaborations.