神经网络动力学的计算机验证：首个案例研究

当前大量机器学习方法依赖于深度神经网络。然而，将神经网络视为非线性动力系统，很快就会发现，用数学严格地证明网络中节点生成的某些模式是极其困难的。事实上，在复杂系统的非线性动力学中，众所周知，即使在低维模型中，基于纸笔方法的分析技术也常常达到其极限。在这项工作中，我们通过非线性动力学的验证数值方法范式提出了一个完全不同的视角。其思想是使用计算机辅助证明来数学验证神经网络中非线性模式的存在性。作为一个案例研究，我们考虑了一类循环神经网络，我们通过计算机辅助证明了数百个Hopf分岔点的存在性及其非退化性，从而也证明了数百个周期轨道的存在性。我们的范式能够严格验证神经网络的复杂非线性行为，这为通过计算机辅助证明解释机器学习方法的全部能力以及潜在敏感性迈出了第一步。我们展示了验证数值技术如何揭示循环神经网络(RNN)的内部工作机制。为此，Hopf分岔的证明是通过证明各种设置下周期轨道的存在性，将动力系统理论整合到RNN实际应用中的第一步。