Ph.D. Student
Davis Automated Reasoning
Group
Department of Computer Science
University of California, Davis
Email: zhetao#ucdavis.edu | zhe#zhe-tao.com
I’m a Ph.D. student in the Davis Automated Reasoning Group at UC Davis, advised by Prof. Aditya V. Thakur. I’m interested in programming languages, automated reasoning and machine learning.
Provable Repair of Vision Transformers [ Paper |
BibTeX | GitHub ]
Stephanie Nawas, Zhe Tao, and Aditya V. Thakur
The 7th International Symposium on AI Verification (SAIV).
2024.
Architecture-Preserving Provable Repair of Deep Neural Networks.
[ Paper | BibTeX | GitHub | arXiv ]
Zhe Tao, Stephanie Nawas, Jacqueline Mitchell, and
Aditya V. Thakur
44th ACM SIGPLAN Conference on Programming Language Design and
Implementation (PLDI 2023). June 2023.
SyReNN: A Tool for Analyzing Deep Neural Networks. [ Paper | BibTeX | GitHub ]
Matthew Sotoudeh†,
Zhe Tao†,
and Aditya V. Thakur
International Journal on Software Tools for Technology Transfer
(STTT).
DICE*: A Formally Verified Implementation of DICE Measured Boot.
[ Paper
| BibTeX | GitHub ]
Zhe Tao, Aseem Rastogi, Naman Gupta, Kapil Vaswani, and
Aditya V. Thakur
30th USENIX Security Symposium (USENIX Security ’21). August
2021.
† Equal contribution.
Algorithms and Applications for Provable Repair of Deep Neural
Networks. (Co-host) [ Website
]
45th ACM SIGPLAN Conference on Programming Language Design and
Implementation (PLDI 2024). June 2024. Copenhagen,
Denmark.
Architecture-Preserving Provable Repair of Deep Neural Networks.
[ Website
]
44th ACM SIGPLAN Conference on Programming Language Design and
Implementation (PLDI 2023). June 2023. Orlando, Florida, United
States.
DICE*: A Formally Verified Implementation of DICE Measured
Boot. [ website
]
30th USENIX Security Symposium (USENIX Security ’21). August 2021.
(Virtual).
APRNN is the first architecture-preserving provable V-polytope repair tool for DNNs. APRNN supports fully-connected, convolutional, pooling and residual layers with activation functions that have some linear pieces. APRNN scales to large networks like ResNet152 and VGG19, achieves low drawdown and high generalization, and introduces no overhead.
SyReNN is a library for analyzing deep neural networks by enumerating the linear regions of piecewise-linear functions (e.g., ReLU).
DICE* is a formally verified DICE measured boot implementation in F*, which is proved to be functionally correct, memory-safe and resistant to timing- and cache-based side channels. A key component of DICE* is a verified certificate creation library for a fragment of X.509.