Perron--Frobenius theorem

Lean~4 中形式化的 Hopfield 网络和玻尔兹曼机

研究人员使用 Lean~4 证明助手形式化了 Hopfield 网络和玻尔兹曼机，解决了验证神经网络行为的挑战。该形式化包括证明 Hopfield 网络的收敛性和用于模式编码的赫布学习的正确性。此外，它还涵盖了玻尔兹曼机的动力学和学习，通过对 Perron--Frobenius 定理的新颖形式化证明了其遍历性，从而确保收敛到唯一的平稳分布。