Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalized Hopfield Networks and Boltzmann Machines

Matteo Cipollina, Michail Karatarakis, Freek Wiedijk

TL;DR

This work formalizes both deterministic Hopfield networks and stochastic Boltzmann machines in Lean 4, establishing convergence, ergodicity, and learning properties within a unified graph-based framework. It develops a rigorous probabilistic foundation using Markov kernels, Gibbs sampling, and a novel formalization of the Perron–Frobenius theorem via a quiver-based irreducibility notion, enabling proofs of a unique stationary distribution for Boltzmann dynamics. Key contributions include formal proofs of Hopfield convergence under asynchronous updates, Hebbian learning for both single and orthogonal multi-pattern storage, and integration with PhysLean to connect neural dynamics to canonical ensembles. The approach emphasizes global dynamic properties of recurrent models over step-by-step computation, offering a robust, verifiable bridge between statistical mechanics, machine learning, and formal mathematics with clear paths for future MCMC and PF enhancements. This formalization advances the reliability and verifiability of neural-network theories by embedding them in a rigorous, library-wide Lean environment.

Abstract

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.

Formalized Hopfield Networks and Boltzmann Machines

TL;DR

This work formalizes both deterministic Hopfield networks and stochastic Boltzmann machines in Lean 4, establishing convergence, ergodicity, and learning properties within a unified graph-based framework. It develops a rigorous probabilistic foundation using Markov kernels, Gibbs sampling, and a novel formalization of the Perron–Frobenius theorem via a quiver-based irreducibility notion, enabling proofs of a unique stationary distribution for Boltzmann dynamics. Key contributions include formal proofs of Hopfield convergence under asynchronous updates, Hebbian learning for both single and orthogonal multi-pattern storage, and integration with PhysLean to connect neural dynamics to canonical ensembles. The approach emphasizes global dynamic properties of recurrent models over step-by-step computation, offering a robust, verifiable bridge between statistical mechanics, machine learning, and formal mathematics with clear paths for future MCMC and PF enhancements. This formalization advances the reliability and verifiability of neural-network theories by embedding them in a rigorous, library-wide Lean environment.

Abstract

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.

Paper Structure

This paper contains 26 sections, 2 theorems, 31 equations.

Table of Contents

  1. Introduction
  2. General Neural Networks
  3. Definitions
  4. Two-state networks
  5. Operation of neural networks
  6. Computations carried out by a general neural network
  7. Hopfield networks
  8. Description of a Hopfield Network
  9. Hopfield networks converge
  10. Hopfield Networks as Associative Memory
  11. The Hebbian learning rule
  12. Hebbian learning computations
  13. Stochastic neural networks
  14. Probability theory
  15. Markov kernels
  16. ...and 11 more sections

Key Result

Theorem 3.1

If the activations of the neurons of a Hopfield network are updated asynchronously, a stable state is reached in a finite number of steps. If the neurons are traversed in an arbitrary, but fixed cyclic fashion, at most $n\cdot2^n$ steps (updates of individual neurons) are needed, where $n$ is the nu

Theorems & Definitions (4)

  • Theorem 3.1: Convergence Theorem for Hopfield networks (Theorem 8.1, comp)
  • Remark 1: On orthogonality
  • Definition 2
  • Theorem 3