### D4RT
+ https://d4rt-paper.github.io/
+ 一句话总结: 用一个Encoder得到视频的`Representation`, 再用轻量化的Decoder查询对应像素的3d位置，实现3维重建。
+ 
![](https://ys.al/static/img/84555fa9f2461ca70035b787c32876bb.image.webp)
+ 训练形式：
    + Encoder得到`Global Scene Representation`**F**
    + Decoder的Query使用$(u,v,t_{src},t_{tgt},t_{cam})$,对F进行查询
        + $(u,v,t_{src})$代表在$t_{src}$时刻的图像的$(u,v)$像素
        + $(t_{tgt},t_{cam})$代表希望查询这个像素的点在$t_{tgt}$时刻在$t_{cam}$相机坐标系下的点
    + 好处: 监督信号的提供较为容易，推理时可以平行推理
### VGGT
+ https://arxiv.org/abs/2503.11651
+ 一句话总结: 在加入`Camera Token`后用交替注意力得到表示，用不同的head解码`Camera Ex/Intrinics/point map/depth map..`
+ 
![](https://ys.al/static/img/599f8d74ba393abcf53cd4df264fae64.image.webp)
+ 训练形式：
    + Camera/Depth maps/Point maps都是稠密的，即一次forward全部算出来
    + Point Tracking得到的是feature,再用下游方法进行追踪。

3d重建论文阅读

# 课程信息:
+ [MIT课程](https://diffusion.csail.mit.edu/2025/index.html)
+ 我只上过微积分/概率论，希望能够以不那么数学的方式学懂




# Introduction
+ 为什么我们需要概率分布去建模图片生成? 
    + 对于同一个prompt, 可能合法的图片有很多，不能够单纯地区分正例负例
    + 和前一点类似，在数据集中，对于同一个prompt，有许多对应的图片，我们可以说，这些图片服从一个概率分布；由于这个概率和prompt相关，因此若想要生成的东西为$z$,prompt本身是$y$, 那么$z\sim p_{data}(·|y)$
    + 为了保证生成图片的多样性，我们可以从一个初始分布$p_{init}$出发,一步一步到达$p_{data}$,在实际操作中，我们从$x\sim p_{init}$中随机采样一个$x_0$, 每次对x的值进行变换再加上噪声，最终得到的$x_n$可能就符合$p_{data}$
+ 从$p_{init}$到$p_{data}$
    + 既然$x$是一个向量，那么不考虑随机噪声的情况下x变换的过程其实是在一个向量场中进行运动($\mu_t(x)$代表x这一点前进的方向)
    + 我们可以列出方程$dX_t=\mu_t(X_t)dt$建模这一个确定的过程
    + 在计算机模拟的时候我们可以用欧拉算法进行建模:
        + Set $t=0$
        + Set step size h=$\frac{1}{n}$
        + Set $X_0=x_0$
        + $\textbf{for}\ i=1,\dots,n-1\ \textbf{do}$
            + $X_{t+h}=X_t+h\mu_t(X_t)$
            + Update $t\leftarrow t+h$
        + $\textbf{end for}$
    + 现在我们希望这个变换不再是确定性的，而是在每次变换的时候也添加一定的噪声；而高斯分布是最常见的噪声，因此添加高斯噪声。布朗运动是高斯噪声对应的随机过程(神秘名词)，其满足性质
        + $W_t-W_s\sim N(0,(t-s)I_d)$ 也就是它是高斯噪声的叠加
        + 由于布朗运动实际上不可导，所以我们希望能用一个不依赖导数的方程去建模它:
        + $dX_t=\mu_t(X_t)dt+\sigma_tdW_t$(实际上不合法)对应的是$X_{t+h}=X_t+h\mu_t(X_t)+h(W_{t+h}-W_t)+hR(t)$&&$lim_{h\rightarrow0}E(R(t))=0$
    + 所以我们可以这样模拟:
        + Set $t=0$
        + Set step size h=$\frac{1}{n}$
        + Set $X_0=x_0$
        + $\textbf{for}\ i=1,\dots,n-1\ \textbf{do}$
            + Sample $\epsilon \sim N(0,I_d)$
            + $X_{t+h}=X_t+h\mu_t(X_t)+\sigma_t\sqrt{h}\epsilon$ $\sqrt{h}$是为了保证方差为h
            + Update $t\leftarrow t+h$
        + $\textbf{end for}$

Diffusion Model&Flow Matching

形式语言与自动机笔记

# Credit
+ 授课教师： [梁红瑾](hongjin-liang.github.io)
+ 上课时间：2025秋
+ 主要是分成`lambda calculus`和`semantics`两部分



# Lambda Calculus
之前就听说过不少，SICP课上还被Church Numeral折磨过

### 定义
$(Terms) M,N\ ::=\ x\ | \lambda x.M\ |\ M\ N$

### 规则
+ $\lambda$延伸到括号的最右方 $\lambda x.\ M\ N$意思是$\lambda x.\ (M\ N)$
+ 函数应用是左结合 $M\ N\ P$意思是$(M\ N)\ P$

### 自由和约束变量
+ $\lambda x.(x+y)$相等于$\lambda z.(z+y)$, $x$是绑定变量(bound variables)
+ 但自由变量的名字很重要
+ fv(M)是M中自由变量的集合
    + $fv(x) \overset{\mathrm{def}}{=} {x}$
    + $fv(\lambda x.M) \overset{\mathrm{def}}{=} fv(M)-{x}$
    + $fv(M\ N) \overset{\mathrm{def}}{=} fv(M) \cup fv(N) $
+ $\alpha$等价: $\lambda x.M=\lambda y.M[y/x]$ y是新变量

### 化简规则
+ $\beta$化简： $(\lambda x.M)N \rightarrow M[N/x]$
+ 替换规则
    + $x[N/x] \overset{\mathrm{def}}{=} N$
    + $y[N/x] \overset{\mathrm{def}}{=} y$
    + $(M P)[N/x] \overset{\mathrm{def}}{=} (M[N/x]) (P[N/x])$
    + $(λx.M)[N/x] \overset{\mathrm{def}}{=} λx.M$
    + $(λy.M)[N/x] \overset{\mathrm{def}}{=} λy.(M[N/x]), if\ y ∉ fv(N)$
    + $(λy.M)[N/x] \overset{\mathrm{def}}{=} λz.(M[z/y][N/x]), if\ y ∈ fv(N)\ and\ z\ fresh$
### 合流性
Terms可以以任何顺序化简，如果有最终结果的话，其唯一确定。
+ $\beta-redex$  类似$(\lambda x.M)N$形式的term
+ $\beta-normal\ form$ 不含$\beta-redex$的term
+ 合流性理论:
    + 对于所有的$M,M_1,M_2$,如果$M\rightarrow^*M_1$且$M\rightarrow^*M_2$,那么存在$M'$使得$M_1\rightarrow^*M'$且$M_2\rightarrow^*M'$
+ $Normal-order\ reduction:$最外层的最左边的redex(有点像lazy evaluation)
    + $(\lambda u.\lambda v.v)((\lambda x.x\ x)(\lambda x.x\ x))\rightarrow \lambda v.v$
+ $Applicative-order\ reduction:$最内层的最左边的redex(有点像eager evaluation)
    + $(\lambda u.\lambda v.v)((\lambda x.x\ x)(\lambda x.x\ x))\rightarrow (\lambda u.\lambda v.v)((\lambda x.x\ x)(\lambda x.x\ x)) ...$
### 求值和化简
+ 化简可以在lambda函数体内化简，但是求值不在lambda函数体内化简
+ 下图中evaluation会停在第三个后
![](https://ys.al/static/img/7df8299e4ae28b0a19ac5f0a74fbdaea.image.webp)
+ ![](https://ys.al/static/img/80566dcadcb54402e0454158a415ace7.image.webp)
+ 范式(canonical form)意思是不能再求值的form, 但可能范式内部（lambda内部）可以继续化简
### 对于常用值的编码
+ $True \overset{\mathrm{def}}{=} \lambda x.\lambda y.x$
+ $False \overset{\mathrm{def}}{=} \lambda x.\lambda y.y$
+ True是取第一个, False是取第二个，因此在此上面进行的运算也是根据这个性质进行的
+ $0 \overset{\mathrm{def}}{=} \lambda f.\lambda x.x$ 
+ $n \overset{\mathrm{def}}{=} \lambda f.\lambda x.f^n\ x$ 
+ n是运算n次
### 不动子
+ $F = \lambda f.\,\lambda n.\,\text{if }(n=0)\text{ then }1\text{ else } n \cdot f(n-1).$ 则$fact = F\ fact$
+ 图灵不动子
    + $A\ =\ \lambda x.\lambda y.y(x\ x\ y)$, $\Theta=A A$
+ Curry不动子
    + $Y=\lambda f.(\lambda x.f (x\ x)) (\lambda x.f (x\ x))$
 
# Simply-Typed Lambda Calculus
### 定义
+ $(\text{Types})\quad \tau, \sigma ::= T \mid \sigma \to \tau$
+ $\Gamma \vdash M : \tau$. $\Gamma$中有所有的自由变量定义
### Soundness
+ 对于任何$M,M',\tau$如果$· \vdash M:\tau$且$M\to^*M'$那么$· \vdash M':\tau$并且要么$M'\in Values$或者$\exist M''.M'\to M''$
+ Preservation: M,M' and $\tau$, 如果$·\vdash M:\tau$且$M\to M'$那么$·\vdash M':\tau$
+ Progress:如果$· \vdash M:\tau$那么要么$M\in Values$或者$\exist M'.M\to M'$
### Not Complete
+ 这个类型系统可能会拒绝不会出错的程序
+ 有完善类型的term永远会终止
### Curry-Howard同构
+ 如果把基础类型看成命题，函数类型看成蕴含，乘积类型看成and，那么构造性命题逻辑和类型系统同构！
+ 测试类型是否非空:(对应的term是否closed)
    + 看这个对应的命题是否能被证明
+ 排中律：在命题逻辑中，一个命题要么真要么假，因此命题$p\lor(p\to q)$永远为真。
    + 但是STLC不支持这一点，它要求必须确定或两边到底哪个为真。因此如果需要用到它，则必须把它作为一个明显的假设
# 操作语义
我们希望探寻语句究竟**怎么算**

### 定义
+ $(States)\quad \sigma \in Var \to Values$
+ $(IntExp)\quad e::=\textbf{n}|x|e+e|e-e|...$
+ $(Comm) c::=\textbf{skip}|x:=e|c;c|\textbf{if}\ b\ \textbf{then}\ c\ \textbf{else}\ c|\textbf{while}\ b\ \textbf{do}\ c$
+ 注意while的小步语义不要丢失b
### 小步语义的性质
+ 对于所有$c,\sigma,c',\sigma ',c'',\sigma ''$, 如果$(c,\sigma)\to(c',\sigma ')$并且$(c,\sigma)\to (c'',\sigma '')$, 那么$(c',\sigma ')=(c'',\sigma '')$ 确定性
+ 对于所有$c,\sigma,c',\sigma ',c'',\sigma ''$, 如果$(c,\sigma)\to^*(c',\sigma ')$并且$(c,\sigma)\to^* (c'',\sigma '')$, 那么存在$c''',\sigma'''$使得$(c',\sigma ')\to^*(c''',\sigma ''') and (c'',\sigma '')\to^*(c''',\sigma ''')$ 合流性
+ $(e,\sigma)$和$(b,\sigma)$是normalizing的（最终会到达一个normal form），但$(c,\sigma)$不一定
### 拓展
+ 直接对表达式求值
+ ![](https://ys.al/static/img/c4a19e539f90bf6164c8327a21ca13b4.image.webp)
+ 我们不希望把局部变量暴露给$\sigma$因此对于局部变量定义
    + ![](https://ys.al/static/img/7964ad5df14db26abf075fadfd14e364.image.webp)
    + 仍然包裹局部变量定义，但执行一步
+ 添加堆
+ Contextual Semantics
    + 我们考虑用`[]`指代下一步要算的`redex`即原子操作，
    + $\mathcal{E} ::= [\,]\mid \mathcal{E} + e\mid \mathcal{E} - e\mid n+\mathcal{E}\mid n - \mathcal{E}$
    + $x:=1+[\ ]\ NOT\ while\ false\ do\ x:=1+[\ ]$ (不该出现)
    + ![](/static/img/5743d755080786a1193fea567291639f.image.webp)
### 大步语义
+ 直接得知最后的结果
+ $(c,\sigma)\Downarrow \sigma';(e,\sigma)\Downarrow n$
+ For all $e,\sigma,n,n',$ 如果$(e,\sigma)\Downarrow n$且$(e,\sigma)\Downarrow n'$那么$n=n'$ 确定性
+ 对于所有$e,\sigma$存在$n$使得$(e,\sigma)\Downarrow n$ 整体性Totality
+ $(e,\sigma)\lfloor \textbf{n}\rfloor\ iff.\ (e,\sigma)\to^*(\textbf{n},\sigma)$和小步语义等价
# 霍尔逻辑
### 定义
+ 偏正确性定义: $\{p\}c\{q\}$
+ 全正确性定义: $[p]c[q]$ (偏正确性+一定终止)
### 核心规则
+ AS: $\{p[e/x]\}x:=e\{p\}$
+ 增强前条件、减弱后条件
+ 循环不变式:
    + $\{i\land b\}c\{i\}$
    + 有时候需要增强`loop invarient`来证明循环后的内容
+ 循环变量:
    + $[i\land b\land (e=x_0)]c[i\land(e<x_0)]$ $i\land b \Rightarrow e\ge0$
    + 递减且有界
+ 在应用顺序规则的时候，需要先标注出二者之间的条件(assertation)
### Soundness and completeness
+ 注意$|-$和$|=$的区别，$|-$是在某个公理系统中可以推导出来的,$|=$代表在某个配置下是真的
+ Soundness: 如果$|-p$那么$|=p$
+ Completeness: 如果$|=p$那么$|-p$
+ 我们可以证明Soundness: 如果$|-\{p\}c\{q\}$那么$|=\{p\}c\{q\}$
    + 先对于公理证明
    + 然后利用小步语义进行归纳法
+ 但是霍尔逻辑并不complete:
    + ![](https://ys.al/static/img/8ca7abe482b7de33f0e6a11d637764ce.image.webp)
    + 如果complete的话，那么任意语义为真的命题都能被证明(与哥德尔不完备定理冲突)
    + $|=\{\textbf{true}\}c\{\textbf{false}\}$ 当且仅当c不停止才成立，然而c是否停止是不可判定的
+ 因此提出`Relative Completeness`相对完备，如果我们把所有语义为真的命题作为已知条件，那么completeness成立

程序设计语言的形式语义笔记

# 事件起因:
我需要微调一个多模态大模型，为了压缩图片输入的token数量，防止上下文数量过长导致训练时间和效果变差，在多模态大模型的```Vision Encoder```后加入一个模块用于把每张图片的token数压缩至32个.



# 奇妙的bug
我加入的模块大概长这样:
```python
def apply_compress(self, features):
    """
    features: [image_size,original_token,hidden_dim]
    """
    new_image_feature = []
    for i in range(image_size):
        new_image_feature.append(compress(features[i]))
    
    return new_image_feature
```
省去了很多细节，在训练的时候，奇怪的事情发生了: 在单卡上训练速度很正常，但一旦我切换到双卡, 训练在第一个batch都没完成的情况下就卡死了(batch_size=1)

经过排查，我发现rank0和rank1都执行到了这个函数, rank0的image_size为47, rank1的image_size为24. 在rank1处理完所有的图片后, rank0和rank1一起卡死.

# 问题解决
我一开始以为是compress函数有问题(但其实它是一个库函数), 结果发现我对torch的多卡运算有误,下面直接贴出AI的解释:

您好！从您提供的详尽代码和问题描述来看，这是一个非常典型的分布式训练（DDP, Distributed Data Parallelism）中遇到的 **死锁（Deadlock）或挂起（Hang）** 问题。

根本原因在于：**在分布式训练中，每个进程（GPU/rank）的计算图和执行路径必须完全一致。而您当前的代码和数据加载方式破坏了这个核心原则。**

### 问题根源：执行路径不一致导致同步失败

在 PyTorch DDP 中，`forward` 传播过程会记录模型中每个参数参与的运算。在 `backward` 传播时，DDP 会为每个参数注册一个钩子（hook），当该参数的梯度计算完成后，DDP 会立即启动一个异步的 `AllReduce` 操作，将所有进程上的这个梯度进行求和平均，从而保证所有进程的梯度一致。

这个机制能正常工作的前提是：**所有进程必须以完全相同的顺序、对完全相同的参数集计算梯度**。如果任何一个进程的计算路径与其他进程不同，就会导致：

  * 某个进程期望收到一个它永远不会收到的梯度（因为它没有执行相应的计算）。
  * 或者，进程之间 `AllReduce` 的顺序错乱。

这两种情况都会导致某些进程无限期地等待其他进程，从而造成整个训练过程的挂起。

#### 1\. 罪魁祸首：不同数量的图像 (47 vs 24)

您描述的场景是问题的核心：

  * **Rank 0** 加载了包含 **47** 个图像的样本。
  * **Rank 1** 加载了包含 **24** 个图像的样本。

  * **执行次数不同**：Rank 0 的 `for` 循环会执行 47 次，而 Rank 1 只会执行 24 次。
  * **计算图不同**：这意味着 `self.compress` 这个模块（它是一个拥有独立参数的神经网络）在 Rank 0 上被调用了 47 次，而在 Rank 1 上只被调用了 24 次。
  * **DDP 崩溃**：当反向传播开始时，Rank 0 会计算 47 次 `compress` 的梯度，并准备进行 47 次相应的 `AllReduce` 同步。而 Rank 1 只会计算 24 次。当 Rank 1 完成它自己的 24 次计算和同步后，它就会进入等待状态。与此同时，Rank 0 在完成了 24 次同步后，会继续尝试发起第 25 次 `AllReduce`，但此时它永远等不到 Rank 1 的响应，因为 Rank 1 的计算图里已经没有这个操作了。于是，Rank 0 就被永久地卡住了。

您遇到的问题是 DDP 的经典陷阱。其核心是由于**数据不均匀（不同数量的图像）导致了模型中带参数模块（`PerceiverResampler`）的调用次数不一致**，破坏了 DDP 要求的“计算图一致性”原则，从而在梯度同步时发生死锁。

**最直接的解决方案是：修改您的数据加载和预处理流程，确保送入模型的每个 batch 在所有 GPU 上的结构（尤其是可变长度的元素，如图像数量）都是统一的，通常通过填充（Padding）来实现。**

# 后续的拓展
只有需要梯度的模块才要求计算图相同.