An Introduction to Xequation

Van Chan Ngo · December 30, 2020

In this post, I am excited to introduce Xequation.


Generally, machine learning (ML) based applications are required to be generalized such that they can work correctly with unseen samples. However, ML algorithms, including highly trained and smooth neutral networks optimized for perception tasks, have been shown to lack robustness to small changes of inputs, known as perturbations. Xequation is a new framework for verifying the robustness of ML-based safety-critical applications. The analysis is fully automatic and derives the estimated probability of how robust a model is w.r.t perturbations, called statistical robustness.

The new technique combines the temporal logics with time bounds, a method for formalizing program specifications, with an adaptation of multi-level splitting, a method for estimating the probability of rare events to the statistical robustness. As a result, the framework provides a unifying formalization of the perturbation generation process and a definition of robustness from a formal methods perspective. An advantage of the technique is that it has an ability to scale to much larger ML models, e.g. deep neutral networks used in autonomous driving software stack, than formal methods approaches such as using an automated theorem prover. The effectiveness of the technique is demonstrated with a prototype implementation that is able to automatically verify on benchmark problems, while scaling to larger deep neutral networks. Experimental results indicate that the derived probability is reliable and accurate.

The objective of Xequation is to provide solutions and tool development for verifying the robustness and reliability from a formal methods perspective for machine learning (ML)-based safety-critical applications such as localization, perception, and planning modules in autnomous driving software stack