gaojie
5de86388db
Sync to site1 / sync (push) Has been cancelled
- Created planning_explainer.html to demonstrate orthogonal invariance and optimal planning with interactive controls and visualizations. - Created spectral_explainer.html to illustrate spectral decomposition and linear identifiability, featuring adjustable spectral weights and real-time correlation calculations.
136 lines
5.4 KiB
Markdown
136 lines
5.4 KiB
Markdown
# LeJEPA 数学证明分解导航
|
||
|
||
> 本目录将论文 *When Does LeJEPA Learn a World Model?* 的数学证明拆分为 6 个独立 topic，每个 topic 专注一个概念，循序渐进。
|
||
>
|
||
> **建议阅读顺序：** Topic 1 → 2 → 3 → 4 → 5 → 6
|
||
>
|
||
> 🎬 **交互式动画：** 每个 topic 都配有可拖动参数的交互式可视化，见 [`animations/`](animations/README.md)。
|
||
|
||
---
|
||
|
||
## 📚 Topic 列表
|
||
|
||
| # | 文件 | 核心概念 | 对应定理 | 难度 |
|
||
|---|------|---------|---------|------|
|
||
| 1 | [Hermite 多项式](01_hermite_polynomials.md) | 高斯分布下的函数分解工具 | 定理1基础 | ⭐⭐ |
|
||
| 2 | [OU 过程与 Mehler 公式](02_ou_process_mehler.md) | 正样本对生成 + 高阶衰减 | 定理1基础 | ⭐⭐ |
|
||
| 3 | [谱分解与线性可识别性](03_spectral_identifiability.md) | 定理1完整证明 | **定理 1** | ⭐⭐⭐ |
|
||
| 4 | [Sturm-Liouville 与高斯唯一性](04_sturm_liouville_uniqueness.md) | 为什么只有高斯分布有效 | **定理 2** | ⭐⭐⭐ |
|
||
| 5 | [近似可识别性界](05_approximate_identifiability.md) | 误差如何优雅降级 | **定理 3** | ⭐⭐ |
|
||
| 6 | [正交不变性与最优规划](06_planning_equivalence.md) | 潜空间规划等价于真实规划 | **定理 4** | ⭐⭐ |
|
||
|
||
---
|
||
|
||
## 🗺️ 知识依赖图
|
||
|
||
```
|
||
Topic 1: Hermite 多项式
|
||
│
|
||
↓
|
||
Topic 2: OU 过程 + Mehler 公式
|
||
│
|
||
↓
|
||
Topic 3: 谱分解 → 线性可识别性（定理1）
|
||
│ │
|
||
↓ ↓
|
||
Topic 4: 高斯唯一性 Topic 5: 近似界 Topic 6: 最优规划
|
||
（定理2） （定理3） （定理4）
|
||
```
|
||
|
||
---
|
||
|
||
## 🎯 四大定理速查
|
||
|
||
### 定理 1：线性可识别性（正向）
|
||
> 高斯世界 + LeJEPA 最优 → `h(z) = Qz`（正交矩阵）
|
||
|
||
**核心工具：** Hermite 谱分解 + OU 衰减 + 最优性条件
|
||
|
||
### 定理 2：高斯唯一性（逆向）
|
||
> 高斯分布是**唯一**使线性可识别性成立的分布
|
||
|
||
**核心工具：** Sturm-Liouville 特征值理论 + 得分函数分析
|
||
|
||
### 定理 3：近似可识别性
|
||
> 条件近似满足时，误差 `≤ D + (ε+D)²`，其中 `D = δ/(2ρ(1-ρ))`
|
||
|
||
**核心工具：** 三角不等式 + Procrustes 分析
|
||
|
||
### 定理 4：最优潜空间规划
|
||
> 线性可识别性 → O(n)-不变代价函数下的规划完全等价
|
||
|
||
**核心工具：** 正交不变性 + 轨迹推前
|
||
|
||
---
|
||
|
||
## 🔑 关键公式速查
|
||
|
||
### LeJEPA 训练目标
|
||
```
|
||
L(h) = λ · L_SIG + (1-λ) · L_align
|
||
|
||
L_align = E[‖h(z') - h(z)‖²] # 对齐损失
|
||
L_SIG = SIGReg(h(z), N(0,I)) # 高斯正则化
|
||
```
|
||
|
||
### OU 过程（正样本对生成）
|
||
```
|
||
z' = ρz + √(1-ρ²) η, η ~ N(0, I_n), ρ ∈ (0,1)
|
||
```
|
||
|
||
### Mehler 公式（核心不等式）
|
||
```
|
||
E[h_i(z') · h_i(z)] = Σ_d w_{i,d} · ρᵈ ≤ ρ
|
||
等号 ⟺ w_{i,1} = 1（纯线性）
|
||
```
|
||
|
||
### 近似界
|
||
```
|
||
E[‖h(z) - Qz‖²] ≤ D + (ε + D)²
|
||
D = δ / (2ρ(1-ρ))
|
||
δ = L_align - 2(1-ρ)n（对齐间隙）
|
||
ε = ‖Cov(h(z)) - I‖_F（白化误差）
|
||
```
|
||
|
||
---
|
||
|
||
## 🔧 代码对应关系
|
||
|
||
| 数学概念 | 代码实现 |
|
||
|---------|---------|
|
||
| 非线性混合 `g`（spiral/banana/sinusoid/coupling） | [`mixing.py`](../lejepa-identifiability/experiments/lejepa_id/mixing.py) |
|
||
| SIGReg 正则化（切片特征函数） | [`losses.py:SIGReg`](../lejepa-identifiability/experiments/lejepa_id/losses.py) |
|
||
| 对齐损失 | [`losses.py:alignment_loss`](../lejepa-identifiability/experiments/lejepa_id/losses.py) |
|
||
| OU 增强 | [`data.py:ou_augment`](../lejepa-identifiability/experiments/lejepa_id/data.py) |
|
||
| R²、正交误差、近似界、Procrustes | [`metrics.py:compute_all_metrics`](../lejepa-identifiability/experiments/lejepa_id/metrics.py) |
|
||
| Reacher 像素渲染 / 数据集 | [`reacher.py`](../lejepa-identifiability/experiments/lejepa_id/reacher.py) |
|
||
| 训练循环（lejepa/whiten/infonce） | [`engine.py:train_and_evaluate`](../lejepa-identifiability/experiments/lejepa_id/engine.py) |
|
||
|
||
---
|
||
|
||
## 🔬 Lean 4 形式化验证对应
|
||
|
||
| 定理 | Lean 文件 | 验证状态 |
|
||
|------|----------|---------|
|
||
| 定理1 / Thm 4.1（Hermite 路径） | [`lean/LeJEPA/Hermite.lean`](../lejepa-identifiability/lean/LeJEPA/Hermite.lean) | ✅ 零 sorry |
|
||
| 定理2（高斯唯一性） | [`lean/LeJEPA/Uniqueness.lean`](../lejepa-identifiability/lean/LeJEPA/Uniqueness.lean) | ✅ 零 sorry |
|
||
| 定理3 / Prop 4.3（近似界） | [`lean/LeJEPA/Approx.lean`](../lejepa-identifiability/lean/LeJEPA/Approx.lean) | ✅ 零 sorry |
|
||
| 定理4 / Corollary（规划等价） | [`lean/LeJEPA/Planning.lean`](../lejepa-identifiability/lean/LeJEPA/Planning.lean) | ✅ 零 sorry |
|
||
| 附录E（Dirichlet 路径） | [`lean/LeJEPA/Dirichlet.lean`](../lejepa-identifiability/lean/LeJEPA/Dirichlet.lean) | ✅ 零 sorry |
|
||
|
||
> 注：Lean 工程使用 Mathlib v4.28.0，零 `sorry`；公理化组件为 Mathlib 尚未提供的标准结论（Hermite 多项式基础设施、Mazur–Ulam、等权 AM–GM 等）。
|
||
|
||
---
|
||
|
||
## 💡 核心洞见（一句话总结）
|
||
|
||
> **LeJEPA 将经典 ICA 的叙事完全颠倒：** 在线性 ICA 中，高斯分布是源分离**失败**的唯一情况；在 LeJEPA 的非线性设置中，高斯分布恰恰是使线性可识别性**成立**的唯一分布。
|
||
|
||
---
|
||
|
||
## 📖 相关文件
|
||
|
||
- [论文完整笔记](../lejepa_world_model_notes.md) — 综合分析（含代码实现、官网图示）
|
||
- [资源汇总](../lejepa_resources.md) — 视频、论文、代码、HuggingFace 模型
|
||
- [代码仓库](../lejepa-identifiability/) — 本地 clone 的官方实现
|