深度学习已经改变了我们思考软件的方式和功能。但深层神经网络是脆弱的,它们的行为常常令人惊讶。在许多情况下,我们需要对神经网络的安全性、正确性或健壮性提供保证。这本正在进行的书涵盖了基本的想法,从正式的验证和他们的应用到有关深度学习的推理。值得跟随
我相信深度学习将会持续下去,而我们仅仅触及了神经网络的皮毛。软件1.0(即手工编写的代码)和软件2.0(学习神经网络)之间的界限越来越模糊,神经网络正在参与对安全至关重要、对安全至关重要和对社会至关重要的任务。例如,医疗、自动驾驶汽车、恶意软件检测等。但神经网络是脆弱的,因此我们需要证明,当应用于关键场合时,它们表现良好。在过去的几十年里,形式方法社区开发了大量的技术来自动证明程序的属性,当然,神经网络就是程序。因此,将验证思想移植到软件2.0设置中是一个很好的机会。这本书提供了第一次介绍的基本思想,自动验证应用到深度神经网络和深度学习。我希望能够激励验证研究者去探索深度学习的正确性,并鼓励深度学习研究者采用验证技术。
地址:
https://verifieddeeplearning.com/
内容:
第1部分将神经网络定义为操作符在重值输入上的数据流图。这个公式将作为本书其余部分的基础。此外,我们将调查一些神经网络需要的正确性属性,并将它们放在一个正式的框架中。
A new beginning
Semantics of neural networks
Correctness properties
第2部分讨论了基于约束的验证技术。顾名思义,我们构造一个约束系统,并对其进行求解,以证明(或反证明)神经网络满足某些性质。
Decidable theories of first-order logic
Encoding neural networks logically
Decision procedures
Specialized decision procedures
第3部分讨论了基于抽象的验证技术。我们不需要在单个输入上执行神经网络,而是可以在无限集上执行它,并证明所有这些输入都满足理想的正确性属性。
Abstraction for neural networks
Relational abstract domains
Training with abstract values
第4部分最后,我们将讨论验证技术在深度强化学习任务中的应用,其中神经网络被用作动力系统的控制器。
Neural networks as policies
Verifying RL policies
Efficient neural policy verification
Enforcing properties in RL
专知便捷查看
便捷下载,请关注专知公众号(点击上方蓝色专知关注)
后台回复“VDL” 就可以获取《可验证深度学习91页pdf》专知下载链接