【开放新书】可验证深度学习，91页pdf阐述Deep Learning的鲁棒性，提升安全可靠性

深度学习已经改变了我们思考软件的方式和功能。但深层神经网络是脆弱的，它们的行为常常令人惊讶。在许多情况下，我们需要对神经网络的安全性、正确性或健壮性提供保证。这本正在进行的书涵盖了基本的想法，从正式的验证和他们的应用到有关深度学习的推理。值得跟随

我相信深度学习将会持续下去，而我们仅仅触及了神经网络的皮毛。软件1.0(即手工编写的代码)和软件2.0(学习神经网络)之间的界限越来越模糊，神经网络正在参与对安全至关重要、对安全至关重要和对社会至关重要的任务。例如，医疗、自动驾驶汽车、恶意软件检测等。但神经网络是脆弱的，因此我们需要证明，当应用于关键场合时，它们表现良好。在过去的几十年里，形式方法社区开发了大量的技术来自动证明程序的属性，当然，神经网络就是程序。因此，将验证思想移植到软件2.0设置中是一个很好的机会。这本书提供了第一次介绍的基本思想，从自动验证应用到深度神经网络和深度学习。我希望能够激励验证研究者去探索深度学习的正确性，并鼓励深度学习研究者采用验证技术。

内容：

第1部分将神经网络定义为操作符在重值输入上的数据流图。这个公式将作为本书其余部分的基础。此外，我们将调查一些神经网络需要的正确性属性，并将它们放在一个正式的框架中。

I Neural networks and correctness

• A new beginning
• Semantics of neural networks
• Correctness properties

第2部分讨论了基于约束的验证技术。顾名思义，我们构造一个约束系统，并对其进行求解，以证明(或反证明)神经网络满足某些性质。

II Constraint-based verification

• Decidable theories of first-order logic
• Encoding neural networks logically
• Decision procedures
• Specialized decision procedures

第3部分讨论了基于抽象的验证技术。我们不需要在单个输入上执行神经网络，而是可以在无限集上执行它，并证明所有这些输入都满足理想的正确性属性。

III Abstraction-based verification

• Abstraction for neural networks
• Relational abstract domains
• Training with abstract values

第4部分最后，我们将讨论验证技术在深度强化学习任务中的应用，其中神经网络被用作动力系统的控制器。

IV Verification and reinforcement learning

• Neural networks as policies
• Verifying RL policies
• Efficient neural policy verification
• Enforcing properties in RL