gaojie/worldmodel

Fork 0

Files

T

History

gaojie bb342fc492

Sync to site1 / sync (push) Has been cancelled

Details

docs(lean): 新增 HOWTO_PROOF.md — LeJEPA Lean4 证明过程完整指南

内容涵盖：
- 为什么用 Lean4 做数学证明（vs 传统证明）
- 项目结构与文件依赖关系
- axiom vs theorem 核心概念
- 5 个证明文件逐行走读（Hermite/Uniqueness/Approx/Dirichlet/Planning）
- 关键 Mathlib 定理对照表
- 常用证明策略速查表（linarith/nlinarith/ring/field_simp 等）
- 如何添加新定理的完整步骤
- 调试技巧与常见错误解决

2026-06-05 17:37:50 +08:00

achieve

Refactor code structure for improved readability and maintainability

2026-06-02 04:41:13 +08:00

LeJEPA

Add detailed lecture plan and summary for LeJEPA four theorems

2026-06-05 16:30:24 +08:00

lejepa-identifiability

docs(lean): 新增 HOWTO_PROOF.md — LeJEPA Lean4 证明过程完整指南

2026-06-05 17:37:50 +08:00

math

feat(JEPA/math): 新增专题 VII & VIII，更新 README 与项目分析

2026-06-05 17:06:09 +08:00

papers

Refactor code structure for improved readability and maintainability

2026-06-02 04:41:13 +08:00

README.md

Refactor code structure for improved readability and maintainability

2026-06-02 04:41:13 +08:00

README.md

LeJEPA 世界模型可识别性 — 综合笔记

本文档合并自 lejepa_world_model_notes.md（论文与代码深度笔记）和 lejepa_resources.md（资源汇总）。

论文： When Does LeJEPA Learn a World Model?

第一部分：论文阅读笔记

作者： David Klindt (CSHL)、Yann LeCun (NYU)、Randall Balestriero (Brown) 发表： arXiv:2605.26379v1 [stat.ML]，2026年5月25日 官网： https://klindtlab.github.io/lejepa-identifiability/（2026-05-27） 代码： JEPA/lejepa-identifiability/（已本地 clone） 原文： research/papers/2605.26379v1.pdf 视频： https://youtu.be/EioGDo67ZDs（官方演示，AI and the Brain 频道）

🎯 核心问题

LeJEPA 学到的表示，什么时候才算真正学到了世界模型（World Model）？

答案：当且仅当它能线性恢复世界的潜在变量（latent variables）时。

🧠 背景与动机

什么是 JEPA？

Joint-Embedding Predictive Architecture（JEPA）是 LeCun 提出的自监督学习框架：

训练编码器 f 对同一内容的两个视图产生相似的嵌入
用正则化器防止表示坍塌（collapse）

什么是 LeJEPA？

LeJEPA = JEPA + SIGReg（Sketched Isotropic Gaussian Regularization）：

对齐损失（Alignment）： 拉近正样本对的嵌入
高斯正则化（SIGReg）： 强制嵌入分布接近各向同性高斯分布 h(z) ~ N(0, I_n)

核心缺口

此前没有任何 JEPA 的可识别性（identifiability）理论——不知道学到的表示是否真正恢复了世界的潜在结构。

🌍 世界模型的数学框架

世界假设（三条）

假设	含义
独立性	潜变量各分量相互独立
平稳性	两个视图共享同一边际分布
加性噪声	`z'_i = m_i(z_i) + η_i`，噪声独立于状态

高斯世界（Gaussian World）

最大熵选择：z ~ N(0, I_n)，转移过程为 Ornstein-Uhlenbeck（OU）过程：

z' = ρz + √(1-ρ²) η,   η ~ N(0, I_n)

其中 ρ ∈ (0,1) 控制两个视图的相关性。

学习目标

min_h  E[‖h(z') - h(z)‖²]    (对齐损失)
s.t.   h(z) ~ N(0, I_n)       (高斯约束)

📐 四大定理

定理 1：LeJEPA 线性可识别性（正向）

在高斯世界中，满足 LeJEPA 目标的最优表示 h 当且仅当 h(z) = Qz，其中 Q ∈ O(n) 为正交矩阵。

证明核心思路（Hermite 多项式谱分解）：

任意函数 h_i(z) 可展开为 Hermite 多项式：h_i = Σ c_α H_α(z)
OU 转移对 d 阶 Hermite 分量的衰减因子为 ρ^d
由 Mehler 公式：E[h_i(z')h_i(z)] = Σ_d w_d · ρ^d ≤ ρ
等号成立 当且仅当 w_1 = 1（即 h_i 是线性的）
任何非线性扭曲都会严格降低正样本对的相关性

直觉： 高斯 OU 过程对高阶非线性成分的衰减更快，因此线性映射是唯一最优解。

定理 2：高斯分布的唯一性（逆向）

在满足世界假设的所有分布中，高斯分布是唯一使 LeJEPA 实现线性可识别性的分布。

证明思路（Sturm-Liouville 理论）：

若第一特征函数 φ_1 是仿射的（φ = az + b），则得分函数 (log p)' 必须是线性的
线性得分函数 → log p(z) ∝ -(z-μ)² → 高斯分布

意义： 这与经典 ICA 的结论完全相反——在线性 ICA 中，高斯分布是唯一失败的情况；在 LeJEPA 的非线性设置中，高斯分布是唯一成功的情况。

定理 3：近似可识别性

当对齐目标和白化约束只近似满足时，恢复误差优雅降级：

E[‖h(z) - Qz‖²] ≤ D + (ε + D)²

其中：

D = δ / (2ρ(1-ρ))：对齐间隙的归一化量
ε = ‖Cov(h(z)) - I‖_F：白化误差

实践含义： 对齐质量是可识别性的主要瓶颈，白化误差影响较小。

定理 4：最优潜空间规划

若 h(z) = Qz（正交），则在旋转不变代价函数下，潜空间中的规划与真实世界中的规划完全等价：

V̂*(h(z₀)) = V*(z₀)   且   â*_{1:T}(h(z₀)) = a*_{1:T}(z₀)

覆盖的控制问题：

目标到达（goal-reaching）
线性二次调节（LQR）
任何依赖旋转不变量的代价函数

🔬 实验验证

实验 1：正向可识别性（验证定理 1）

2D 设置，4种非线性混合函数（见 mixing.py）：
- spiral（螺旋，保测度旋转微分同胚 g(z) = R(π‖z‖)z）
- banana（香蕉/抛物线弯曲，x₁ = z₁ + z₀²）
- sinusoid（正弦剪切，x₀ = z₀ + sin(1.5 z₁)）
- nvp（RealNVP 风格耦合层，make_coupling_mixing，任意偶数维）
LeJEPA 在所有情况下恢复各向同性高斯结构（旋转等价）
扩展到 1024 维：SIGReg 和 VICReg 保持 R² > 0.999

实验 2：逆向验证（验证定理 2）

扫描广义正态分布族（形状参数 α）
R² 在 α=2（高斯） 时达到峰值，非高斯分布线性可识别性下降

实验 3：近似界验证（验证定理 3）

所有运行的实际恢复误差均低于理论界
对齐损失是可识别性的最强预测指标

实验 4：潜空间规划（验证定理 4）

DMC Reacher 环境（像素输入，2D 关节角度潜变量）
高斯编码器（OU 采样）：规划质量与 oracle 无统计显著差异
轨迹编码器（RL 策略采样，非高斯）：规划质量显著下降

🔑 关键洞见

1. 谱分解是核心工具

Hermite 多项式将任意函数分解为线性/非线性成分，OU 转移对高阶成分的衰减更强，这使得线性映射成为唯一最优解。

2. 数据分布决定可识别性

OU 采样（各向同性高斯） → 满足理论假设 → 高可识别性
RL 策略轨迹（非高斯、各向异性） → 违反假设 → 低可识别性

3. 探索策略的重要性

对于自监督预训练，近似各向同性随机游走的探索策略能保持数据在理论覆盖的范围内。

4. 三种方法的失效模式不同

方法	优势	失效场景
SIGReg	对非高斯潜变量更鲁棒	高维时正交误差略增
VICReg	与 SIGReg 性能相当	非高斯潜变量时下降更快
InfoNCE	低维时表现好	高维时核宽度不匹配导致梯度消失

🔧 形式化验证（Lean 4）

所有定理均在 Lean 4 定理证明器中形式化验证（零 sorry 义务），使用 Mathlib v4.28.0。

验证组件概览：

文件	内容	状态
`Hermite.lean`	定理 1（Hermite 多项式路径）	✅ 已验证
`Uniqueness.lean`	定理 2（高斯唯一性）	✅ 已验证
`Dirichlet.lean`	附录 E（Dirichlet 能量路径）	✅ 已验证
`Approx.lean`	定理 3（近似界）	✅ 已验证
`Planning.lean`	定理 4（规划等价）	✅ 已验证

📊 与慢特征分析（SFA）的关系

维度	Sprekeler et al. (2014)	本文
可识别性类	置换等价	正交等价
潜变量分布	任意独立	高斯（或 i.i.d.）
转移结构	需要不同速率	需要各向同性
提取方式	顺序（贪心）	同时
函数空间	固定多项式核	学习（神经网络）
近似界	无	`D + (ε+D)²`
实用算法	xSFA（脆弱，≤6个潜变量）	LeJEPA/SIGReg（可扩展）

💡 局限性与未来方向

潜变量是否真的是高斯的？ 宏观任务相关变量可能因中心极限定理趋向高斯，但无法从观测中验证。
维度不匹配问题（m ≠ n）： 编码器输出维度与真实潜变量维度不同时的行为尚未理论化。
有限样本与优化动态： 定理 3 是总体层面的结论，样本复杂度和训练动态未涉及。
动作条件转移的可识别性： 本文只处理编码器侧，动作条件转移 p̂(ẑ'|ẑ,a) 的可识别性是下一步工作（与因果表示学习相关）。

🏆 核心贡献总结

LeJEPA 将经典 ICA 的叙事完全颠倒： 在线性 ICA 中，高斯分布是源分离失败的唯一情况；在 LeJEPA 的非线性设置中，高斯分布恰恰是使线性可识别性成立的唯一分布。

五大贡献：

首个 JEPA 可识别性结果（定理 1）
高斯分布唯一性的逆向定理（定理 2）
量化近似可识别性界（定理 3）
各向同性转移是同时提取的必要条件（附录 F）
线性可识别性与最优潜空间规划的等价性（定理 4）

线性可识别性使学到的表示成为控制系统的可用状态，任何正交不变代价函数都可以直接在学到的潜空间中使用，无需修改——这是可证明地学到世界模型的含义。

📚 关键参考文献

LeJEPA： Balestriero & LeCun, arXiv:2511.08544, 2025
LeWorldModel： Maes et al., arXiv:2603.19312, 2026
V-JEPA 2： Assran et al., arXiv:2506.09985, 2025
VICReg： Bardes et al., arXiv:2105.04906, 2021
SFA 可识别性： Sprekeler et al., JMLR 15:921-947, 2014
Causal-JEPA： Nam et al., arXiv:2602.11389, 2026

第二部分：代码仓库深度解析

本部分基于本地 clone 的 JEPA/lejepa-identifiability/ 仓库，对核心实现进行逐模块分析。

仓库结构

lejepa-identifiability/
├── lean/                    # Lean 4 形式化证明
│   └── LeJEPA/
│       ├── Hermite.lean     # 定理1（Hermite 多项式路径）
│       ├── Uniqueness.lean  # 定理2（高斯唯一性，Sturm-Liouville）
│       ├── Approx.lean      # 定理3（近似可识别性界）
│       ├── Dirichlet.lean   # 附录E（Dirichlet 能量替代证明）
│       └── Planning.lean    # 定理4（规划等价）
└── experiments/
    ├── lejepa_id/
    │   ├── mixing.py        # 非线性混合（spiral/banana/sinusoid/coupling）
    │   ├── losses.py        # SIGReg、白化损失、对齐损失、InfoNCE
    │   ├── models.py        # MLP 编码器、MatchedEncoder、CNN 编码器
    │   ├── data.py          # 潜变量采样、OU 增强
    │   ├── metrics.py       # R²、正交误差、近似界量化、Procrustes
    │   ├── reacher.py       # DMC Reacher 渲染与数据集
    │   └── engine.py        # 训练循环（warmup + cosine LR）
    ├── run.py               # 2D/scaling/gennorm/grid 统一入口
    ├── run_reacher.py       # Reacher 像素观测入口
    ├── prerender.py         # 渲染 Reacher OU/轨迹帧
    ├── analysis/            # 后处理绘图与表格
    └── configs/             # 实验超参数 YAML

核心实现：损失函数（`losses.py`）

`SIGReg`（Sliced characteristic-function Isotropic Gaussian Regularizer）

代码 docstring 标注为 Sliced characteristic function regularizer（Balestriero & LeCun 2025）。

class SIGReg(nn.Module):
    def __init__(self, knots=17, n_slices=256, t_max=3.0):
        # 梯形积分节点 + 高斯加权
        t = torch.linspace(0, t_max, knots)
        dt = t_max / (knots - 1)
        w = torch.full((knots,), 2 * dt); w[[0, -1]] = dt   # 梯形权重
        self.phi = torch.exp(-t**2 / 2)                     # 标准高斯特征函数
        self.weights = w * torch.exp(-t**2 / 2)             # 积分权重×高斯加权

    def forward(self, h):
        # h: (V, B, N) -> scalar
        flat = h.flatten(0, 1)
        A = F.normalize(torch.randn(flat.size(-1), self.n_slices), dim=0)  # 随机切片方向
        xt = (flat @ A).unsqueeze(-1) * self.t
        err = (xt.cos().mean(0) - self.phi)**2 + xt.sin().mean(0)**2
        return (err @ self.weights).mean() * flat.size(0)

关键设计：

用特征函数（Fourier 变换）的实部/虚部偏差度量分布差异，而非矩匹配
随机切片（slicing）将高维问题降为一维投影，线性时间复杂度
knots=17 个积分节点，n_slices=256 个随机方向，t_max=3.0
积分权重 weights = 梯形权重 × exp(-t²/2)：对低频段加权更高，与高斯特征函数的衰减一致

`alignment_loss` 与 `whitening_loss`

def alignment_loss(h):
    """拉近正样本对。h: (V, B, N) -> scalar"""
    return (h.mean(0) - h).square().mean()

def whitening_loss(h):
    """||Cov(h) - I||²_F（VICReg 风格白化）"""
    cov = (flat.T @ flat) / (flat.shape[0] - 1)
    return (cov - torch.eye(...)).square().mean()

训练目标：

# LeJEPA 模式
loss = lamb * sig + (1 - lamb) * align

# VICReg 模式（对比用）
loss = lamb * wht + (1 - lamb) * align

# InfoNCE 模式（对比用）
loss = infonce_loss(h, sigma)

核心实现：非线性混合（`mixing.py`）

混合函数 g 将独立潜变量 z 映射到"观测"空间 x = g(z)，模拟世界的非线性渲染。编码器的任务是反转它（恢复到正交等价）。

def mix_spiral(z):
    """g(z) = R(π‖z‖) z —— 保测度螺旋微分同胚（旋转角随半径变化）"""

def mix_banana(z):
    """香蕉形：x₀ = z₀, x₁ = z₁ + z₀²"""

def mix_sinusoid(z):
    """正弦剪切：x₀ = z₀ + sin(1.5 z₁), x₁ = z₁"""

def make_coupling_mixing(N, n_layers=4, seed=1337):
    """RealNVP 风格耦合层，适用于任意偶数维 N（含 N=2 的 'nvp' 情形）
    交替更新：z2 += tanh(z1 @ W) / z1 += tanh(z2 @ W)，W 为正交矩阵×2"""

设计要点：

spiral 保测度 → 不改变体积，是对编码器最严苛的"扭曲"测试
banana/sinusoid 引入低阶多项式/三角非线性
coupling 提供可扩展到高维的可逆混合，与 MatchedEncoder 结构对偶

核心实现：数据生成（`data.py`）

`ou_augment`（OU 过程增强）

def ou_augment(z, rho, n_views=2, dist="gaussian", alpha=None):
    """z' = ρz + √(1-ρ²)η，η 与 z 同分布
    返回 (V, B, N) 形状的多视图张量"""
    fac = (1 - rho ** 2) ** 0.5
    eta = sample_latents(n_views * D, N, dist=dist, ...)
    return rho * z.unsqueeze(0) + fac * eta

支持的分布：

"gaussian"：标准正态（理论保证成立）
"laplace"：拉普拉斯（理论保证失效，用于消融）
"gennorm"：广义正态（扫描形状参数 α，验证定理2）

核心实现：评估指标（`metrics.py`）

`compute_all_metrics`

def compute_all_metrics(z, x, h, h_prime, rho, N):
    # 混合可逆性 R²（x↔z，作为上界参考）
    r2_zx, r2_xz = bidirectional_r2(z, x)
    # 双向 R²（z↔h，线性可识别性的主要指标）
    r2_zh, r2_hz = bidirectional_r2(z, h)

    # 正交误差（衡量 h = Qz 中 Q 的正交性）
    A = W[:N].T  # 线性回归系数
    orth_err = ||A^T A - I||_F
    orth_err_normalized = orth_err / √N   # 维度归一化，便于跨 N 比较

    # 近似界量化（验证定理3）
    delta = max(L_h - 2*(1-rho)*trace_cov, 0)
    D_bound = delta / (2*rho*(1-rho))          # spectral_gap = 2ρ(1-ρ)
    approx_bound = D_bound + (epsilon + D_bound)**2

    # Procrustes 距离（最优正交对齐后的误差）
    M = h^T z / n;  U, S, Vt = SVD(M);  Q = U @ Vt
    procrustes_mse = ||h - z @ Q^T||²

辅助函数： compute_recovery_metrics 用于 Reacher 等只需 R²(z↔h) + 正交误差的场景，支持 suffix 区分 OU/轨迹编码器的指标键名。

核心实现：编码器架构（`models.py`）

编码器	用途	结构
`make_mlp_encoder`	2D 实验	4层 MLP + GELU
`MatchedEncoder`	高维 Scaling	逆 NVP 耦合层（与混合函数匹配）
`make_cnn_encoder`	Reacher 像素	4层 CNN + BN + AvgPool + 线性头

MatchedEncoder 设计亮点：

与 RealNVP 混合函数结构对称（逆耦合层）
理论上能精确反转混合，验证可识别性上界
参数：z2 = z2 - tanh(z1 @ W)（逆向耦合）

核心实现：训练引擎（`engine.py`）

def train_and_evaluate(encoder, mix_fn, *, N, rho, lamb, mode="lejepa", steps=20000, ...):
    # LR 调度：前半段恒定，后半段 cosine 衰减
    # 在线数据生成（无需预存数据集）
    # 每 log_every 步在固定 eval 集上评估所有指标

训练流程：

采样潜变量 z ~ N(0, I_N)（或 laplace/gennorm，用于消融）
OU 增强得到正样本对 (z, z')
混合函数 g 映射到观测空间 (x, x') = (g(z), g(z'))
编码器 h 映射到嵌入空间
按 mode 计算损失：
- lejepa：L = λ·SIGReg + (1-λ)·Alignment
- whiten（VICReg 风格对照）：L = λ·Whitening + (1-λ)·Alignment
- infonce：L = InfoNCE(h, σ)
AdamW 优化（lr=3e-3，warmup 占前半段，后半段 cosine 衰减）
每 log_every 步在固定 z_eval 集上评估全部指标

核心实现：Reacher 像素数据（`reacher.py`）

验证定理4的物理控制实验，基于 DeepMind Control Suite 的 reacher / hard 任务，通过 MuJoCo（EGL 后端）渲染 64×64 像素帧。

函数	作用
`render_at`	设定关节角 `qpos` 与目标位置，渲染单帧 `(3,64,64)`
`generate_ou_image_pairs`	用 OU 过程采样关节角对 `(z_t, z_{t+1})` 并渲染为图像对
`solve_ik_grid`	200×200 网格搜索逆运动学，定位指尖到目标的关节角
`ReacherOUDataset`	预渲染 OU 图像对 + 真值潜变量（2D 关节角）的数据集

关键点： 潜变量是 2D 关节角，像素是高度非线性的"渲染混合"。OU 编码器恢复正交等价关节角 → 规划等价；RL 轨迹编码器因数据非各向同性而失效。

第三部分：Lean 4 形式化证明深度解析

定理1证明链（`Hermite.lean`）

核心数据结构：

structure SpectralWeights where
  w : ℕ → ℝ          -- Hermite 展开系数
  nonneg : ∀ d, 0 ≤ w d
  zero_degree : w 0 = 0   -- 零均值约束
  total_variance : ∑' d, w d = 1  -- 单位方差

7步验证链：

步骤	定理/引理	状态
1	`mehler_summability`：Mehler 公式可求和性	公理化
2	`correlation_le_rho`：相关性 ≤ ρ	✅ 已验证
3	`loss_lower_bound`：损失 ≥ 2(1-ρ)n	✅ 已验证
4	最优性 → 每个 corr_i = ρ（`Finset.sum_lt_sum`）	✅ 已验证
5	`equality_forces_degree_one`：corr_i = ρ → w₁ = 1	✅ 已验证
6	`linear_of_degree_one`：w₁ = 1 → h 线性	公理化
7	`orthogonal_of_gaussian_linear`：线性 + 高斯 → 正交	公理化

关键引理（已验证）：

-- ρᵈ < ρ 对 d ≥ 2 严格成立（非线性成分被严格惩罚）
theorem pow_lt_self_of_ge_two (ρ : ℝ) (hρ0 : 0 < ρ) (hρ1 : ρ < 1)
    (d : ℕ) (hd : 2 ≤ d) : ρ ^ d < ρ

-- 等号成立 ⟺ 所有 d ≥ 2 的权重为零（即 h 是线性的）
theorem equality_forces_degree_one ...
    (heq : ∑' d, sw.w d * ρ ^ d = ρ) :
    ∀ d, 2 ≤ d → sw.w d = 0

定理2证明链（`Uniqueness.lean`）

Sturm-Liouville 框架：

structure LatentComponent where
  K : ℝ          -- 扩散系数（K > 0）
  score : ℝ → ℝ  -- (log p)'，得分函数
  ev : ℝ         -- 第一非常数特征值 λ₁（ev > 0）

核心代数步骤（已验证）：

-- K·score(z)·a = −ev·(az + b)，a ≠ 0
-- ⟹ score(z) = (−ev/K)z + (−ev·b/(Ka))，斜率 < 0
theorem score_affine_of_eigenfunction ...
    ⟹ ∃ α β, α < 0 ∧ score z = α * z + β

双条件定理（已验证）：

theorem gaussian_uniqueness (lc : LatentComponent) :
    (IsGaussianScore → ∃ 仿射特征函数)  -- if 方向
    ∧
    (∀ 仿射特征函数 → IsGaussianScore)  -- only-if 方向

定理3证明链（`Approx.lean`，Proposition 4.3）

核心装配定理（已验证）：

theorem approximate_identifiability
    (ρ δ ε W_nl M_Q_norm total_error : ℝ) ...
    (hgap : δ ≥ 2 * ρ * (1 - ρ) * W_nl)        -- 谱间隙控制非线性能量
    (hpolar : M_Q_norm ≤ ε + W_nl)             -- 极分解界
    (hpythag : total_error = M_Q_norm ^ 2 + W_nl) :  -- 勾股分解
    total_error ≤ δ / (2*ρ*(1-ρ)) + (ε + δ/(2*ρ*(1-ρ))) ^ 2

验证状态表：

组件	状态
谱间隙正性 `2ρ(1-ρ) > 0`	✅ 已验证
非线性能量界 `W_nl ≤ D`	✅ 已验证
极分解 `‖M−Q‖ ≤ ε+W_nl`	公理化
跨阶 Hermite 正交性	公理化
线性偏差平方界	✅ 已验证
勾股分解	公理化
单调性 `(ε+t)²+t` 递增	✅ 已验证
完整界装配	✅ 已验证
精确恢复 `δ=ε=0 ⟹ 误差=0`（退化为定理1）	✅ 已验证

附加结论（已验证）： bound_small_perturbation——当 ε+D ≤ 1 时，二次项可被一阶项控制，界简化为 ≤ 2D + ε。

定理4证明链（`Planning.lean`，Corollary）

控制问题结构：

structure ControlProblem (n : ℕ) (Action : Type*) where
  stage_cost : Latent n → Action → ℝ
  terminal_cost : Latent n → ℝ

-- O(n) 不变性：ℓ(Qz, a) = ℓ(z, a)
def IsOrthogonalInvariant cp Q : Prop :=
  (∀ z a, cp.stage_cost (Q z) a = cp.stage_cost z a) ∧
  (∀ z, cp.terminal_cost (Q z) = cp.terminal_cost z)

规划等价定理（已验证）：

-- 对任意动作序列，推前动力学下的总代价 = 原始动力学下的总代价
theorem planning_equivalence ... :
    totalCost cp E_hat a (Q z) = totalCost cp E a z

-- 最优动作序列在两个空间中完全相同
theorem minimizer_equivalence ... :
    (∀ a', cost_hat a (Q z) ≤ cost_hat a' (Q z)) ↔
    (∀ a', cost a z ≤ cost a' z)

第四部分：官方网站图示与实验结果

🖼️ 官方网站图示解读

来源：https://klindtlab.github.io/lejepa-identifiability/（2026-05-27）

核心图示（三面板）

[左] 世界的潜变量          [中] 非线性混合           [右] LeJEPA 恢复
  z ~ N(0, I_n)    →→→   x = g(z)（未知）   →→→   h(x) = Qz（正交）
  独立高斯分量              螺旋/香蕉/剪切等           旋转等价恢复

TL;DR（官网原文）：

LeJEPA linearly recovers the world's latent variables — up to rotation — if and only if those latents are Gaussian. The forward direction is a spectral argument on Hermite polynomials; the converse rules out every non-Gaussian alternative. All proofs are checked in Lean 4.

实验图示解读

图(a)：近似界验证（定理3）

横轴：理论界 D + (ε+D)²
纵轴：实际恢复误差
所有运行点均在对角线下方（界成立）

图(b)：高斯唯一性（定理2）

横轴：广义正态形状参数 α（α=2 为高斯）
纵轴：线性可识别性 R²
R² 在 α=2 处尖锐达到峰值，两侧均下降

图(c)：控制代价（定理4）

高斯-OU 编码器：与 oracle 统计上无显著差异
轨迹编码器：代价显著偏高

图(d)：代价随 R² 单调下降

线性可识别性越高 → 规划代价越低
支持定理4的连续性推论

Reacher 规划演示

[顶行] Oracle（关节空间直线）：平滑弧线轨迹
[中行] 高斯-OU 编码器：紧密跟随 oracle
[底行] RL 轨迹编码器：明显偏离（不可识别）

解码方式：在潜空间中线性插值，用最近邻检索解码到像素帧。

📊 完整实验结果表（官网版）

N	混合 R²(x→z)	SIGReg R²(h→z)	VICReg R²(h→z)	InfoNCE R²(h→z)
2	0.781±2.1e-3	0.999998±3.4e-7	0.999996±8.4e-7	0.950961±1.6e-3
4	0.727±24e-3	0.999996±12e-7	0.999987±54e-7	0.910871±8.2e-3
8	0.728±10e-3	0.999993±9.0e-7	0.999988±4.8e-7	0.886818±42e-3
16	0.734±6.3e-3	0.999988±4.9e-7	0.999987±4.6e-7	0.999880±0.01e-3
32	0.737±2.3e-3	0.999981±7.2e-7	0.999981±9.4e-7	0.907809±26e-3
64	0.737±1.5e-3	0.999966±7.4e-7	0.999968±8.1e-7	0.648496±3.1e-3
128	0.739±0.61e-3	0.999938±3.2e-7	0.999942±7.2e-7	0.566955±6.6e-3
256	0.742±0.49e-3	0.999884±7.9e-7	0.999889±7.2e-7	0.696587±0.49e-3
512	0.749±0.30e-3	0.999775±6.7e-7	0.999785±6.9e-7	0.704393±0.26e-3
1024	0.763±0.17e-3	0.999561±12e-7	0.999582±11e-7	0.720241±0.20e-3

5 个随机种子的均值±标准差。SIGReg 和 VICReg 在所有维度保持 R² > 0.999；InfoNCE 在高维（N ≥ 64）因固定核宽度退化。

第五部分：资源汇总

通过互联网搜索整理，收录时间：2026-06-01

🎬 视频资源

官方演示视频

标题	链接	频道	时间	说明
world model video（官方）	https://youtu.be/EioGDo67ZDs	AI and the Brain	2026-05-09	论文官方配套视频，291次观看，由作者团队发布

📌 该视频由 GitHub README 直接链接，是论文的官方配套演示视频。

📄 论文资源

核心论文

论文	arXiv	发表时间	说明
When Does LeJEPA Learn a World Model?	2605.26379	2026-05-25	本文，可识别性理论
LeJEPA: Provable and Scalable Self-Supervised Learning Without the Heuristics	2511.08544	2025-11-11	LeJEPA 原始论文，提出 SIGReg
LeWorldModel: Stable End-to-End JEPA from Pixels	2603.19312	2026-03-13	LeJEPA 扩展到动作条件控制
V-JEPA 2: Self-Supervised Video Models	2506.09985	2025	Meta 的视频 JEPA，理解/预测/规划
Causal-JEPA	2602.11389	2026	通过对象级干预学习世界模型

LeJEPA 原始论文摘要（arXiv:2511.08544）

Learning manipulable representations of the world and its dynamics is central to AI. Joint-Embedding Predictive Architectures (JEPAs) offer a promising blueprint, but lack of practical guidance and theory has led to ad-hoc R&D. We present a comprehensive theory of JEPAs and instantiate it in LeJEPA, a lean, scalable, and theoretically grounded training objective.

核心贡献：

识别各向同性高斯分布为 JEPA 嵌入的最优分布

提出 SIGReg（Sketched Isotropic Gaussian Regularization）

单一超参数、线性时间/内存复杂度、无启发式技巧

~50 行代码实现，ViT-H/14 在 ImageNet-1k 达到 79%

LeWorldModel 摘要（arXiv:2603.19312）

LeWorldModel (LeWM) 是首个仅用两个损失项（下一嵌入预测 + 高斯正则化）从原始像素端到端稳定训练的 JEPA。

亮点：

~15M 参数，单 GPU 数小时可训

规划速度比基础模型快 48 倍

潜空间编码有意义的物理结构

可可靠检测物理上不合理的事件

🌐 官方网站与代码

项目主页

官方网站： https://klindtlab.github.io/lejepa-identifiability/
- 包含完整摘要、定理说明、实验结果图表
- 发布时间：2026-05-27

代码仓库

可识别性论文代码： https://github.com/klindtlab/lejepa-identifiability
- Lean 4 形式化证明（lean/ 目录）
- 实验代码（experiments/ 目录）
- 支持 2D、Scaling、Gennorm、Grid、Reacher 五类实验
LeJEPA 原始代码： https://github.com/rbalestr-lab/lejepa
- GitHub Stars: 1,170+
- 包含完整训练代码

交互演示

Google Colab Demo（~30秒，T4 GPU）： https://colab.research.google.com/drive/1ozjRk3FfUIDX7WBqlOKvhNcIamy0JxCH?usp=sharing

🤗 HuggingFace 资源

论文页面

可识别性论文： https://huggingface.co/papers/2605.26379
- AI 生成摘要：LeJEPA demonstrates linear identifiability of latent variables from nonlinear observations under Gaussian distributions, enabling reliable world modeling and planning.
LeJEPA 原始论文： https://huggingface.co/papers/2511.08544

模型	说明
gajeshladhar/core-jepa	图像特征提取，25次下载
falafel-hockey/lejepa-vit-small-patch8-256-sentinel2-5band	遥感图像（Sentinel-2）特征提取
adipanda/lejepa	LeJEPA 模型
caiovicentino1/lejepa-v1-tinyimagenet	TinyImageNet 训练版本

数据集	说明
falafel-hockey/sentinel2-lejepa-global-diverse-256	Sentinel-2 遥感数据，5k 样本

📚 相关背景论文

JEPA 系列

论文	说明
LeCun, A Path Towards Autonomous Machine Intelligence (2022)	JEPA 原始提案
I-JEPA (Assran et al., CVPR 2023)	图像 JEPA
V-JEPA (Bardes et al., 2024)	视频 JEPA
V-JEPA 2 (Assran et al., 2025)	视频理解/预测/规划

可识别性理论背景

论文	说明
Hyvärinen & Pajunen (1999)	非线性 ICA 不可识别性
Hyvärinen & Morioka (2016, 2017)	时间对比学习 + 非线性 ICA
Khemakhem et al. (2020)	VAE + 非线性 ICA 统一框架
Sprekeler et al. (2014)	SFA 非线性盲源分离理论
Sobal et al. (2022)	JEPA 关注慢特征

自监督学习对比

方法	论文	与 LeJEPA 关系
VICReg	Bardes et al. (2021)	二阶矩白化，理论上等价
InfoNCE	van den Oord et al. (2018)	隐式高斯化，高维退化
BYOL	Grill et al. (2020)	stop-gradient，无理论保证
SimSiam	Chen & He (2021)	stop-gradient，无理论保证
DINO/DINOv3	Caron et al. (2021) / 2025	自蒸馏 + 特征聚类

🔬 技术要点速查

LeJEPA 训练目标

L(h) = λ · L_SIG + (1-λ) · L_inv

L_inv = E[‖h(z') - h(z)‖²]          # 对齐损失（正样本对）
L_SIG = SIGReg(h(z), N(0,I))         # 高斯正则化（防坍塌）

SIGReg 实现原理

通过随机切片（sliced/sketching）将嵌入投影到 n_slices=256 个一维方向
在 knots=17 个积分节点上估计投影的特征函数（实部 cos + 虚部 sin）
与标准高斯特征函数 φ(t)=exp(-t²/2) 对比，按梯形权重×高斯权重加权积分
线性时间复杂度，~50 行代码（见 losses.py:SIGReg）

关键超参数

参数	推荐范围	说明
`λ`（正则化权重）	`1e-3` ~ `1e-2`	太大→坍塌，太小→不可识别
`ρ`（OU 相关性）	`0.8` ~ `0.95`	控制正样本对的相似度

实验结果摘要

维度 N	SIGReg R²	VICReg R²	InfoNCE R²
2	0.999998	0.999996	0.950961
64	0.999966	0.999968	0.648496
256	0.999884	0.999889	0.696587
1024	0.999561	0.999582	0.720241

📋 BibTeX 引用

@article{klindt2026lejepa,
  author    = {Klindt, David and LeCun, Yann and Balestriero, Randall},
  title     = {When Does LeJEPA Learn a World Model?},
  year      = {2026},
  journal   = {arXiv preprint arXiv:2605.26379},
}

@article{balestriero2025lejepa,
  author    = {Balestriero, Randall and LeCun, Yann},
  title     = {LeJEPA: Provable and Scalable Self-Supervised Learning Without the Heuristics},
  year      = {2025},
  journal   = {arXiv preprint arXiv:2511.08544},
}

@article{maes2026leworldmodel,
  author    = {Maes, Lucas and Le Lidec, Quentin and Scieur, Damien and LeCun, Yann and Balestriero, Randall},
  title     = {LeWorldModel: Stable End-to-End Joint-Embedding Predictive Architecture from Pixels},
  year      = {2026},
  journal   = {arXiv preprint arXiv:2603.19312},
}

🗺️ 资源地图

LeJEPA 生态系统
├── 理论基础
│   ├── arXiv:2511.08544 (LeJEPA 原始论文)
│   └── arXiv:2605.26379 (可识别性理论，本文)
├── 应用扩展
│   ├── arXiv:2603.19312 (LeWorldModel，像素控制)
│   └── arXiv:2602.11389 (Causal-JEPA，因果干预)
├── 代码
│   ├── github.com/rbalestr-lab/lejepa (LeJEPA 训练)
│   └── github.com/klindtlab/lejepa-identifiability (可识别性实验)
├── 演示
│   ├── YouTube: youtu.be/EioGDo67ZDs (官方视频)
│   ├── 官网: klindtlab.github.io/lejepa-identifiability
│   └── Colab: 交互式 2D 演示
└── 社区
    ├── HuggingFace: huggingface.co/papers/2605.26379
    └── HuggingFace: huggingface.co/papers/2511.08544 (1170+ Stars)

📖 相关文件

数学证明分解导航 — 6 个 topic 拆解四大定理
代码仓库 — 本地 clone 的官方实现
论文笔记原文｜资源汇总原文

README.md Unescape Escape

LeJEPA 世界模型可识别性 — 综合笔记

📑 目录

第一部分：论文阅读笔记

🎯 核心问题

🧠 背景与动机

什么是 JEPA？

什么是 LeJEPA？

核心缺口

🌍 世界模型的数学框架

世界假设（三条）

高斯世界（Gaussian World）

学习目标

📐 四大定理

定理 1：LeJEPA 线性可识别性（正向）

定理 2：高斯分布的唯一性（逆向）

定理 3：近似可识别性

定理 4：最优潜空间规划

🔬 实验验证

实验 1：正向可识别性（验证定理 1）

实验 2：逆向验证（验证定理 2）

实验 3：近似界验证（验证定理 3）

实验 4：潜空间规划（验证定理 4）

🔑 关键洞见

1. 谱分解是核心工具

2. 数据分布决定可识别性

3. 探索策略的重要性

4. 三种方法的失效模式不同

🔧 形式化验证（Lean 4）

📊 与慢特征分析（SFA）的关系

💡 局限性与未来方向

🏆 核心贡献总结

📚 关键参考文献

第二部分：代码仓库深度解析

仓库结构

核心实现：损失函数（losses.py）

SIGReg（Sliced characteristic-function Isotropic Gaussian Regularizer）

alignment_loss 与 whitening_loss

核心实现：非线性混合（mixing.py）

核心实现：数据生成（data.py）

ou_augment（OU 过程增强）

核心实现：评估指标（metrics.py）

compute_all_metrics

核心实现：编码器架构（models.py）

核心实现：训练引擎（engine.py）

核心实现：Reacher 像素数据（reacher.py）

第三部分：Lean 4 形式化证明深度解析

定理1证明链（Hermite.lean）

定理2证明链（Uniqueness.lean）

定理3证明链（Approx.lean，Proposition 4.3）

定理4证明链（Planning.lean，Corollary）

第四部分：官方网站图示与实验结果

🖼️ 官方网站图示解读

核心图示（三面板）

实验图示解读

Reacher 规划演示

📊 完整实验结果表（官网版）

第五部分：资源汇总

🎬 视频资源

官方演示视频

📄 论文资源

核心论文

LeJEPA 原始论文摘要（arXiv:2511.08544）

LeWorldModel 摘要（arXiv:2603.19312）

🌐 官方网站与代码

项目主页

代码仓库

交互演示

🤗 HuggingFace 资源

论文页面

相关模型（基于 LeJEPA 训练）

相关数据集

📚 相关背景论文

JEPA 系列

可识别性理论背景

自监督学习对比

🔬 技术要点速查

LeJEPA 训练目标

SIGReg 实现原理

关键超参数

README.md

核心实现：损失函数（`losses.py`）

`SIGReg`（Sliced characteristic-function Isotropic Gaussian Regularizer）

`alignment_loss` 与 `whitening_loss`

核心实现：非线性混合（`mixing.py`）

核心实现：数据生成（`data.py`）

`ou_augment`（OU 过程增强）

核心实现：评估指标（`metrics.py`）

`compute_all_metrics`

核心实现：编码器架构（`models.py`）

核心实现：训练引擎（`engine.py`）

核心实现：Reacher 像素数据（`reacher.py`）

定理1证明链（`Hermite.lean`）

定理2证明链（`Uniqueness.lean`）

定理3证明链（`Approx.lean`，Proposition 4.3）

定理4证明链（`Planning.lean`，Corollary）