A large number of current machine learning methods rely upon deep neural networks. Yet, viewing neural networks as nonlinear dynamical systems, it becomes quickly apparent that mathematically rigorously establishing certain patterns generated by the nodes in the network is extremely difficult. Indeed, it is well-understood in the nonlinear dynamics of complex systems that, even in low-dimensional models, analytical techniques rooted in pencil-and-paper approaches frequently reach their limits. In this work, we propose a completely different perspective via the paradigm of validated numerical methods of nonlinear dynamics. The idea is to use computer-assisted proofs to validate mathematically the existence of nonlinear patterns in neural networks. As a case study, we consider a class of recurrent neural networks, where we prove via computer assistance the existence of several hundred Hopf bifurcation points, their non-degeneracy, and hence also the existence of several hundred periodic orbits. Our paradigm has the capability to rigorously verify complex nonlinear behaviour of neural networks, which provides a first step to explain the full abilities, as well as potential sensitivities, of machine learning methods via computer-assisted proofs. We showcase how validated numerical techniques can shed light on the internal working of recurrent neural networks (RNNs). For this, proofs of Hopf bifurcations are a first step towards an integration of dynamical system theory in practical application of RNNs, by proving the existence of periodic orbits in a variety of settings.

翻译：大量当前机器学习方法依赖于深度神经网络。然而，将神经网络视为非线性动力系统时，很快就会发现，以数学严格方式论证网络中节点生成的特定模式极其困难。事实上，复杂系统的非线性动力学领域早已认识到，即使是在低维模型中，基于纸笔方法的解析技术也常常达到其极限。在本文中，我们通过非线性动力学验证数值方法范式提出了一种完全不同的视角。其核心思想是利用计算机辅助证明来数学验证神经网络中非线性模式的存在性。作为案例研究，我们考虑一类循环神经网络，通过计算机辅助手段证明了数百个霍普夫分岔点的存在性及其非退化性，进而证明了数百个周期轨道的存在性。本范式能够严格验证神经网络的复杂非线性行为，这为通过计算机辅助证明解释机器学习方法的全部能力及潜在敏感性迈出了第一步。我们展示了验证数值技术如何揭示循环神经网络（RNN）的内部工作机制。为此，霍普夫分岔的证明通过在不同场景下证明周期轨道的存在性，成为将动力系统理论整合到循环神经网络实际应用中的第一步。