AlumKal's Blog

群数独

发表于 2024-12-13 更新于 2026-04-29 本文字数： 3k 阅读时长 ≈ 11 分钟

前言

看抽象代数的时候突然想到，群的 Cayley 表和数独一样，都要求每行（列）中的元素互异。那么能不能按照群的规则（即结合律）出一道变种数独题呢？于是简单试了一下。

规则：

题面是一个 $10 \times 10$ 数表（行和列从 $0$ 开始计数），元素为 $0 \sim 9$ 的整数；第 $0$ 行和第 $0$ 列的值已经给出
与普通数独相同，每行、每列的元素不能重复；注意没有九宫格的条件
若 $i$ 行 $j$ 列的值为 $x$，$j$ 行 $k$ 列的值为 $y$，则 $i$ 行 $y$ 列和 $x$ 行 $k$ 列的值相同

TLDR：补全一个以 $0$ 为单位元的 $10$ 阶群的乘法表。（提示：$10$ 阶群只有 $\mathrm{Z}_{10}$ 和 $\mathrm{D}_{10}$ 两种）

为什么这一规则对应群

把第 $i$ 行第 $j$ 列的值记为 $i \otimes j$. 根据第一条规则，$\otimes$ 是 $\{0,1,\dots,9\}$ 上的一个二元运算，值域也是 $\{0,1,\dots,9\}$. 因此 $\otimes$ 满足封闭性。

第 $0$ 行和第 $0$ 列的值表明，对任意 $x$ 都有 $0 \otimes x = x \otimes 0 = x$，因此 $0$ 是单位元。

若 $i \otimes j = x,\ j \otimes k = y$，由第三条规则可得

\[ i \otimes (j \otimes k) = i \otimes y = x \otimes k = (i \otimes j) \otimes k, \]

因此 $\otimes$ 满足结合律。

根据第二条规则，每一行、每一列的 $10$ 个数都互不相同；又因为它们都落在 $\{0,1,\dots,9\}$ 中，因此每一行、每一列都是这 $10$ 个数的一个排列。

于是对任意 $a$，存在 $b,c$ 使得 $a \otimes b = 0,\ c \otimes a = 0$. 再由结合律可得

\[ c = c \otimes 0 = c \otimes (a \otimes b) = (c \otimes a) \otimes b = 0 \otimes b = b, \]

因此 $b$ 同时是 $a$ 的左逆元和右逆元。

综上所述，这三条规则恰好定义了一个以 $0$ 为单位元的 $10$ 阶群；反过来，任何 $10$ 阶群的 Cayley 表也都满足这三条规则。

题目

题 1：（表中横、竖线仅作美化排版用途，无实际含义）

\[ \begin{array} {r|rrr|rrr|rrr} 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 \\ \hline 1 & 0 & & & & & & & & \\ 2 & & & 1 & & & & & & \\ 3 & & 4 & & & & & & & \\ \hline 4 & & & & & & & & & \\ 5 & & & & 2 & & & & & \\ 6 & & & & & & & & & \\ \hline 7 & & & & & & 3 & & & \\ 8 & & & & & 9 & & & & \\ 9 & & & & & & & & & \\ \end{array} \]

解析

表中 $2 \otimes 3 \ne 3 \otimes 2$，说明这个群一定是 $\mathrm{D}_{10}$. 这里先明确一下记号：$\mathrm{D}_{10} = \langle r, s \mid r^5 = s^2 = e,\ sr = r^{-1}s \rangle$.

解决题目的关键在于理解 $\mathrm{D}_{10}$ 的自同构。 $\operatorname{Aut}(\mathrm{D}_{10})$ 在 $\{r,r^2,r^3,r^4\}$ 与 $\{s,rs,r^2s,r^3s,r^4s\}$ 上分别传递作用；等价地，任取一个非单位旋转元 $r^n\ (n=1,2,3,4)$ 和一个反射元 $r^m s\ (m=0,1,2,3,4)$，都存在 $\mathrm{D}_{10}$ 的自同构 $\varphi$，使得 $\varphi(r^n)=r,\ \varphi(r^m s)=s$.

$0$ 是单位元，而 $1 \otimes 1 = 0$，说明 $1$ 是“s 型”元素。再由上面的自同构性质可知，若本题有解，则一定可以通过适当的自同构让 $1$ 对应群中元素 $s$（下文简写为 $1 \sim s$）。因此不妨设 $1 \sim s$.

$2 \otimes 3 = 1$，说明 $2$ 和 $3$ 一个是“r 型”，一个是“s 型”。注意到 $5 \otimes (3 \otimes 2) = 2$，因此 $5$ 和 $3$ 互为逆元。“s 型”元素的逆元都是它本身，因此 $3$ 是“r 型”，$2$ 是“s 型”。

不妨设 $3 \sim r$，则 $2 \sim rs$，$5 \sim r^4$. $3 \otimes 2 = 4$，说明 $4 \sim r^2 s$.

这是目前已确定的元素：

$0$	$1$	$2$	$3$	$4$	$5$	$6$	$7$	$8$	$9$
$e$	$s$	$rs$	$r$	$r^2 s$	$r^4$

还剩下 $r^2,\, r^3,\, r^3 s,\, r^4s$ 尚未确定。

$7 \otimes 6 = 3$，说明 $6$ 和 $7$ 要么都是“r 型”，要么都是“s 型”。而 $r^2 \cdot r^3 = r^3 \cdot r^2 = e$，说明 $6$ 和 $7$ 只能都是“s 型”，因此 $6 \sim r^3 s$，$7 \sim r^4 s$.

$8 \otimes 5 = 9$，而 $8$ 和 $9$ 只能在 $r^2,\, r^3$ 中取值，因此 $8 \sim r^3$，$9 \sim r^2$.

完整的对应关系如下：

$0$	$1$	$2$	$3$	$4$	$5$	$6$	$7$	$8$	$9$
$e$	$s$	$rs$	$r$	$r^2 s$	$r^4$	$r^3 s$	$r^4 s$	$r^3$	$r^2$

据此把乘法表补全即可。

答案：

\[ \begin{array} {r|rrr|rrr|rrr} 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 \\ \hline 1 & 0 & 5 & 7 & 8 & 2 & 9 & 3 & 4 & 6 \\ 2 & 3 & 0 & 1 & 5 & 4 & 8 & 9 & 6 & 7 \\ 3 & 2 & 4 & 9 & 6 & 0 & 7 & 1 & 5 & 8 \\ \hline 4 & 9 & 3 & 2 & 0 & 6 & 5 & 8 & 7 & 1 \\ 5 & 7 & 1 & 0 & 2 & 8 & 4 & 6 & 9 & 3 \\ 6 & 8 & 9 & 4 & 3 & 7 & 0 & 5 & 1 & 2 \\ \hline 7 & 5 & 8 & 6 & 9 & 1 & 3 & 0 & 2 & 4 \\ 8 & 6 & 7 & 5 & 1 & 9 & 2 & 4 & 3 & 0 \\ 9 & 4 & 6 & 8 & 7 & 3 & 1 & 2 & 0 & 5 \\ \end{array} \]

题 2：

\[ \begin{array} {r|rrr|rrr|rrr} 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 \\ \hline 1 & & & & & & & & & \\ 2 & & & & & & & & & \\ 3 & & & 0 & & & & & & 4 \\ \hline 4 & & & & & & & & 0 & \\ 5 & & 7 & & & & & & & \\ 6 & & & & & & & & & \\ \hline 7 & & & & & & & & & \\ 8 & & & & & 2 & & & & \\ 9 & & & & 1 & & & & & \\ \end{array} \]

解析

用和题 1 类似的方法，可以发现 $\mathrm{D}_{10}$ 是不行的。因此，这个群只能是 $\mathrm{Z}_{10}$. 记 $\mathrm{Z}_{10} = \langle g \mid g^{10} = e \rangle$.

$3 \otimes 3 = 0$，说明 $3$ 的阶为 $2$，因此 $3 \sim g^5$.

考虑从 $4$ 出发往后推。但我们还不确定 $4$ 的阶是 $5$ 还是 $10$. 先假设 $4$ 的阶是 $5$，那么不妨设 $4 \sim g^2$.

$3 \otimes 9 = 4$，说明 $9 \sim g^7$. $4 \otimes 8 = 0$，说明 $8 \sim g^8$. $9 \otimes 4 = 1$，说明 $1 \sim g^9$.

这是目前已确定的元素：

$0$	$1$	$2$	$3$	$4$	$5$	$6$	$7$	$8$	$9$
$e$	$g^9$		$g^5$	$g^2$				$g^8$	$g^7$

还剩下 $g,\, g^3,\, g^4,\, g^6$ 尚未确定。

还有两个条件没有用到：$5 \otimes 2 = 7$ 和 $8 \otimes 5 = 2$. 对 $8 \otimes 5 \otimes 2$ 使用结合律，得到 $2 \otimes 2 = 8 \otimes 7$.

这说明 $7$ 是 $g^4$ 或者 $g^6$. 若 $7 \sim g^4$，则 $2 \sim g$ 或 $2 \sim g^6$；若 $7 \sim g^6$，则 $2 \sim g^2$ 或 $2 \sim g^7$，矛盾。因此，$7 \sim g^4$.

$5 \otimes 2 = 7$，若 $2 \sim g$，则 $5 \sim g^3$；若 $2 \sim g^6$，则 $5 \sim g^8$，矛盾。因此，$2 \sim g$，$5 \sim g^3$，$6 \sim g^6$.

完整的对应关系如下：

$0$	$1$	$2$	$3$	$4$	$5$	$6$	$7$	$8$	$9$
$e$	$g^9$	$g$	$g^5$	$g^2$	$g^3$	$g^6$	$g^4$	$g^8$	$g^7$

据此把乘法表补全即可。

如果 $4$ 的阶是 $10$，按同样流程推导会出现矛盾，过程不再赘述。

答案：

\[ \begin{array} {r|rrr|rrr|rrr} 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 \\ \hline 1 & 8 & 0 & 7 & 2 & 4 & 3 & 5 & 9 & 6 \\ 2 & 0 & 4 & 6 & 5 & 7 & 9 & 3 & 1 & 8 \\ 3 & 7 & 6 & 0 & 9 & 8 & 2 & 1 & 5 & 4 \\ \hline 4 & 2 & 5 & 9 & 7 & 3 & 8 & 6 & 0 & 1 \\ 5 & 4 & 7 & 8 & 3 & 6 & 1 & 9 & 2 & 0 \\ 6 & 3 & 9 & 2 & 8 & 1 & 4 & 0 & 7 & 5 \\ \hline 7 & 5 & 3 & 1 & 6 & 9 & 0 & 8 & 4 & 2 \\ 8 & 9 & 1 & 5 & 0 & 2 & 7 & 4 & 6 & 3 \\ 9 & 6 & 8 & 4 & 1 & 0 & 5 & 2 & 3 & 7 \\ \end{array} \]

以下是作者的一些疑问：

存不存在只有 5 个已知数且有唯一解的题面？
有没有比较有效的方法构造这类题目的 $8 \times 8$ 版本？

自动生成器

时隔一年多突然想起这篇烂尾博客，我惊喜地发现现在的 LLM 已经可以爆杀上文的两个疑问了。以下两节的代码全部由 GPT-5.4 生成。

首先从枚举所有合法的 Cayley 表开始。借助一些（我并不会的）抽象代数知识，可以在近似 $O(\mathrm{output \_ size})$ 的时间复杂度内完成枚举。生成枚举结果的 GAP 程序见此。生成 3GiB 大小的 $12 \times 12$ Cayley 表全集需要约 5min。

$8$ 阶群有 $2760$ 种 Cayley 表，$10$ 阶群有 $108864$ 种，$12$ 阶群有 $21621600$ 种。对于 $8$ 阶和 $10$ 阶群，可以直接使用（剪枝后的）暴力搜索找出已知数最少且有唯一解的题面。对于 $12$ 阶群，暴力搜索已经不可行了，因此略作妥协：对于每类群，随机选择一个答案，二分搜索已知数的数量，随机生成题面，若连续 $1000$ 个题面都有多解，则认为该数量的已知数不足以保证唯一解，尝试更多的已知数。

对于两种 $10$ 阶群，最少的已知数都是 $5$ 个：

\[ \begin{array} {r|rrr|rrr|rrr} 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 \\ \hline 1 & 5 & & & & & & & & \\ 2 & & 4 & & & & & & & \\ 3 & & & & 8 & & & & & \\ \hline 4 & & & & & & & & & \\ 5 & & 7 & & & & & & & \\ 6 & 3 & & & & & & & & \\ \hline 7 & & & & & & & & & \\ 8 & & & & & & & & & \\ 9 & & & & & & & & & \\ \end{array} \]

\[ \begin{array} {r|rrr|rrr|rrr} 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 \\ \hline 1 & 7 & & & & & & & & \\ 2 & & 8 & & & & & & & \\ 3 & 6 & & & & & & & & \\ \hline 4 & & & & & 8 & & & & \\ 5 & & & & & & 2 & & & \\ 6 & & & & & & & & & \\ \hline 7 & & & & & & & & & \\ 8 & & & & & & & & & \\ 9 & & & & & & & & & \\ \end{array} \]

8 阶群的结果

这些题目都不难，欢迎读者尝试！为减少对读者时间的浪费，我直接给出了每道题对应的群类型。

$\mathrm{Z}_8$:

\[ \begin{array} {rrrr|rrrr} 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 \\ 1 & & & & & & & \\ 2 & 3 & & & & & 5 & \\ 3 & & & & & & & 4 \\ \hline 4 & & & & & & & \\ 5 & & & & & 3 & & \\ 6 & & & & & & & \\ 7 & & & & & & & \\ \end{array} \]

$\mathrm{Z}_4 \times \mathrm{Z}_2$:

\[ \begin{array} {rrrr|rrrr} 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 \\ 1 & 0 & & & & & & \\ 2 & & & & & & & 0 \\ 3 & & & & & & & \\ \hline 4 & & & & 3 & & & \\ 5 & & & & & & & \\ 6 & & & & 2 & & & \\ 7 & & & & & & & \\ \end{array} \]

$\mathrm{D}_8$:

\[ \begin{array} {rrrr|rrrr} 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 \\ 1 & & & & & & & \\ 2 & & & & & & & \\ 3 & & & & & & & \\ \hline 4 & & & & & & & \\ 5 & & & & & 0 & & \\ 6 & & & & & & 3 & 2 \\ 7 & 3 & & & & & & \\ \end{array} \]

$\mathrm{Q}_8$:

\[ \begin{array} {rrrr|rrrr} 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 \\ 1 & & & & & & & \\ 2 & & & 5 & & & & \\ 3 & & & & & & & \\ \hline 4 & & & & 7 & 6 & & \\ 5 & & & & & 7 & & \\ 6 & & & & & & & \\ 7 & & & & & & & \\ \end{array} \]

$\mathrm{Z}_2 \times \mathrm{Z}_2 \times \mathrm{Z}_2$:

\[ \begin{array} {rrrr|rrrr} 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 \\ 1 & & & & & & 4 & \\ 2 & & & & & 1 & & \\ 3 & & & & 2 & & & \\ \hline 4 & & & & & & & \\ 5 & & & 6 & & & & \\ 6 & 4 & & & & & & \\ 7 & & & & & & & 0 \\ \end{array} \]

12 阶群的结果

~~我对这些群不熟悉，就不手算了，总之能做~~

$\mathrm{Q}_{12}$:

\[ \begin{array} {rrr|rrr|rrr|rrr} 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & \mathrm{A} & \mathrm{B} \\ 1 & & 4 & & & & & & & & & \\ 2 & & & & & & & & & & & \\ \hline 3 & & & & & & & \mathrm{B} & & & & \\ 4 & & & & & & & & & & & \\ 5 & & & & & & & 1 & & & & \\ \hline 6 & & & & & & & & & & & \\ 7 & & & 6 & & & 8 & & & & & \\ 8 & & & & & & & & & & & \\ \hline 9 & & & 1 & & & & & & & & \\ \mathrm{A} & & & & & & & & & & & \\ \mathrm{B} & & & & & & & & & & & \\ \end{array} \]

$\mathrm{Z}_{12}$:

\[ \begin{array} {rrr|rrr|rrr|rrr} 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & \mathrm{A} & \mathrm{B} \\ 1 & & & & & & & & & & & \\ 2 & & & & & 6 & & & & & & \\ \hline 3 & & & & & & & & & & & \\ 4 & & & & & & & & & & \mathrm{B} & \\ 5 & & & & & & & & & & & \\ \hline 6 & & & & & & & & & 2 & & \\ 7 & & & & & & & & & & & \\ 8 & & & & & & & & 2 & & & \\ \hline 9 & & & & & & & & & & & \\ \mathrm{A} & 0 & & & & & & & & & 5 & 7 \\ \mathrm{B} & & & & & & & & & & & \\ \end{array} \]

$\mathrm{A}_{4}$:

\[ \begin{array} {rrr|rrr|rrr|rrr} 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & \mathrm{A} & \mathrm{B} \\ 1 & & & & & & & & & & & \\ 2 & & & \mathrm{B} & & & & & & & & \\ \hline 3 & & & & & & & & & & & \\ 4 & & & & & & & & & & & \\ 5 & 7 & & & & & & & & & & \\ \hline 6 & & & & & 7 & & & & & & \\ 7 & & & & & & & & & & & \\ 8 & & & & & & & & 5 & & & \\ \hline 9 & & & & & 4 & & & & & & \\ \mathrm{A} & & & & & & & & & & & \\ \mathrm{B} & & & & & & & & & & & \mathrm{A} \\ \end{array} \]

$\mathrm{D}_{12}$:

\[ \begin{array} {rrr|rrr|rrr|rrr} 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & \mathrm{A} & \mathrm{B} \\ 1 & & & & & & & & & & & \\ 2 & & & & & & & & & & & \\ \hline 3 & & & & & & & & & & & \\ 4 & & & & & & 9 & & & & & \\ 5 & & & & & & & & & & & \\ \hline 6 & & 1 & & & & & & & & & \\ 7 & & & & & 8 & & & & & & \\ 8 & 4 & & & & & & & & & & \\ \hline 9 & \mathrm{A} & & & & & & & & & & \\ \mathrm{A} & & & & 3 & & & & & & & \\ \mathrm{B} & & & & & & 0 & & & & & \\ \end{array} \]

$\mathrm{Z}_{6} \times \mathrm{Z}_{2}$:

\[ \begin{array} {rrr|rrr|rrr|rrr} 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & \mathrm{A} & \mathrm{B} \\ 1 & & & & & & 3 & & & & & \\ 2 & & & & & & & & & & & \\ \hline 3 & & & & & & & & & & & \\ 4 & & & & & & & & & & & \\ 5 & & & & & & & & & & & \\ \hline 6 & & 8 & & & & & & & & & \\ 7 & & & & & & & & & & & \\ 8 & 4 & & & & & & & & & & \\ \hline 9 & & & & & & & & & & & \\ \mathrm{A} & & & & & & & 9 & & 8 & & \\ \mathrm{B} & & & & 3 & & & 2 & & & & \\ \end{array} \]

自动求解器

首先考虑最暴力的求解方法：直接把结合律作为约束，使用求解器求解。使用 Z3 描述这种约束非常简单：

op = Function("op", IntSort(), IntSort(), IntSort())
solver = Solver()

for left in range(order):
    for right in range(order):
        solver.add(op(left, right) >= 0, op(left, right) < order)

for element in range(order):
    solver.add(op(0, element) == element)
    solver.add(op(element, 0) == element)
    solver.add(Distinct([op(element, other) for other in range(order)]))
    solver.add(Distinct([op(other, element) for other in range(order)]))

for row in range(1, order):
    for col in range(1, order):
        clue = grid[row][col]
        if clue is not None:
            solver.add(op(row, col) == clue)

for a in range(order):
    for b in range(order):
        for c in range(order):
            solver.add(op(a, op(b, c)) == op(op(a, b), c))

这个程序可以求解 $8$ 阶和 $10$ 阶的题目，但对于 $12$ 阶的题目就无能为力了：五道题目在 1min 的时限内都无法求解并证明唯一性。

能不能做得更好呢？答案是肯定的。我们可以把抽象代数知识融入求解器，告诉它对应阶数的群的所有种类。对于每个种类，任取一个 Cayley 表作为规范形，让求解器搜索题面数字与这一 Cayley 表中元素之间的一一映射。这样，求解器的搜索空间就从 $121$ 个格子变成了 $11$ 个元素的排列。改进后的程序可以在 27s 内解决五道 $12$ 阶题目。

当然——如果融入更多的知识，也就是直接把所有 Cayley 表丢进去，那么遍历一遍就能得到答案了，用时甚至不到一秒钟！看来数学理论对这个奇特的解谜帮助确实很大（笑）

Pandas 读取 CSV 时保留字符串原值

发表于 2026-01-13 本文字数： 354 阅读时长 ≈ 1 分钟

TLDR: 使用 Pandas 读取 CSV 文件时，最好指定 keep_default_na=False, na_values=''。

问题

Pandas 的 read_csv 默认会把长得像无效值的字符串（如 NA、null、None 等）解析为 NaN，而这些字符串有时确实是合法内容~~（比如某些不知好歹的人的用户名）~~。这会导致读入 CSV 后重新导出的过程中丢失数据。

Pandas 默认的 NA 值列表可以在文档中找到：

By default the following values are interpreted as NaN: , #N/A, #N/A N/A, #NA, -1.#IND, -1.#QNAN, -NaN, -nan, 1.#IND, 1.#QNAN, <NA>, N/A, NA, NULL, NaN, None, n/a, nan, null.

解决方案

在 read_csv 时指定以下参数：

1 2	df = pd.read_csv('data.csv', keep_default_na=False, na_values='') df.to_csv(index=False)

keep_default_na=False 的作用是禁用默认的 NA 值列表；na_values='' 的作用是把空字符串视为缺失值。如果去掉后者，则所有包含空单元格的列都会被视作字符串类型，对数值类数据不合理。

美中不足的是，并不存在一个参数可以直接将所有字符串列的空值视作 ''，同时保留数值列的 NaN。不过可以通过后续处理来实现：

1 2	cols = df.select_dtypes(include=['object']).columns df.fillna(pd.Series('', index=cols), inplace=True)

示例

>>> df = pd.read_csv(io.StringIO('str,num\nnull,\n,1')); df
   str  num
0  NaN  NaN
1  NaN  1.0

>>> df = pd.read_csv(io.StringIO('str,num\nnull,\n,1'), keep_default_na=False, na_values=''); df
    str  num
0  null  NaN
1   NaN  1.0

>>> df.fillna(pd.Series('', index=df.select_dtypes(include=['object']).columns))
    str  num
0  null  NaN
1        1.0

准定态挂机教程：基于状态机实现

发表于 2025-08-09 本文字数： 4.4k 阅读时长 ≈ 16 分钟

自然出怪的特点

在之前我们写的脚本中，绝大多数都假设每一波的刷新时长是一个定值。这使得脚本执行的操作与场上状态基本无关，大幅简化了脚本的编写。

但是，当我们把目光转向自然出怪长生存时，我们会面临很多新的问题：

两炮激活可能会刷新延迟
双边热过渡可能会意外刷新
红眼关随时可能转白
收尾的不确定性很大

即便是对于打法非常固定的键控炮阵，这些问题通常也是难以避免的。我们接下来逐个分析这些问题。

刷新延迟和意外刷新在实现上是可以统一的：它们通常的处理方法都是在某个时间点检查是否刷新，视结果执行不同的分支。

在转白之后，我们通常希望改用白眼/快速关的打法以节省资源。转换阵解时可能需要几个过渡波处理残留的红眼。

收尾很难有统一的应对方案，需要视所守列数和炮恢复情况而定。

状态机对前三个问题提供了一种较为泛用的解决方案。它保留了常规逐波/循环定态脚本的易写易读的优点，但同时又有一定的表达能力，足以应对自然出怪冲关的复杂条件。

状态机

在状态机的框架下，阵解由许多个状态组成，状态之间相互连接。每个状态代表一波或其一部分。

状态之间以刷新节点为边界。什么是刷新节点呢？比如你炸了一对激活炮，这时可能激活，也可能没有激活，炮落地的瞬间就是一个刷新节点。

如果阵型里有前场自然输出，有可能你不需要做什么也会自动刷新。这种情况下，刷新节点是连续的。状态转移允许指定一个时间区间，在区间内任意时间激活视作正常激活，区间结束时仍未激活视作延迟。

在刷新节点观测到的场上信息会用来决定转移路径。如果把阵解建模成一张图，那么状态是节点，转移路径就是连接两者的有向边。比如说你执行一组操作（它们被封装在一个状态中），执行之后可能延迟，也可能激活刷新，就需要为它配置两条转移路径。如果你确信某操作不会出现刷新意外，就可以只配置一条转移路径。

每个转移路径都有触发条件。现实中，在根据刷新情况进行状态转移时，我们一般只会使用固定的几种条件。作者实现的转移函数支持以下几种条件：

延迟
激活，下波为指定波次（如w9/w19）
激活，下波转白
激活，无特殊情况

状态机的优势在于，如果脚本只使用这几种转移条件，则完全不需要自行编写判断刷新的代码，具体的判断逻辑交由预定义的转移函数处理。

本文接下来以一个经典超多炮阵型——双冰16炮为例，介绍状态机框架下代码的编写。

代码架构

状态机的核心是以下几个变量和函数：

unordered_map<string, ATimeline> states;
string lastState, currentState;

_TransitionKey activate, delay, nogiga, finish;
_TransitionKey WaveIs(std::convertible_to<int> auto... waves);

ATimeline Transition(pair<int, int> wl, auto... args);
ATimeline Transition(int wl, auto... args);
void StartTransition(int wave, const string& state);

Transition函数封装了状态转移的所有逻辑，其调用格式形如Transition(601, key1 = "next_state_name1", key2 = "next_state_name2", ...) （如果你对这种语法感到不解：在C++中，operator=可以被重载，并且返回类型可以任意指定）。其中的key可以是delay、activate、nogiga和finish，对应上一节中提到的四种转移条件（finish等效于WaveIs(9, 19)）。

lastState和currentState是由Transition函数自动设置的，在运阵过程中可以读取。

states用于存储阵解，键代表状态名（可以任意取），值代表该状态对应的操作。在AScript()中，操作被逐个添加到states中，形如：

states["s1"] = {
    Transition(601, activate = "s2", delay = "s3"),
    At(300) PP(),
};

这段代码表示若当前状态为s1，则在本波300时刻发一对炮，若401时刻激活，则在下波执行状态s2；若401时刻未激活，则在本波执行状态s3。

状态机一般需要在w1和w10各启动一次（w20不需要纳入状态机中）。启动状态机的代码是：

1 2	StartTransition(1, "state1"); StartTransition(10, "state2");

一个完整的状态机脚本的大致结构是：

// 状态机本身的代码

void AScript() {
    // 选卡等等操作

    states["s1"] = {
        Transition(601, activate = "s2", delay = "s3", finish = "final1"),
        // ...
    };
    states["s2"] = {
        Transition(1200, activate = "s1", delay = "s4", finish = "final2"),
        // ...
    };
    // ...

    StartTransition(1, "s1");
    StartTransition(10, "s1");
    OnWave(20) {
        // ...
    };
}

阵解分析

主循环

本教程侧重于键控脚本编写，对阵解设计部分只是简略带过。如果对本节理解有困难可以跳过。

我们采用经典的ch6解：IPP-PP|PPDD循环。运阵过程中有两处可能发生刷新意外：

IPP刷新
IPP-PP延迟

对于前一种情况，我们可以把冰波改成IPP|cPP。第二波的PP要同时全伤两波的红眼，设冰波1冰1048激活，加速波389激活（垫舞王激活的最晚时机），得出IPP波波长应为1048-389=659，对应459热过渡。加速波的红眼再冰一下，避免砸炮。

对于后一种情况，我们可以在激活炮之后再补一对炮，然后直接接下一个冰波。在执行IPP-PP|PPDD时，加速波的PP发射时本波僵尸还未刷出。本着能不读刷新倒计时就不读的态度，不妨让这对炮无论冰波是否延迟都照常发射。这样的话，冰波延迟时的激活时机为1248+291=1539。（注：由于引信延迟，实际激活时机也可能是1542。引信延迟并不会给此阵造成任何实质上的困难，但会给脚本编写增加无谓的工作量，因此脚本中关闭了引信延迟）

把状态转移关系画成图，是这样的：

代码如下：

// 冰波：IPP-PP 1248
states["hb_IPP"] = {
    Transition(659, delay = "hb_(IPP-)PP", activate = "hb_(IPP|)cPPI"),
    At(1) I(),
    At(459) P(15, 8.325),
    At(1048) PP(8.75), // 1048 = 659 + 389
};
states["hb_(IPP-)PP"] = {
    Transition(1248, activate = "hb_PPDD", delay = "hb_(IPP-PP-)cPP"),
};
// 加速波：PPDD 601
states["hb_PPDD"] = {
    Transition(601, activate = "hb_IPP"),
    At(291) PP() & DD<107>(9),
};
// 冰波延迟：IPP-PP-cPP 1739
states["hb_(IPP-PP-)cPP"] = {
    Transition(1739, activate = "hb_IPP"),
    At(1300) C.TriggerBy(AGIGA_GARGANTUAR & CURR_WAVE)(266),
    At(1539) PP(), // 1539 = 1248 + 291
};
// 冰波意外刷新：IPP|cPPI 659|601
states["hb_(IPP|)cPPI"] = {
    Transition(601, activate = "hb_PPDD"),
    At(195) C.TriggerBy(ADANCING_ZOMBIE, ALADDER_ZOMBIE)(40),
    At(390) I(),
};

细心的读者可能会问：hb_(IPP|)cPPI一定不会延迟吗？事实上热过渡意外刷新和PP延迟对出怪的要求是一定程度上相互冲突的，前一波意外刷新而后一波延迟的概率极低，可以忽略。当然把这一部分补上也是不难的，具体实现就留给读者了。

首代

为了省冰，我们在w1和w10用NDD首代一波。虽然红眼关w10 PPDD不太可能延迟，但保险起见写上好了。脚本很简单，就不细讲了：

// 红眼关起手：NDD 601
states["hb_NDD"] = {
    Transition(601, activate = "hb_PPDD", delay = "hb_(NDD-)PP"),
    At(292) N({{3, 9}, {4, 9}}) & DD<106>(9),
};
// NDD延迟：NDD-PP 1092
states["hb_(NDD-)PP"] = {
    Transition(1092, activate = "hb_IPP"),
    At(892) PP(), // 892 = 601 + 291
};

收尾

到目前为止，我们顺利解决了w1~w8，下一个任务是w9/w19。需要注意的是，w9/w19的激活判定只考虑本波僵尸，因此可能出现w9激活后w8红眼仍在场上的情况。

收尾的处理方式需要视阵型特点而定。此阵炮数充足，收尾容错很大。ch6冰循环压力本就不大，加之此阵转白后无需用冰，不需要拖w9/w19的收尾。因此这里采用了一种比较朴素的处理方式。

首先是w9本波的激活操作。既然已经到了收尾波，没有热过渡的必要，可以直接把IPP改成PPI（由于主循环时长3700>3475，这里是能复用上的）。加速波反正早晚得冰，不如也改成PPI。唯一的例外是上波为IPP，此时本波仍需cPPI以保证全伤上波红眼。

极端条件下，可能会出现w9 401激活（对应波长1346），而场上仍有w8三血红的情况。这时虽然剩余的炮不够把它们炸死，但我们可以把这些w8红眼拖到w10。假设w9 401激活，根据w8的类型分类讨论：

IPP：剩3血红和w8撑杆，猴年马月才能砸炮。一炮收掉残余的撑杆，剩下的2血红交给w10
(IPP-)PP或(IPP|)cPPI：剩2血红，1510砸炮。垫一下，交给w10收掉
PPDD或(IPP-PP-)cPP：剩1血红，1161砸炮。一对炮收掉

如果w9 401没有激活，假设收尾使用8门炮，算一下可能的复用：

IPP-PP|[PP]DD|收尾|NDD|PP[DD]：收尾最短时间3475+291−601×2−398=2166，对应1221激活
PPDD|I[PP]-PP|收尾|NDD|PP[DD]：收尾最短时间3475+459−1248−601−398=1687，对应742激活
PPDD|IPP-[PP]-PP|收尾|NDD|PP[DD]：收尾最短时间3475+1048−1739−601−398=1785，对应840激活
[PP]DD|IPP|收尾|NDD|[PP]DD：收尾最短时间3475+291−601×2−659−291=1614，对应669激活

可以看出除了第一种情况都是白给。第一种情况下，为了收掉w8的红眼，需要早于1161炸一对炮。但如果这对炮导致激活，说明w8和w9的僵尸一定都死了，不需要再炸剩下两对炮。这样复用就能宽松很多，依然不会出问题。

作为演示脚本，就不拖收尾了，直接炸掉就好。预定在1000、1500和2300发炮，如果此时已经进入w10或不存在除伴舞和小鬼之外的僵尸则取消此次发炮。

作者编写了一个简单的EndingHelper函数用于处理这种较简单的收尾。这个函数的原型是：

ATimeline EndingHelper(const vector<int>& times, const vector<ATimeline>& ops,
    int withdrawThreshold = 0);
ATimeline EndingHelper(const vector<int>& times, const ATimeline& op,
    int withdrawThreshold = 0);

它的功能是在当前波（EndingHelper执行时的波次）的times[0]时间执行ops[0]，times[1]时间执行ops[1]，以此类推（若ops中只有一个操作，则每次都执行ops[0]）。如果场上没有僵尸（无视小鬼、伴舞，开启女仆时额外无视舞王），或者当前操作对应的时间已经超过了下一波的withdrawThreshold，则取消操作。

比如OnWave(19) EndingHelper({1200, 1800, 2400}, PP(), 0); 的含义为在w19的1200cs、1800cs和2400cs各生效一对炮，保证炮的生效时间不会在w20的0cs之后。若1200cs的炮激活了刷新，则w19的波长为2145cs，这时1800cs的炮会照常发射，但2400cs的炮会被取消。

收尾代码如下：

states["hb_final"] = At(-200) CoDo {
    // 发本波的激活炮
    ATime thisWave = now + 200;
    if (lastState == "hb_IPP") {
        // cPPI波的处理和其他波不同
        At(thisWave + 195) C.TriggerBy(ADANCING_ZOMBIE, ALADDER_ZOMBIE)(40);
        At(thisWave + 390) I();
    } else {
        At(thisWave + 291) PP();
        At(thisWave + 360) I();
    }

    co_await (thisWave + 401);
    if (ANowTime(true).time < 0) {
        // 如果收尾波直接刷了（波长1346）
        if (lastState == "hb_IPP") {
            // w8红还剩3血，w8撑杆还在；一炮收掉撑杆，红眼交给w10
            At(thisWave + 900) PP();
        } else if (lastState == "hb_(IPP-)PP" || lastState == "trans_cPP") {
            // w8红还剩2血，1510砸炮；垫一下红眼就行
            At(thisWave + 401) C.TriggerBy(AGIGA_GARGANTUAR)(800);
        } else if (lastState == "hb_PPDD" || lastState == "hb_(IPP-PP-)cPP") {
            // w8红还剩1血，最快1161砸炮；用炮收掉
            At(thisWave + 1161) PP();
        }
    } else {
        // 随便炸炸
        At(now) EndingHelper({1000, 1500, 2300}, PP());
    }
};

代码中通过读取lastState实现了对w8的分类讨论。

收尾段还有一个额外的小问题：如果w8轮到(IPP|)cPPI状态，咖啡豆CD会不够。此时需要特化处理一下这一波，去掉w8的冰，改打cPP|PPIc。为此，需要给IPP状态添加一个WaveIs(8, 18)分支：

// 冰波：IPP-PP 1248
states["hb_IPP"] = {
    Transition(659, delay = "hb_(IPP-)PP", activate = "hb_(IPP|)cPPI", WaveIs(8, 18) = "hb_(IPP|)cPPI_w8", finish = "hb_final"),
    At(1) I(),
    At(459) P(15, 8.325),
    At(1048) PP(8.75), // 1048 = 659 + 389
};
// 如果cPPI波出现在w8，需要调整为cPP|PPIc
states["hb_(IPP|)cPPI_w8"] = {
    Transition(601, finish = "hb_final"),
    At(195) C.TriggerBy(ADANCING_ZOMBIE, ALADDER_ZOMBIE)(40),
    At(next_wave + 401) C.TriggerBy(AGIGA_GARGANTUAR)(800),
};

转白

转白是大部分键控自然出怪阵型都需要考虑的事项。一方面，转白后通常可以省冰、省阳光；另一方面，转白后热过渡意外刷新的概率会明显上升。

首先考虑这个阵的白眼关阵解。打P6的话，每3波有一对多余的炮，因此可以垫两波PPDD一波，就不需要冰了。写成轨道是cPP|PPc|PPDD。

这一部分比红眼关简单得多，就不细讲了，直接上代码：

states["b_PPDD"] = {
    Transition(601, activate = "b_cPP", delay = "b_(PPDD)-PP", finish = "b_final"),
    At(270) PP() & DD<110>(9),
};
states["b_(PPDD)-PP"] = {
    Transition(1202, activate = "b_PPc", finish = "b_final"),
    At(1002) PP(),
};
states["b_cPP"] = {
    Transition(601, activate = "b_PPc", finish = "b_final"),
    At(195) C.TriggerBy(ADANCING_ZOMBIE, ALADDER_ZOMBIE)(40),
    At(389) PP(8.75),
};
states["b_PPc"] = {
    Transition(601, activate = "b_PPDD", finish = "b_final"),
    At(318) PP(),
    At(599) C.TriggerBy(APOLE_VAULTING_ZOMBIE)(1),
};
states["b_final"] = At(-200) Do {
    ATime thisWave = now + 200;
    if (GetCobReadyTime(4) <= 988) {
        // PPDD收尾，DD于788极限全收撑杆
        At(thisWave + 270) PP();
        At(thisWave) EndingHelper({788}, PP());
    } else {
        // cPP-PP收尾
        At(thisWave + 195) C.TriggerBy(ADANCING_ZOMBIE, ALADDER_ZOMBIE)(40);
        At(thisWave + 389) PP(8.75);
        At(thisWave) EndingHelper({1150}, PP());
    }
};

为什么PPDD波反而要考虑延迟？因为这个状态会用在w10，而大波的普僵进场时间非常晚，401时大量铁桶、铁门仍在可伤域外，在无红关很容易造成延迟。

接下来考虑如何从红眼关阵解过渡到白眼关阵解。分类讨论最后一波红眼所在波次：

NDD、(IPP-)PP：本来也要接PPDD，直接转到白眼关阵解的PPDD即可
(IPP-PP-)cPP：这波相比主循环的IPP-PP|PPDD省了一对炮，因此也能转白眼关PPDD
PPDD：下一波还要处理残余2血红，不能直接转入白眼关。可以先打一波PPI作为过渡，然后转白眼关的PPc
IPP：原本要接cPPI，但由于不需要压制下波红眼，可以改打cPP，然后转白眼关PPDD

插一句题外话，虽然这个解考虑了所有状态转白的情况，但如果有的状态不能转，需要接着按原阵解打下一波，状态转移函数也支持这种情况。如果nogiga分支未被指定，则接下来会继续执行activate分支，直到遇到包含nogiga分支的状态为止。

更新后的红眼关阵解如下，增加了nogiga分支和trans_PPI状态：

// 冰波：IPP-PP 1248
states["hb_IPP"] = {
    Transition(659, delay = "hb_(IPP-)PP", activate = "hb_(IPP|)cPPI", WaveIs(8, 18) = "hb_(IPP|)cPPI_w8", nogiga = "trans_cPP", finish = "hb_final"),
    At(1) I(),
    At(459) P(15, 8.325),
    At(1048) PP(8.75), // 1048 = 659 + 389
};
states["hb_(IPP-)PP"] = {
    Transition(1248, activate = "hb_PPDD", delay = "hb_(IPP-PP-)cPP", nogiga = "b_PPDD", finish = "hb_final"),
};
// 加速波：PPDD 601
states["hb_PPDD"] = {
    Transition(601, activate = "hb_IPP", nogiga = "trans_PPI", finish = "hb_final"),
    At(291) PP() & DD<107>(9),
};
// 冰波延迟：IPP-PP-cPP 1739
states["hb_(IPP-PP-)cPP"] = {
    Transition(1739, activate = "hb_IPP", nogiga = "b_PPDD", finish = "hb_final"),
    At(1300) C.TriggerBy(AGIGA_GARGANTUAR & CURR_WAVE)(266),
    At(1539) PP(), // 1539 = 1248 + 291
};
// 冰波意外刷新：IPP|cPPI 659|601
states["hb_(IPP|)cPPI"] = {
    Transition(601, activate = "hb_PPDD", nogiga = "b_PPDD", finish = "hb_final"),
    At(195) C.TriggerBy(ADANCING_ZOMBIE, ALADDER_ZOMBIE)(40),
    At(390) I(),
};
// 如果cPPI波出现在w8，需要调整为cPP|PPIc
states["hb_(IPP|)cPPI_w8"] = {
    Transition(601, finish = "hb_final"),
    At(195) C.TriggerBy(ADANCING_ZOMBIE, ALADDER_ZOMBIE)(40),
    At(next_wave + 401) C.TriggerBy(AGIGA_GARGANTUAR)(800),
};
****
// 转白过渡
states["trans_PPI"] = {
    Transition(601, activate = "b_PPc", finish = "b_final"),
    At(318) PP(),
    At(360) I(),
};
states["trans_cPP"] = {
    Transition(601, activate = "b_PPDD", finish = "hb_final"),
    At(195) C.TriggerBy(ADANCING_ZOMBIE, ALADDER_ZOMBIE)(40),
};

其他

现在只剩w20了！由于ch6冰平衡过于轻松，我们干脆冰消珊瑚好了：~~（才不是因为w19不拖的情况下w20不好打呢）~~

OnWave(20) {
    At(96) I(),
    At(380) P(15, 9), // 热过渡
    At(953) PP(), // 全伤巨人
    At(1220) PP(), // 全伤撑杆
    EndingHelper(PP(), {1600, 2300}),
};

最后还需要启动状态机。红眼关以NDD起手，无红关以PPDD起手：

1
2
3

auto initialState = AGetZombieTypeList()[AGIGA_GARGANTUAR] ? "hb_NDD" : "b_PPDD";
StartTransition(1, initialState);
StartTransition(10, initialState);

完整代码

附赠一个简短的天台十炮脚本，阵解主体只有23行。

总结

本文以双冰16炮键控脚本为例，展示了状态机框架的大部分核心要素。这一方法的主要优势是，使用状态机编写非定态脚本时，只需复制状态机本身的代码，并根据阵解定义新的状态和转移，无需设计复杂的嵌套或回调，也不必写大量重复的刷新检测代码。

键控炮阵冲关仍有一些难点有待解决。以下是我想到的一些，希望本文能够抛砖引玉。

其一是测试较为困难。随机发生的刷新意外和转白波次的不同都会导致轨道改变，因此执行轨迹的种类数会远多于定态演示脚本，人工分析容易有所遗漏。跳帧测试配合回放功能是一个可行的测试手段，但仍然不够高效。

其二是收尾难以系统化。可以看到，文中的阵型完全没有拖收尾。拖收尾是一件很复杂的事，上波残留僵尸、本波出红情况以及场上能垫的位置都需要考虑。笔者暂未想到能够统一大部分阵型收尾的框架。

Lean 4 初体验

发表于 2025-07-21 本文字数： 730 阅读时长 ≈ 3 分钟

第一次不依赖大模型用 Lean 证明了一个没那么显然的定理，在此记录一下。写得很 naive，希望将来自己的水平能有所长进吧。

题目：设 $d(n)$ 表示自然数 $n$ 在十进制下的各位数字之和。证明：对于任意自然数 $n,\,k$，若 $1 \le n \le 10^k$，则有 $d\left(\left(10^k - 1\right) \cdot n\right) = 9k$.

思路：把 $\left(10^k - 1\right) \cdot n$ 拆分为高 $k$ 位和低 $k$ 位两部分。高 $k$ 位的值为 $n - 1$，低 $k$ 位的值为 $10^k - n$。注意到 $(n - 1) + (10^k - n) = 10^k - 1$，因此这两部分的各位数字互补，每一位的数字之和都为 $9$。因此总和为 $9k$。

代码如下：

import Mathlib

def digitSum (n : ℕ) := (Nat.digits 10 n).sum

theorem digitSum_divmod_10 (n : ℕ) :
  digitSum n = digitSum (n / 10) + (n % 10) := by
  by_cases hn : n = 0
  · simp [hn]
  · simp [digitSum]
    rw [Nat.digits_eq_cons_digits_div (by decide) hn]
    simp [add_comm]

theorem digitSum_eq_self_iff (n : ℕ)
  : n < 10 ↔ digitSum n = n := by
  constructor
  · intro hn
    by_cases hn2 : n = 0
    · simp [digitSum, hn2]
    · simp [digitSum, Nat.digits_of_lt _ _ hn2 hn]
  · contrapose!
    intro hn
    apply Nat.ne_of_lt
    rw [digitSum_divmod_10]
    nth_rw 3 [← Nat.div_add_mod n 10]
    calc digitSum (n / 10) + n % 10
      _ ≤ n / 10 + n % 10 := by simp [digitSum, Nat.digit_sum_le]
      _ < 10 * (n / 10) + n % 10 := by
        have : n / 10 > 0 := Nat.div_pos hn (by decide)
        linarith

theorem digitSum_divmod_power_of_10 (n k : ℕ)
  : digitSum n = digitSum (n / 10^k) + digitSum (n % 10^k) := by
  induction k generalizing n with
  | zero => norm_num; simp [Nat.mod_one, digitSum]
  | succ k ih =>
    -- LHS: digitSum n
    -- digitSum n = digitSum n/10^k + digitSum n%10^k
    -- digitSum n/10^k = digitSum n/10^(k+1) + n/10^k % 10
    rw [ih, digitSum_divmod_10]
    rw [Nat.div_div_eq_div_mul, ← Nat.pow_add_one, add_assoc]
    -- RHS: digitSum n/10^(k+1) + digitSum n%10^(k+1)
    -- digitSum n%10^(k+1) = digitSum n%10^(k+1) / 10^k + digitSum n%10^k
    -- n%10^(k+1) / 10^k = n/10^k % 10
    nth_rw 4 [ih]
    have : 10 ^ k ∣ 10 ^ (k + 1) := Nat.pow_dvd_pow _ (Nat.le_add_right _ _)
    rw [Nat.mod_mod_of_dvd _ this]
    rw [pow_succ, Nat.mod_mul_right_div_self]
    nth_rw 4 [(digitSum_eq_self_iff _).mp]
    exact Nat.mod_lt _ (by decide)

lemma complement_divmod_10 {a b k : ℕ} :
  a + b = 10 ^ (k + 1) - 1 ↔ a / 10 + b / 10 = 10 ^ k - 1 ∧ a % 10 + b % 10 = 9 := by
  constructor
  · intro h
    have h2: (a % 10 + b % 10) % 10 = 9 := by
      rw [← Nat.add_mod, h]
      induction k with
      | zero => simp
      | succ k ih =>
        rw [Nat.pow_succ, Nat.mod_eq_sub_iff (c := 1) (by decide) (by decide)]
        rw [← Nat.pow_succ, Nat.sub_add_cancel (Nat.one_le_pow _ _ (by decide))]
        apply Nat.dvd_mul_left
    omega
  · rintro ⟨ha, hb⟩
    rw [← Nat.div_add_mod' a 10, ← Nat.div_add_mod' b 10]
    have : (a / 10 * 10 + a % 10) + (b / 10 * 10 + b % 10)
      = (a / 10 + b / 10) * 10 + (a % 10 + b % 10) := by ring
    rw [this, ha, hb]
    rw [Nat.sub_mul, ← Nat.pow_succ]
    have : 10 ≤ 10 ^ (k + 1) := by apply Nat.le_pow; simp
    rw [← Nat.sub_add_comm this, Nat.add_sub_add_right]

lemma digitSum_eq_9k_of_complement {a b k : ℕ}
  (h : a + b = 10 ^ k - 1) :
  digitSum a + digitSum b = 9 * k := by
  induction k generalizing a b with
  | zero => norm_num at *; simp [digitSum, h]
  | succ k ih =>
    rw [complement_divmod_10] at h
    rw [digitSum_divmod_10 a, digitSum_divmod_10 b]
    rw [mul_add_one, ← ih (h.left), ← h.right]
    ac_rfl

-- For all natural number n, k such that 1 ≤ n ≤ 10^k, show that the digit sum of (10^k - 1)n is 9k.
example (k : ℕ) (n : ℕ) (hn : 1 ≤ n ∧ n <= 10 ^ k) :
  digitSum ((10 ^ k - 1) * n) = 9 * k := by
  -- (10^k - 1) * n = 10^k * n - n = (n - 1) * 10^k + (10^k - n)
  -- divide the digits into two parts：
  -- 1. digitSum ((n - 1) * 10^k) = digitSum (n - 1)
  -- 2. digitSum (10^k - n) = digitSum ((10^k - 1) - (n - 1)) = 9 * k - digitSum (n - 1)
  let x := (10^k - 1) * n
  have hSplit : x / 10^k = n - 1 ∧ x % 10^k = 10^k - n := by
    rw [Nat.div_mod_unique (Nat.pow_pos (by decide))]
    constructor
    · dsimp [x]
      zify [hn.left, hn.right, show 1 ≤ 10^k from Nat.one_le_pow _ _ (by decide)]
      ring
    · exact Nat.sub_lt (Nat.pow_pos (by decide)) hn.left
  rw [digitSum_divmod_power_of_10 _ k, hSplit.left, hSplit.right]
  apply digitSum_eq_9k_of_complement
  rw [← Nat.sub_add_comm hn.left, Nat.add_sub_of_le hn.right]

Vibe Coding 小记

发表于 2025-07-16 本文字数： 1k 阅读时长 ≈ 4 分钟

概述

其后，京兆尹将饰官署，余往过焉。委群材，会众工。或执斧斤，或执刀锯，皆环立向之。梓人左持引，右执杖，而中处焉。量栋宇之任，视木之能举，挥其杖曰：“斧！”彼执斧者奔而右；顾而指曰：“锯！”彼执锯者趋而左。俄而斤者斫，刀者削，皆视其色，俟其言，莫敢自断者。其不胜任者，怒而退之，亦莫敢愠焉。画宫于堵，盈尺而曲尽其制，计其毫厘而构大厦，无进退焉。既成，书于上栋，曰“某年某月某日某建”，则其姓字也。凡执用之工不在列。余圜视大骇，然后知其术之工大矣。
——《梓人传》柳宗元

我花了一周的时间，用 Claude Code 从头搓了一个前端 app。花在项目上的时间大约有 40h。代码总计 14k 行，去除单元测试、注释和空行后约 6k 行。项目的所有代码都是 Claude Code 生成的，我只提供了约 2000 字的初始项目描述和后续开发过程中的 prompt。

总体来说，Claude Code 的表现相当不错，我最担心的界面美观性对它而言其实不是问题。我观察到的比较明显的缺点有：

Token 用量过大：通过 API 高强度使用 Claude Code 的话花费能达到 $5/h 级别，这已经和人类实习生的工资在同一个数量级了。
重构能力较弱：对于较大的项目，Claude Code 很难在重构时追踪到所有需要修改的文件，导致重构很难一遍过，需要反复修正。或许换个 prompt 能好点。
处理复杂功能时表现不佳：我本来想让 Claude Code 实现一个 drag & drop，但它死活写不对，只好先放弃了。

瑕不掩瑜，强烈建议需要大量写代码（尤其是前后端、CLI等典型场景）的人试一试 Claude Code。Claude Pro $20/mo 的订阅价格和它的功能相比非常划算。目前 Claude Pro 提供的额度还是很慷慨的，大概能支撑你每 5h 高强度使用（上一条恢复后立刻开始下一条）2h。低强度使用的话根本不需要担心额度问题。

小技巧

以下是我使用 Claude Code 的过程中摸索出来的一些小技巧。

通知

Claude Code 执行一个任务可能需要几分钟，这段时间一直盯着终端有点浪费时间。可以加个 hook，让它在请求权限或任务完成时发送通知。把以下内容写到 ~/.claude/settings.json 中即可。（非 Linux 系统请自行修改命令）

{
  "hooks": {
    "Notification": [
      {
        "matcher": "",
        "hooks": [
          {
            "type": "command",
            "command": "jq -r \"\\\"notify-send -a 'Claude Code' 'Notification' '\\(.message)'\\\"\" | bash"
          }
        ]
      }
    ],
    "Stop": [
      {
        "matcher": "",
        "hooks": [
          {
            "type": "command",
            "command": "notify-send -a 'Claude Code' 'Task Finished' 'Claude is waiting for your input'"
          }
        ]
      }
    ]
  }
}

Playwright MCP

Playwright MCP 可以让 Claude Code 以 a11y tree 的形式访问网页并操作，这样它就可以自动测试网页了。执行以下命令以添加：

1	claude mcp add playwright -- npx @playwright/mcp@latest --executable-path /usr/bin/chromium --isolated --headless

浏览复杂网页时 token 用量不小，按量计费时需要注意。

Think

在 Claude Code 中，思维链模式需要通过特定关键词触发。

These specific phrases are mapped directly to increasing levels of thinking budget in the system: "think" < "think hard" < "think harder" < "ultrathink." Each level allocates progressively more thinking budget for Claude to use.

在实现复杂功能之前，开启 plan mode 并加入 ultrathink 关键词可以让 Claude Code 先思考出一个详细的计划。

中途输入

你可以在任何时刻向 Claude Code 提供输入，它会在完成下一次工具交互后读入这些内容。比如你发现它犯错后，你可以及时纠正，而不需停止整个任务。

继续对话

claude --resume 可以选择一个之前的对话继续进行。claude --continue 会继续最近的对话。

过长的对话会增大 token 用量。适时清空上下文或者使用 /compact 命令可以减少花费。

软件工程

TBD

华中科技大学篮球（四）慕课答案

发表于 2025-05-22 更新于 2025-06-04 本文字数： 2.4k 阅读时长 ≈ 9 分钟

这门课有点离谱，很多题没有唯一客观答案，还不对应视频原文。本人用了一些奇怪的方法才试出答案。

二三联防

篮球23区域联防通常适用于哪种情况？
对方投篮能力差或陷入低迷
在篮球比赛中2-3区域联防战术的核心目的是什么？
保护篮下，限制对方内线得分
区域联防战术中，防守队员主要依据什么来判断自己的防守位置？
球的位置
篮球2-3区域联防的优点包括哪些？
压迫感强，给对方造成心理压力
容易造成对方失误
限制对方突破和中距离投篮
篮球2-3联防的应用场景包括哪些？
面对拥有身高和体型优势的内线球员时
比赛关键时刻需要加强防守时

进攻二三联防

攻2-3联防时，哪种方式最能有效破解上线防守？
切入并传球给空位球员
进攻2-3联防时，以下哪项是球员最需要避免的？
忽视与队友之间的配合
当后卫发现低位防守队员补防时，应如何应对？
观察场上形势，选择传球或突破
进攻2-3联防时，如何利用对方的防守空隙？
多传球，制造进攻方人数多于防守方的局面
在进攻2-3联防时，以下哪些策略是有效的？
利用外线投射能力强的球员吸引防守
保持进攻节奏，避免被防守打乱
加强内线的篮下进攻

身体素质（上）

坐姿臂屈伸动作是练习（）非常有效的动作之一。
肱三头肌
我们在做壶铃甩摆练习时，通过伸髋肌群发力将壶铃甩出，在髋关节完全打开时，壶铃应该甩至与（）齐平高度。
眼睛
篮球运动专项身体素质训练可以保证运动员掌握有难度的动作技术质量，提高我们的（），培养我们优良的作风和顽强的意志品质，增强篮球比赛的对抗性和观赏性。
竞技水平
延长运动寿命
应变能力
减少运动创伤
我们可以通过（）动作来进行下肢力量训练。
哑铃前蹲
壶铃甩摆
保加利亚分腿蹲
我们可以通过（）动作来进行核心力量训练。
仰卧卷腹抛接球
仰卧卷腹
坐姿卷腹
仰卧负重卷腹

半场人盯人防守

人盯人防守战术中，防守队员主要盯防的是？
各自负责的进攻球员
在人盯人防守中，当对手运球突破时，防守球员应：
跟随对手，尽量干扰其运球和突破
在人盯人防守中，防守队员应如何调整自己的防守位置？
随时注意人、球、对手、篮圈的方位
在人盯人防守中，当防守无球队员时，防守队员应主要注意什么？
对手的跑动方向
人盯人防守的基本要求包括哪些？
人球兼顾
盯人为主
控制对手

进攻半场人盯人防守

进攻半场人盯人防守战术打法的基础是（）之间的进攻配合。
两三名队员
进攻半场人盯人防守的方法，应根据全队，特别是（）的身体、技术条件情况来确定。
中锋
‌进攻半场人盯人时要先确定进攻的（），选择适合队伍的进攻落位。常用的落位阵型有1-2-2、1-3-1、2-3等。
区域与结构
进攻半场人盯人防守，常见的战术打法有：
通过中锋打法
移动进攻打法
综合性进攻打法
进攻半场人盯人防守是由哪些配合来组织全队进攻战术的？
突分
策应
掩护
传切

身体素质（中）

三人直线快攻（往返）是一种（），将多种基础练习综合起来进行循环练习。
高强度间歇训练
运动员进行低强度、长时间不间断的训练方法，主要目标是提高（）和发展基础有氧代谢能力。
心肺功能
有氧耐力和无氧耐力是两种不同的体能素质，主要区别在于（）。
运动方式
运动时间
供能方式
锻炼效果
下列哪几个项目属于柔韧练习。
伸展运动
坐位体前屈
灵敏素质是指在各种突变条件下，运动员（）的能力，是复合素质的综合表现。
随机应变
转换动作
改变体位

全场紧逼人盯人防守

全场紧逼人盯人防守时，防守队员应如何利用场地空间？
分散在场地的各个角落
全场紧逼人盯人防守时，要求防守球员要有充分的体力与信心，（）及其顽强拼搏作风。
速度快、反应灵敏
在全场紧逼人盯人防守中，防守球员对持球者的逼抢主要是为了
制造对手失误
全场紧逼人盯人防守的优势在于：
使进攻方难以组织有效的进攻战术
限制对手的传球和移动
消耗防守队员体力
制造对手失误，增加抢断机会
‍全场紧逼人盯人防守是以个人防守为基础，综合运用（）等防守基础配合所组成的全队防守。
夹击
关门
换防
挤过

进攻全场紧逼人盯人防守

进攻全场紧逼人盯人防守时，以下哪项策略是有效的？
减少个人运球，多利用团队配合
破解全场紧逼人盯人防守时，球员之间应该如何配合？
保持适当的间距，以便传球和移动
在进攻全场紧逼人盯人防守时，接应队员积极跑动的正确做法是？
快速而准确地移动，以制造进攻方人数多于防守方的局面
在进攻全场紧逼人盯人防守时,接应队员要把握（）的配合原则，尽量减少传接球的失误，为全场进攻建立基础。
横向跑动与纵向传接球
在进攻全场紧逼人盯人防守时，以下哪些策略是有效的？
保持球员之间的间距，以便传球和移动
快速转移球权，避免长时间持球

身体素质（下）

下列拉伸动作中，主要拉伸大腿后侧肌肉的动作是（）。
腿后侧拉伸
做屈肘水平外展动作过程中，要求（）肌群要放松，保持收腹挺胸。
颈部
柔韧素质是指人（）的伸展能力。
肌肉
关节活动幅度
韧带
柔韧训练可分为（）等练习方式。
主动性
被动性
混合性
做弓箭步转体练习时，前腿屈膝形成前弓步，后腿跟随屈膝90°，同时手臂水平举后，前弓步腿的同侧手臂向后旋，带动（）向后转直至达到最大幅度。
头部
上身

期末测试

在2-3联防时，外线防守队员应如何对待突破能力强的对手？
保持距离，等待协防
进攻2-3联防时，哪种战术可以制造进攻球员多于防守球员的局面？
Motion Offense（流动进攻）
仰卧卷腹训练时，由（）发力将上体卷起，同时双臂随身体向前伸，直至指尖能够触及到脚。
腹部肌群
全场紧逼人盯人防守战术是与对方在（）展开全面激烈的争夺。
全场
在全场紧逼人盯人防守中，如何有效限制对手的传球？
全体球员收缩防守，减少传球空间
切断传球路线，迫使对手失误
有氧耐力通常指运动员长时间进行低强度运动的能力，主要目标是提高（）和发展（）能力。
基础有氧代谢
肌肉力量
进攻2-3联防时，以下哪些注意事项是正确的？
保持球的移动，避免停滞不前
外线球员应随时准备接球并投射
球员之间应保持良好的沟通，协同作战
以下哪项是人盯人防守的注意要点？
防守时以人为主，人球兼顾
防守时应尽量靠近对手，不给其投篮或传球的空间
防守无球队员时，主要任务是防止对手接球
进攻半场人盯人时要选择适合队伍的进攻落位，常用的落位阵型有（）
2-3
1-3-1
1-2-2
破解全场紧逼人盯人防守时，以下哪些做法有助于提升进攻效率？
保持球员之间的默契和沟通
快速而准确地做出进攻决策

黑科技：如何向 Transformers 中的模型传递注意力掩码矩阵

发表于 2025-04-09 本文字数： 585 阅读时长 ≈ 2 分钟

由于 Transformer 本质上是位置无关的，因此通过正确设置 positional embedding 和 attention mask，我们可以把多个“序列”合并到一个序列里进行推理。当这些序列具有很长的公共前缀时，这种方法会比 batched inference 更高效。这种方法的具体用途不是本文的重点，此处不做展开。

图片出自 SpecInfer: Accelerating Generative Large Language Model Serving with Tree-based Speculative Inference and Verification

但是，Transformers 库的自带 API 并不支持传递 attention mask 矩阵，而只支持选择是否 mask 掉整个 token（这种 mask 是用来处理 padding 的）。一种常见的解决方法是直接修改模型的代码，比如 REST 的实现。显然，这种方法在需要测试多种模型时会很麻烦。

有没有更通用一点的方法呢？有的！通过阅读源码可以发现，当模型把 2d 的 attention mask（这个参数是从 forward 一路传过来的）转化为 4d 时，如果输入已经是 4d 的话，这个函数会直接返回输入。因此通过这个不在文档里的 API，就可以传递 attention mask 矩阵了。

代码大概是这样的：（注意传入的 mask 值应为 -inf/0 而非 0/1）

import torch
from transformers import AutoModelForCausalLM, AutoTokenizer

# Load model
model_name = "Qwen/Qwen2.5-0.5B-Instruct"
model = AutoModelForCausalLM.from_pretrained(model_name, device_map="auto")
tokenizer = AutoTokenizer.from_pretrained(model_name)

# Create test input
message = "You are a are not a"
message_tokenized = tokenizer.encode(message, return_tensors="pt").to(model.device)
assert message_tokenized.shape[-1] == 6

# Create position_ids and attention_mask according to the tree structure
position_ids = torch.Tensor([[0, 1, 2, 1, 2, 2]]).long().to(model.device)
attn_mask_bool = torch.Tensor([[[
    [1, 0, 0, 0, 0, 0],
    [1, 1, 0, 0, 0, 0],
    [1, 1, 1, 0, 0, 0],
    [1, 0, 0, 1, 0, 0],
    [1, 0, 0, 1, 1, 0],
    [1, 0, 0, 1, 0, 1],
]]]).bool()
attn_mask_float = torch.where(attn_mask_bool, 0.0, -torch.inf).to(model.device)
print("position_ids:", position_ids.shape)
print("attn_mask_float:", attn_mask_float.shape)

r'''
树的结构：
        - are ----- a
       /
You ---           - not
       \         /
        - are ---
                 \
                  - a

如果实现正确，两个 "are" 和 "a" 的 logits 应该相同
'''

# Run model
with torch.no_grad():
    outputs = model(
        message_tokenized,
        position_ids=position_ids,
        attention_mask=attn_mask_float
    )
logits = outputs.logits
print("logits:", logits.shape)
print(f"{torch.allclose(logits[0, 1, :], logits[0, 3, :])=}")
print(f"{torch.allclose(logits[0, 2, :], logits[0, 5, :])=}")

输出为：

position_ids: torch.Size([1, 6])
attn_mask_float: torch.Size([1, 1, 6, 6])
logits: torch.Size([1, 6, 151936])
torch.allclose(logits[0, 1, :], logits[0, 3, :])=True
torch.allclose(logits[0, 2, :], logits[0, 5, :])=True

这种方法的优点：

对大部分 Transformer 模型即插即用
不需要深入模型的实现细节

这种方法的缺点：

不是官方支持的 API，随时可能失效
不支持 Flash Attention 2

实用工具

发表于 2025-01-19 更新于 2025-03-28 本文字数： 533 阅读时长 ≈ 2 分钟

收录了一些博主喜欢的实用工具。本页面不定期更新。

计算

Qalculate!

功能非常全面且设计合理的 PC 端计算器。（高级计算器和编程语言之间并没有明确的区隔；由于它很重视 fuzzy parsing，所以我还是将其算作计算器）

支持的特性非常多，比如大量非初等函数、简单的符号计算、不确定度传播、单位转换等等。详见官方示例。

IPython

博主在科学计算方面基本只会 Python 生态，会用 MATLAB 或 Mathematica 的人可以忽略此节。

Python 自带 REPL 的上位。支持保存历史记录、语法高亮~~以及用·exit 而非 exit() 退出~~等。其中一部分功能也添加到了 Python 3.13 的新 REPL 中。

IPython 还支持一些拓展语法。博主比较常用的有：

按 Ctrl+R 可以搜索历史记录
函数/类名后加 ? 可以查看其帮助文档
Tab 补全可以补全目录/文件名
全局变量 _ 可以访问上一个返回值，Out[i] 可以返回第 i 个语句（块）的返回值

Plotly

比 Matplotlib 更现代的 Python 绘图库。这个库视 DataFrame 为一等公民，而且默认就能生成美观的交互式图表，适合 prototyping。

美中不足的是深度定制样式还是不如 Matplotlib 方便，毕竟后者资料太多了。而且现在有大模型。

网页小工具

Pastebin

无需注册，支持不超过 50MB 的二进制文件，可以直接 POST/GET 的 pastebin。

最朴素的就是最好用的。

Windows 工具

PowerToys

由微软官方开发的一组 Windows 上的奇怪小工具。本人用它把 CapsLock 键改成了 Backspace~~（因为我打字准度太差了~~

AutoHotkey

用于操作自动化的脚本语言，可以写一些快捷键什么的。其实拿来写游戏的挂机脚本都可以，就是满屏 ImageSearch 啊 Click 啊可维护性太差了。

WizTree

可以非常快速地统计出磁盘占用的树形结构，清理磁盘空间时很有用。

功能测试

发表于 2024-07-04 更新于 2024-12-22 本文字数： 244 阅读时长 ≈ 1 分钟

LaTeX

\[\int_{0}^{1}\!x^{-x} \mathrm{d}x = \sum_{n=1}^{\infty}n^{-n}\]

$\int_{0}^{+\infty}\!\sin(x^2) \mathrm{d}x = \sqrt{\frac{\pi}{8}}$

\[\mathit{mathit} \quad \mathrm{mathrm} \quad \mathcal{mathcal} \quad \mathscr{mathscr} \quad \mathbb{mathbb} \quad \mathfrak{mathfrak}\]

\[\mathit{MATHIT} \quad \mathrm{MATHRM} \quad \mathcal{MATHCAL} \quad \mathscr{MATHSCR} \quad \mathbb{MATHBB} \quad \mathfrak{MATHFRAK}\]

\[\mathit{01234} \quad \mathrm{56789} \quad \mathcal{01234} \quad \mathscr{56789} \quad \mathbb{01234} \quad \mathfrak{56789}\]

\[2.71828\,18284\,59045\,23536\,02874\,71352\,66249\,77572\,47093\,69995\,95749\,66967\,62772\,40766\,30353\,54759\,45713\,82178\,52516\,64274\]

代码块

(* take first n elements from list xs *)
let take n xs =
  let rec take_impl acc n xs = match (n, xs) with
    | (0, _) -> acc
    | (_, []) -> acc
    | (n, x::xs) -> take_impl (x::acc) (n-1) xs
  in List.rev (take_impl [] n xs)

(* drop first n elements from list xs *)
let rec drop n xs = match (n, xs) with
  | (_, []) -> []
  | (0, xs) -> xs
  | (n, _::xs) -> drop (n-1) xs

Copied from lipsum.com

Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat.

Mermaid 图

sequenceDiagram
    Alice->>John: Hello John, how are you?
    John-->>Alice: Great!
    Alice-)John: See you later!

折叠

不要点开

Hidden text

LLM 学习笔记（二）：从头训练 LLM 的简要流程

发表于 2024-10-11 本文字数： 1.6k 阅读时长 ≈ 6 分钟

本章以 Llama 3 为讨论对象。

2.1 模型设计

Llama 3 的模型架构较为常规，但值得一提的是其模型尺寸的选择。Llama 3 的旗舰版本是 405B 而非常见的 70B，这一选择是经过了充分分析和论证的。

给定总计算量（这直接由预算决定），Llama 团队希望训练出一个尽可能强的模型。盲目增加参数量并不是最优解：增加参数意味着减少训练数据量，而一个欠拟合的大模型未必比一个充分拟合的较小模型更优。DeepMind 团队在 2022 年研究了该问题。这篇文章在固定总计算量的条件下训练了大量不同尺寸的 LLM，并观察到（最小化 loss 意义下的）最优模型尺寸与总计算量之间存在与数据相当吻合的经验关系。Llama 3 沿用了这一方法，但重做了其中的实验。实验得出的数据与原文有差异，但结论是一致的。405B 的选择正是根据这项数据外推得来。

图片出自 Training Compute-Optimal Large Language Models

作者曾经读到过一句话：“工程师是能用最低限度的创新达成目的的人。”Llama 3 正是这样：其成功的最主要原因并非其方法论所含的原创性，而是大量人力、算力资源的投入以及对现有 best practice 的有效整合。这样的工作是否预示着在不久的将来，深度学习领域“单打独斗”的时代将会迎来结束？这是一个引人遐想的问题。

2.2 Pre-training

Llama 3 的预训练分为三个步骤：初始训练、上下文增长和 annealing（冷却？）。

2.2.1 初始训练

训练由一个较短的预热阶段（学习率线性增长）和一个较长的主阶段（学习率余弦衰减）组成。模型初始阶段很不稳定，因此使用更低的学习率和更小的 batch size 以保证梯度在合理范围内，使模型的学习更加可控。

值得一提的是，训练数据不仅在内容上进行了多方面的把控，不同类型数据的配比也是刻意调整优化过的。得益于 scaling law，小模型上的实验结果可以较为可靠地迁移到大模型上，使得对训练数据配比的调优成为可能。~~展现了深度学习中炼金术的一面~~

2.2.2 上下文增长

由于 transformer 模型的算力消耗随输入长度是超线性增长的，以超长上下文训练会拖慢训练效率。因此，模型在初始训练阶段以 8K 上下文长度进行训练，训练好之后逐步增长到 128K。

用于监控训练进程的指标是原长度下的表现和新长度下 needle in a haystack 测试的成功率。当模型 100% 完成 needle in a haystack 任务，且在原长度下的表现恢复到训练前水平时，即认为模型适应了新的上下文长度，接下来再进行下一轮上下文增长，直到达到最终的 128K。

2.2.3 冷却

在以上两个阶段后，还会再进行一个较短的冷却阶段（学习率线性衰减）。这一阶段使用精选的高质量数据进行训练。~~这或许是 LLM 版的“考前冲刺”？~~

2.3 Post-training

经过 pre-training 后，模型具有了理解语言的能力，但它只学习了文本续写这一项任务。想要让模型顺利地和人类对话，还需要作出一定微调。

2.3.1 Instruction Tuning

首先，需要规定一种用于对话的格式，以便 LLM 知道上文的每一部分都来自于谁（系统/用户/LLM/工具...）。以 Llama 3.1 为例，一个简单的 prompt 如下：（形如 <|begin_of_text|> 的为特殊 token）

<|begin_of_text|><|start_header_id|>system<|end_header_id|>

Cutting Knowledge Date: December 2023
Today Date: 23 July 2024

You are a helpful assistant<|eot_id|><|start_header_id|>user<|end_header_id|>

What is the capital of France?<|eot_id|><|start_header_id|>assistant<|end_header_id|>

定义了对话格式后，需要在对话数据上微调 LLM。对话数据可能来自于人，也可能由已经 post-training 过的 LLM 生成。

2.3.2 偏好学习

仅仅在格式上让 LLM 适配对话是不够的。互联网上存在大量的低质量内容，也包含很多我们不希望 LLM 去模仿的行为（如恶意言论）。因此，需要让 LLM 学习在人类看来更加“正确”的行为，而非无意识地模仿互联网上的内容。

构建高质量的对话数据集是较为困难的。但是还有一种相对容易的获取人类偏好的方式：让人类比较对同一问题的两个回答孰优孰劣。模型通过某种方式的学习，提高生成较优答案的概率，降低生成较劣答案的概率，从而实现适配人类偏好的效果。

~~受限于作者的数学水平，~~本节只概括性地描述偏好学习的理念，不涉及具体细节。

一个典型的 RLHF (Reinforcement Learning from Human Feedback) 流程如下：

收集偏好数据。一条偏好数据是形如 $\mathrm{(input,\,output\_win,\,output\_lose)}$ 的三元组。
根据偏好数据训练一个模型（通常是 LLM 附加一个分类层），用于给 $\mathrm{(input,\,output)}$ 对打分。训练时最大化打分和偏好数据的吻合程度（给 $\mathrm{output\_win}$ 高分，给 $\mathrm{output\_lose}$ 低分）。这个模型被称为 reward model。
以 reward model 为指导微调模型。这一步最大化模型输出在 reward model 上的得分，同时通过一个惩罚项避免模型偏离太远。由于 reward model 并不可微，这一步无法使用梯度下降法。通常使用强化学习领域的 PPO 算法进行优化。

PPO 过程较为繁琐，需要训练辅助模型和使用相对复杂的优化算法。DPO 通过一些数学上的调整，在保留原本算法的优秀性质的同时不再需要 reward model 和强化学习，而是直接更新模型参数。DPO 的复杂性显著低于 PPO，同时性能接近或更优。

前言

题目