Location
MC 5501
Candidate
Shengbo (Joseph) Zou | Applied Mathematics, University of Waterloo
Title
Formal Verification of Robustness of Neural Networks: Applications in LLMs and PINNs
Abstract
We consider the verification of robustness of neural networks under two application scenarios. In the first case, we consider (transformer-based) large language models (LLMs), which have proven to excel at natural language processing tasks with varied input formats and languages, along with support for directed writing. However, LLMs suffer from hallucinations and sensitivity in the input data, which prohibit their wider adoption under compliance requirements. In the second case, we consider multi-layer-perceptron (MLP)-based physics-informed neural networks (PINNs), which has been widely adopted as an alternative of traditional numerical methods for solving partial differential equations (PDEs) when the data is scarce, noisy, or incomplete. However, since the correctness for the numerical solutions for PDEs generated by PINNs is typically verified with sampling-based empirical tests, they do not provide formal guarantees, e.g., on the worst-case residual error. In light of the issues in the two scenarios above, we propose to apply the branch-and-bound techniques on the nonlinear atomic operators in both scenarios to extend linear bound propagation methods such that: i) in case 1, the robustness of LLMs can be efficiently verified; ii) in case 2, the correctness and robustness for the numerical solutions for PDEs generated by PINNs can be efficiently verified.