Transformers are Bayesian Networks
Gregory Coppola
cs.AI
Mar 17, 2026 · v1
TL;DR
Proves in Lean 4 that sigmoid transformers implement belief propagation, with exact-BP weight constructions, uniqueness, Turing completeness, and finiteness results, across named Lean repositories.
Abstract
Transformers are the dominant architecture in AI, yet why they work remains poorly understood. This paper offers a precise answer: a transformer is a Bayesian network. We establish this in five ways. First, we prove that every sigmoid transformer with any weights implements weighted loopy belief propagation on its implicit factor graph. One layer is one round of BP. This holds for any weights – trained, random, or constructed. Formally verified against standard mathematical axioms. Second, we give a constructive proof that a transformer can implement exact belief propagation on any declared knowledge base. On knowledge bases without circular dependencies this yields provably correct probability estimates at every node. Formally verified against standard mathematical axioms. Third, we prove uniqueness: a sigmoid transformer that produces exact posteriors necessarily has BP weights. There is no other path through the sigmoid architecture to exact posteriors. Formally verified against standard mathematical axioms. Fourth, we delineate the AND/OR boolean structure of the transformer layer: attention is AND, the FFN is OR, and their strict alternation is Pearl's gather/update algorithm exactly. Fifth, we confirm all formal results experimentally, corroborating the Bayesian network characterization in practice. We also establish the practical viability of loopy belief propagation despite the current lack of a theoretical convergence guarantee. We further prove that verifiable inference requires a finite concept space. Any finite verification procedure can distinguish at most finitely many concepts. Without grounding, correctness is not defined. Hallucination is not a bug that scaling can fix. It is the structural consequence of operating without concepts. Formally verified against standard mathematical axioms.
Problem
Why transformers work is poorly understood. The paper claims a precise characterization: a sigmoid transformer is a Bayesian network, with each layer performing one round of belief propagation.
Approach
Results are stated and machine-checked in Lean 4 repositories (e.g., sigmoid-transformer-lean, universal-lean, godel/*.lean). The first result shows that any sigmoid transformer implements weighted loopy BP on an implicit factor graph. Explicit weights are constructed and proven to implement exact BP on declared factor graphs, and a uniqueness result is proven. Further proofs cover Turing completeness via Boolean circuit simulation and the finiteness of distinguishable concepts under finite verification.
Results
Lean-verified theorems include transformer_implements_bp, transformer_exact_on_tree, every_sigmoid_transformer_is_bayesian_network, transformer_is_turing_complete, and finite_distinguishable_symbols. Experiments are reported to corroborate the formal results, including the practical viability of loopy BP.
