Formalized Hopfield Networks and Boltzmann Machines

AI summary

Overview

Research area: Formal verification / proof assistants (Lean 4 and mathlib) applied to neural network theory, specifically energy-based recurrent models and their learning rules.

Technical level: Advanced. The paper assumes familiarity with Markov kernels, measure-theoretic probability, matrix spectral theory, and the Lean 4 proof assistant, though its stated findings (convergence, ergodicity, Hebbian learning) are conceptually accessible.

One-sentence scope: A Lean 4 formalization, comprising around 16,000 lines of new code, of deterministic Hopfield networks and stochastic Boltzmann machines — including their dynamics, learning rules, and a new formal proof of the Perron–Frobenius theorem.

What This Paper Is About

Neural networks are ubiquitous, but their analysis and verification remain difficult, and mainstream verification work targets feedforward networks with local robustness properties rather than recurrent networks with global convergence behavior. Recurrent, energy-based models demand a different class of theorems: that asynchronous updates terminate, that the induced Markov chain is ergodic, and that it converges to a unique stationary distribution. This paper closes that gap by machine-checking the dynamics and learning algorithms of Hopfield networks and Boltzmann machines in a proof assistant, so that the resulting theorems can serve as rigorous specifications.

Key Contributions

1. A unified framework for feedforward and recurrent networks. The authors define a general NeuralNetwork structure (Listing 1) and separate Params (Listing 2), built on mathlib's Quiver type. Feedforward networks arise as a special case (SequentialArch, Sequential.toNeuralNetwork). This component is 2,400 lines and uses Quiver, linear algebra, and analysis.

2. Formalized discrete symmetric Hopfield networks with convergence and Hebbian learning. This component is 2,000 lines and draws on mathlib's Matrix and Vector. Formalization surfaced an implicit fairness condition on the update order that is required for convergence but omitted from textbook statements.

3. Probabilistic infrastructure plus the first Lean 4 formalization of Perron–Frobenius. The probabilistic infrastructure (reversibility, invariance of Markov kernels, Gibbs sampling) is 1,700 lines; the Perron–Frobenius development for irreducible/stochastic matrices is 5,400 lines, proved via an analytic Collatz–Wielandt argument.

4. Formalized Boltzmann machines: convergence and learning. At 4,600 lines, this covers convergence to the Boltzmann distribution, single-pattern Boltzmann learning, and CD-k, bridging to Physlib's CanonicalEnsemble and Temperature.

The authors state that this is, to their knowledge, the first formalization of Hopfield networks and Boltzmann machines in any proof assistant, and the first formalization of the Perron–Frobenius theorem in Lean 4.

Main Findings

• Asynchronous Hopfield updates always converge: Theorem 0.3.1 (HopfieldNet_convergence_fair) states that under asynchronous updates a stable state is reached in a finite number of steps.

• An explicit step bound for cyclic updates: If neurons are traversed in an arbitrary but fixed cyclic fashion, at most n·2ⁿ steps (updates of individual neurons) are needed, where n is the number of neurons (HopfieldNet_convergence_cyclic).

• A "fairness" hypothesis that textbooks omit: Convergence requires that every neuron is eventually updated. The authors define fairness as: for all u and n, there exists m ≥ n such that useq m = u. Without this, an update schedule may permanently exclude a neuron that needs to change, so energy stops decreasing even though no stable state has been reached. A fixed cyclic order is proven fair via the lemma cycl_fair.

• Energy never increases and revisits are impossible: The energy function E = −½ Σ_{u≠v} w_{uv} act_u act_v + Σ_u θ_u act_u yields the difference ΔE = (act_u^(old) − act_u^(new))(net_u − θ_u), which is < 0 or ≤ 0 in the two cases considered. If energy strictly decreases, the old state cannot be revisited; if energy is unchanged, the number of +1 activations increases, so the old state likewise cannot be revisited (lemma energy_lt_zero_or_pluses_increase).

• Hebbian storage works cleanly only for orthogonal patterns: The Hebbian weight matrix is W = Σ_{i=1}^{m} pᵢpᵢᵀ − mI. For orthogonal patterns, Wpⱼ = (n − m)pⱼ; for non-orthogonal patterns, a disturbance term Σ_{i≠j} pᵢ(pᵢᵀpⱼ) appears, and as m grows and (n − m) shrinks, the network cannot achieve its theoretical storage capacity.

• Reversibility gives invariance for both single-site and random-scan kernels: A Markov kernel Kᵢ reversible with respect to π satisfies detailed balance, and reversibility implies invariance (IsReversible.invariant). If each single-site kernel is reversible, so is the random-scan kernel K_rand(x,A) = (1/n) Σᵢ Kᵢ(x,A).

• The Perron–Frobenius theorem (Theorem 0.4.1, pft_irreducible) delivers six properties for an n×n irreducible non-negative matrix T: a real eigenvalue r > 0; strictly positive left and right eigenvectors; r ≥ |λ| for any eigenvalue; uniqueness of the eigenvectors up to constant multiples; the comparison result that 0 ≤ B ≤ T with eigenvalue β gives |β| ≤ r, with |β| = r implying B = T; and simplicity of r as a root of the characteristic equation. For a column-stochastic matrix, r = 1.

• Aperiodicity is what turns invariance into ergodicity: If an irreducible matrix is aperiodic/primitive, r is the unique eigenvalue of maximum modulus (pft_primitive); if it is periodic with period d > 1, there are exactly d such eigenvalues. Irreducibility plus aperiodicity is the condition for convergence to a unique stationary distribution.

• The algebraic/combinatorial bridge: The function Matrix.toQuiver maps a matrix A to a quiver where an edge i → j exists iff A_{ij} > 0, and pow_apply_pos_iff_nonempty_path proves that a positive entry in Aᵏ is equivalent to the existence of a path of length k. This supports eigenvector_is_positive_of_irreducible.

• Boltzmann machines converge to the Boltzmann distribution: π(act) = (1/c) exp(−E(act)/kT), where c = Σ exp(−E(act)/T). The authors adopt the common machine-learning simplification of replacing kT with T, omitting Boltzmann's constant (given as approximately 1.38·10⁻²³ J/K).

• Framework sanity checks: In the three-neuron recurrent network of Fig. 2 (p. 42 of the textbook), one update order reaches a stable all-zero state while another oscillates indefinitely — behavior precluded in Hopfield networks, which always converge under asynchronous updates. HNtest.lean instantiates a four-neuron Hopfield network with two orthogonal patterns, stores them via Hebbian learning, and demonstrates convergence to a stable stored pattern.

• Most of the new definitions do not yield executable code: The components marked non-computable are the probabilistic infrastructure, Perron–Frobenius, and Boltzmann machines; the unified framework and Hopfield components are computable. The definitions in §0.4–§0.4.2 are noncomputable, relying on mathlib's nonconstructive reals.

Methodology in Plain English

The authors work in Lean 4, a proof assistant, using mathlib — its shared library of mathematics — as the foundation. They chose Lean 4 because mathlib offers a single unified hierarchy of probability, algebra, analysis, and topology that the proofs use together, and they follow mathlib's philosophy of maximal generality rather than ad hoc formalization.

The design of the network representation separates architecture (the graph structure) from parameters (weights, input vectors, thresholds). Rather than tracking adjacency proofs everywhere, the authors use a matrix w : Matrix U U R and adopt the convention that all weights for non-adjacent neurons are zero. They initially modeled networks with mathlib's Digraph, but the Perron–Frobenius proof forced a move to Quiver, a directed multigraph type where connections inhabit a Type rather than being propositions. The authors describe this adoption as discovered, not designed — it was needed for path manipulation in the Perron–Frobenius proof before proving to be the right abstraction for the whole framework.

The convergence proof for Hopfield networks uses a Lyapunov-style energy argument: define an energy function, show it never increases under a single-neuron update, show that when energy is unchanged the number of +1 activations strictly increases (so the previous state is never revisited), and conclude that finiteness of the state space forces arrival at a stable state — provided updates are fair.

The Perron–Frobenius development combines a combinatorial view (positive powers of a matrix correspond to paths in a quiver) with an analytic view (the Collatz–Wielandt characterization of the Perron root as a supremum of minima of ratio terms). The authors also bridge to Physlib, a mathlib-style physics library, and lay groundwork for Optlib, a library of first-order optimization and convergence theorems. Proofs use standard Lean and mathlib tactics and automation throughout, and the authors describe upstreaming status for each component: Physlib pull requests under review or in preparation, a mathlib pull request in preparation for Perron–Frobenius, a mathlib submission ongoing for the probabilistic infrastructure, and an Optlib submission in preparation.

Why This Matters

Impact on research. The paper addresses a gap: mainstream neural-network verification targets feedforward networks where the network is a fixed function and properties are local, typically robustness of a single input-output map on a bounded region. Formalization of recurrent networks and their learning algorithms themselves remained relatively unexplored. A machine-checked account of these dynamics gives a specification against which hardware and the algorithms running on it could be verified. The work also produced a reusable finding of independent interest — the fairness condition — and a general framework that treats feedforward and recurrent architectures uniformly.

Real-world applications (as identified in the paper):

• Quantum annealing: minimizing a Hopfield energy is, up to an affine change of variables, quadratic unconstrained binary optimization (QUBO), the native input format of quantum annealers.
• Analog neuromorphic hardware: the same energy descent is realized directly in such hardware, meaning optimization is carried out in the physical device rather than a general-purpose processor.
• Stochastic Ising machines: these realize Boltzmann sampling over discrete spin states.
• Neural network verification: the formalized theorems provide specifications that could underpin verification of the above hardware and the algorithms running on it.

Industry relevance. The paper notes that neural networks underpin most current practice in machine learning, and that the Nobel Prize in Physics was awarded in October 2024 to John Hopfield and Geoffrey Hinton for work on artificial neural networks whose mathematics comes directly from statistical mechanics. The connection between continuous Hopfield update rules and Transformer attention, shown by Ramsauer et al. in 2020, links this formalization work to the architecture behind modern large-scale models. The authors' contributions are also aimed at reusable, upstreamed library components rather than a standalone artifact.

Future Directions

• Upstreaming the components. The paper records a status for each component: Physlib pull requests under review for the unified framework and Hopfield networks, a mathlib pull request in preparation for Perron–Frobenius, ongoing mathlib work for the probabilistic infrastructure, and a Physlib pull request plus an Optlib submission in preparation for Boltzmann machines. Completing these is an explicit open thread.

• Extending the framework beyond the architectures covered. The authors note that Quiver provides the extensibility required to model complex neural architectures beyond those explored in this work.

• Building out Optlib. The Boltzmann component lays groundwork for a library of first-order optimization and convergence theorems, which the paper lists as a separate deliverable.

• Verifying hardware against the formalized specifications. The paper frames the machine-checked account of these dynamics as a specification against which quantum annealers, analog neuromorphic hardware, stochastic Ising machines, and the algorithms running on them could be verified — a verification step that is proposed rather than carried out here.

• Improving executability. Most definitions in §0.4–§0.4.2 are noncomputable and yield no executable code, leaving open the question of extracting runnable implementations.

Target Audience

This paper is most valuable to researchers working at the intersection of formal verification and machine learning — particularly those using Lean 4 and mathlib, and those interested in contributing to Physlib or Optlib. It also serves theorists interested in machine-checked statements of convergence and ergodicity for energy-based models, and hardware or quantum-computing researchers who need rigorous specifications for annealers and neuromorphic devices. Readers without a background in proof assistants or Markov chain theory will find the high-level results accessible but the formalization details difficult.

Authors’ abstract

Neural networks are widely used, yet their analysis and verification remain challenging. We present a Lean~4 formalization covering both deterministic and stochastic models. We first formalize Hopfield networks -- recurrent networks that store patterns as stable states -- and prove their convergence, and the correctness of Hebbian learning, the rule that updates parameters to encode patterns. We then turn to stochastic networks, whose probabilistic updates converge to a stationary distribution: we formalize the dynamics and learning of Boltzmann machines and prove their ergodicity -- convergence to a \emph{unique} stationary distribution -- via a new formalization of the Perron--Frobenius theorem.