The SIGReg Objective as Variational Free Energy: A Theoretical Active-Inference Account of JEPA World Models
Fabio Arnez, Alexandra Gomez-Villa
cs.LG
Jul 15, 2026 · v1
cs.AI
TL;DR
The algebraic core of every theoretical result (Gaussian bridge, gap decomposition, correspondence theorem) is machine-verified in Lean 4.
Abstract
Joint-Embedding Predictive Architectures (JEPAs) are the dominant design for latent world models, yet they are usually justified by empirical performance rather than a normative principle. We show that the choice of anti-collapse regulariser determines whether a JEPA's training objective, a prediction loss plus a weighted embedding regulariser, is a valid Active Inference (AIF) variational free energy. We organise four non-contrastive regularisers (VICReg, LogDet, PairDist, and SIGReg) into an entropy-estimator hierarchy indexed by a prior-miscalibration gap, and show that the gap's sign, whether the estimator bounds the latent entropy from above or below, decides whether the AIF surprise bound survives: VICReg and LogDet are unsafe upper bounds, PairDist a safe lower bound, and SIGReg eliminates the gap. We then prove a correspondence theorem: under the standard constant-noise encoder model and successful SIGReg enforcement (isotropic-Gaussian embeddings), the gap vanishes, the objective becomes an exact information bottleneck, the surprise bound is preserved, and the latent goal cost becomes an exact proxy for AIF pragmatic value, whereas VICReg leaves an irreducible second-order anisotropy term. We extend the correspondence to multi-step expected free energy, ensemble epistemic value, and a learned-policy regime, and we identify the one AIF term no current JEPA world model computes: the state-epistemic value, a future-state coverage signal. The predictions differ in kind, not degree, and are stated here as theoretical consequences left for empirical test in separate work; full proofs are in Appendix A, and the algebraic core of every result is machine-verified in Lean 4 (Appendix D).
Problem
Joint-Embedding Predictive Architectures (JEPAs) for latent world models are justified empirically rather than by normative principle. It is unclear when a JEPA's training objective corresponds to a valid Active Inference variational free energy, which depends on the choice of anti-collapse regulariser.
Approach
Four non-contrastive regularisers (VICReg, LogDet, PairDist, SIGReg) are organised into an entropy-estimator hierarchy indexed by a prior-miscalibration gap. The sign of the gap determines whether the AIF surprise bound survives. A correspondence theorem identifies AIF quantities with JEPA counterparts under a constant-noise encoder model. The algebraic core of every result is machine-verified in Lean 4.
Results
Under successful SIGReg enforcement the gap vanishes, the objective becomes an exact information bottleneck, and the latent goal cost becomes an exact proxy for pragmatic value, whereas VICReg leaves an irreducible second-order anisotropy term. The state-epistemic value is identified as an AIF term absent from current JEPA world models.
| Result | Lean declaration | Status |
|---|
| Gaussian bridge; argmin equiv. | gaussKL_eq, gaussKL_le_iff | verified |
| Prop. 1 decomposition; Gap II ≤ 0 | gap_decomposition, gapII_nonpos | verified |
| Prop. 2 (bound type) | boundtype_* | verified |
| Prop. 3; isotropy maximises | sigreg_zero_gap, isotropy_maximises | verified |
| Prop. 5 (exact KL proxy) | pragmatic_exact | verified |
Lean-verified results