Formalized Hopfield Networks and Boltzmann Machines
This work provides rigorous mathematical verification for neural network models, which is incremental but important for researchers in formal methods and theoretical machine learning.
The authors formalized Hopfield networks and Boltzmann machines in Lean 4, proving convergence for Hopfield networks with Hebbian learning on orthogonal patterns and ergodicity for Boltzmann machines using a new formalization of the Perron-Frobenius theorem.
Neural networks are widely used, yet their analysis and verification remain challenging. In this work, we present a Lean 4 formalization of neural networks, covering both deterministic and stochastic models. We first formalize Hopfield networks, recurrent networks that store patterns as stable states. We prove convergence and the correctness of Hebbian learning, a training rule that updates network parameters to encode patterns, here limited to the case of pairwise-orthogonal patterns. We then consider stochastic networks, where updates are probabilistic and convergence is to a stationary distribution. As a canonical example, we formalize the dynamics of Boltzmann machines and prove their ergodicity, showing convergence to a unique stationary distribution using a new formalization of the Perron-Frobenius theorem.