神经网络已经成为现代人工智能的重要组成部分。尽管如此,它们通常都是黑盒,它们的行为可能出人意料,并产生出人意料的错误结果,比如对抗性的例子。在本教程中,我们将介绍神经网络验证问题,其目的是正式保证神经网络的特性,如鲁棒性、安全性和正确性。我们的教程涵盖了验证问题的理论基础和最先进算法的介绍。此外,我们还将为用户友好的神经网络验证工具箱提供实践编码教程,允许从业者轻松地将正式的验证技术应用到他们的定制应用中。
我们的教程包括在谷歌Colab中编码演示。我们将演示通用的auto_LiRPA库和获奖的α,β-CROWN验证器的使用。