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

我们的教程包括在谷歌Colab中编码演示。我们将演示通用的auto_LiRPA库和获奖的α，β-CROWN验证器的使用。