Hopfield Networks

Stream: general

[Matteo Cipollina]

Hi!

I'd like to share my repository NeuralNetworks, which formalizes Hopfield networks in Lean 4.

(J. Hopfield showed in 1982 that "Computational properties of use to biological organisms or to the construction of computers can emerge as collective properties of systems having a large number of simple equivalent components (or neurons)..." and won the 2024 Nobel prize in physics for this, jointly with G. Hinton).

https://github.com/or4nge19/NeuralNetworks

The core contribution is a collection of sorry-free proofs establishing fundamental properties of discrete deterministic symmetric Hopfield networks, specifically:

1. Monotonic energy decrease during network updates
2. Convergence to stable states under the assumptions of zero thresholds

The formalization introduces a framework with:

• A SpinState type for neural activation states
• HopfieldState configurations with associated energy functions
• Update sequences with well-founded termination arguments
• Proofs of fixed-point stability using energy Lyapunov functions

Here's a summary of key files and their status:
Sorry-Free Core Files:

• Hopfield/Basic.lean: Defines the fundamental structures (SpinState, HopfieldState, HopfieldNetwork) with metrics and operations
• Hopfield/Energy.lean: Proves energy monotonicity theorems for symmetric networks with zero thresholds
• Hopfield/Convergence.lean: Proves convergence to fixed points using well-founded induction on the energy function

• Hopfield/StochasticUpdate.lean: Provides the foundational stochastic update framework using probability mass functions (implementation is complete but not yet connected to convergence results)
  In-Progress Extensions:

• Hopfield/Biased.lean: Generalizes to non-zero thresholds (partially complete)

• Hopfield/Hebbian/*.lean: Implements Hebbian learning with pattern storage theorems (contains sorries for capacity bounds)
• Hopfield/Asymmetric.lean: Addresses asymmetric weight matrices with stability analysis
• ForMathlib/MetropolisHastings.lean: Generalizes sampling algorithms (contains sorries in measure-theoretic proofs)

While the energy functions and update sequences are currently noncomputable, I believe (hope?) they could be made computable with @Alex Meiburg 's ComputableReals library, enabling simulations within Lean .

To my knowledge, this represents the first formalization of Hopfield networks in a theorem prover. I'm drafting a manuscript on this work and would welcome critical feedback from the community. Contributions are most welcome, particularly in extending the formalization to broader neural network classes or making components executable.
Thanks to @Britt Anderson for sparking the idea (here: #general > Computational Neuroscience in Lean? ) and for encouragement during the development.

[Michail Karatarakis]

Interesting to see this! We have also formalized Hopfield networks with a different approach. Repo here: https://github.com/mkaratarakis/HopfieldNet. Happy to discuss further!

[Matteo Cipollina]

Same here! At a quick glance the two repos seems complementary which would be great, mine more abstract and yours showing a rich implementation of hebbian rule.

[Matteo Cipollina]

Here are a few impressions after going through the HopfieldNet repo.
It seems to complement well and that we have saved each other time in our next development steps: mine has an emphasis on building a strictly hopfield framework as powerful, flexible and mathlib integrated as possible and with an eye on mathematical 'depth' though not yet 'generality' (this allowed me to build more extensions like stochastic and not be constrained to the specific proofs chosen by a specific text), yours follows a cohesive and self-contained textbook implementation (but perhaps more constrained), where hopfield networks are restriction of general networks defined in terms of graphs. I have chosen to generalize towards category theory afterwards, as well as towards statistical mechanics (Isin spin glasses, etc), possibly contributing that t PhysLib.
In this view these definitely need to be unified. While merging would be the ultimate goal, for the time being, I will try to prove equivalence lemmas between the two. For possible proof of isomorphism, I need to work out an implementation of ComputableReals but still equivalence should be enough.

In short and with some simplifications how I see the integration is: "here is the Theory" (modular, felxible to adapt formalization of specific research level models)(my NeuralNetworks.Hopfield); "here is a self-contained and workable classic Hopfield model with full parameters to run (your HN); plus your NN as Core.lean file pointing towards Category Theory

[Alex Meiburg]

I'm happy to help if you want to use ComputableReals! but I will caution that I'm not sure they will do well for your purpose - and, I'm not sure exactly what your goal is.

Is your goal to make a Lean program that can train and run a Hopfield network? Because in that sense, proofs in Lean (the programming language) are "optional" in the end. More likely than not, using Mathlib's Real type will be the wrong choice, since you probably want some finite data representation of things, like rational numbers maybe.

If you want to accompany that with proofs, then you'll need to think about whether the update sequence is deterministic or random - and if it's random, then how you source the randomness (in a 'safe' provable way).

ComputableReal was designed for tasks of the form, "I want to prove such-and-such real inequality is true". I could forsee it being useful if you want to prove that some particular rational-number implementation correctly reflects a real-number theory, or if the definition of your system has reals really baked in. For instance, if you wanted to implement a Boltzmann machine, then you can't really avoid using Real.exp, which is inherently going to mean that you need to use reals.

Unless I'm mistaken, though, Hopfield networks can be nicely described entirely using rational numbers and rational arithmetic. If you have an eye towards producing an implementation, I might start by looking at whether you can change Real to Rat everywhere, and see if anything breaks.

[Matteo Cipollina]

Alex Meiburg ha scritto:

For instance, if you wanted to implement a Boltzmann machine, then you can't really avoid using Real.exp, which is inherently going to mean that you need to use reals.

Indeed this is the reason I'm hoping to make use of ComputableReals, to be able to formalize and somewhat at some point run also Boltzmann Machines (extending hopfield ones) and in general advanced stochastic models. From my side, I wanted to have a code framework which is as powerful as possible from the start so I need reals (Michail did differently). (you can see I have started a framework of implementation for stochastic update).

[Alex Meiburg]

Ah, I see it now, ok! Well then I think the biggest hurdle will be integrating a random number generator (I guess using docs#Random ) and then the whole run will be some monad, either over IO or at least over a RandomGen. And then you can prove that, assuming the random number generator is uniformly random and iid, this is all correct?

I actually don't see anything in Batteries/Mathlib about "correctness" of random number generators, which is kind of surprising - maybe that can be found in some other downstream crypto-oriented library though. (The crypto-lean4 library looks promising.)

I guess I could add a BoundedRandom Real based on splitting the random number generator, and then there would be a ComputableReal instance for such reals. And then values like Real.exp (Random.randReal ...)could be processed too. I don't know much about this API though.

[Alex Meiburg]

How much are you hoping that the randomness is provably correct? vs. just proving the theoretical properties of Hopfield networks, and just plugging in _some_ source of randomness?

[Mario Carneiro]

Are there any statements of correctness of random number generators that aren't either false or imply $P \ne NP$ if true? PRNGs are a myth AFAICT

[Alex Meiburg]

"Correctness" in the sense that "If the RandomGen instance produced iid uniformly random bits, then this function produces iid values from distribution f." Like, the docs#Random.instBoundedRandomFin appears to have no such guarantees proved anywhere -- I could easily make an instance that always returned the minimum value of the range, which would be a "bad" Random instance.

(The actual implementations in Init/Mathlib all appear 'correct' in this sense, but it's just not stated anywhere.)

[Alex Meiburg]

There is something sort of in this direction at https://github.com/dtumad/VCV-io/blob/62413c72b84b57f8c1332237c81bf99977dc8567/VCVio/OracleComp/DistSemantics/EvalDist.lean but that is mostly using the PMF API to describe crypto operations more "in theory", afaict.

[Alex Meiburg]

I just realized that essentially the same topic is underway at #general > Proving things about functions using a PRNG.

Someone there linked SampCert, which has exactly the kinds of proofs I was talking about: https://github.com/leanprover/SampCert/blob/main/SampCert/Samplers/Geometric/Properties.lean#L368

[Matteo Cipollina]

Thanks @Alex Meiburg ! The current (sorry-free but idle) extension in Hopfield.StochasticUpdate and the WIP ForMathlib.MetropolisHastings do not connect (yet) to a sample random generator.
neuronUpdatePMF in in Hopfield.StochasticUpdate constructs probability distributions over spin states using the Boltzmann distribution
In general, I believe developing a BoundedRandom ComputableReal instance to support the transcendental functions needed for Boltzmann machines could work here.
Interesting examples in the links, let's see if I can come up with a meaningful RandomMonad typeclass along the lines of what you suggest!

[Robert Joseph]

@Matteo Cipollina this is great work!