> For the complete documentation index, see [llms.txt](https://www.daiwk.net/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://www.daiwk.net/6.llm_math.md).

# 6.llm\_math

## 线性代数(linear algebra)

[MIT Gilbert Strang系列视频](https://www.bilibili.com/video/BV1rH4y1N7BW/?spm_id_from=333.788.videopod.episodes\&vd_source=1ae2f94a63a5ab75ddbbb426fa107515\&p=3)

### lecture1 方程组的几何解释

如下的二元一次方程组，可以写成矩阵的形式，$$A$$是系数矩阵，$$\mathbf{x}$$是未知数列向量，$$b$$是结果向量

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-df5f5e49933d2d3af52b2cc699b4e90afe501ff3%2Flinear-equations-matrix.png?alt=media)

行图像：就是2条直线求交点

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-7819872479917cc13a0c05629f22b47f011f9bc1%2Frowpicture.png?alt=media)

列图像：求解两个列向量的线性组合

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-4d23f49c0bb60dcc801cb6346341ed068aee4c4e%2Fcolumnpicture1.png?alt=media)

col1和col2的线性组合，要得到$$\[0,3]$$这个向量。我们已经知道答案是$$\[1,2]$$，所以从col1的尾部，画一个2倍col长度的向量，得到一个点，从原点连过来刚好就是$$\[0,3]$$这个向量

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-1c0b5f8c7a8c393e8e60adc09a75acae589de0ba%2Fcolumnpicture2.png?alt=media)

注意，向量平移，结果还是它本身，即上面从col1尾部画向量那一步

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-24615edfedb64ae190fe67d49c67c4d10844261c%2Fvec-move.png?alt=media)

如果是三元方程组，从行图像的角度来讲，那就是3个平面，前2个相交是一条直线，和第3个再相交就是一个点

从列图像来讲，就更简单一点了，还是3个向量的线性组合，只不过换成了3维空间

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-43d30bbd71dd1a5964a4773567f768d83cf0cc24%2Fcolumnpicture-3d.png?alt=media)

对于任意一个$$b$$，是否都能求解$$Ax=b$$？(如果有，消元法就能求解)

这个问题就转化成，列向量的线性组合是否可以覆盖整个3维空间？

答案：对于可逆矩阵（非奇异矩阵），可以；如果3个列向量在同一平面上，不行，这种情况叫奇异矩阵(不可逆)

矩阵乘向量的列视角：$$Ax$$是$$A$$各列的线性组合

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-675ca8a497e71a9e9a8da65008d431e8caedf2df%2Fmat-mul-vec-colview.png?alt=media)

### lecture2 矩阵消元

先选中第1行第1列为主元（pivot），其所在的行不变，乘以一个消元系数（图中的3），然后被第2行减掉（即$$R\_2 \leftarrow R\_2-3 R\_1$$），让第2行的pivot对应的元素变成0；然后对第3行也这么做

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-2599eb7f6d92c140b75435845dd745585bd58d9c%2Felimination1.png?alt=media)

然后第2行第2列为主元，消掉第3行

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-d94e5ac00f7247fe972ed869f9583bf4e71bc05e%2Felimination2.png?alt=media)

这样矩阵消元最后得到的就是一个**上三角矩阵**（左下角全0，右上角非0），这是计算机中最常见的运算，人们在想各种加速方法。

另外矩阵的行列式正好等于主元的积

注意，主元不能是0，这个矩阵很好，刚好主元都没有0。特殊情况：

1. 第1个主元是0，不代表不行，可以交换矩阵的行再继续
2. 但如果下面的元素也全是0，那就没法交换了，消元就失效了

接下来把b拼进去（增广矩阵），然后一起消元，就可以得到下图

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-7007f581171dfb35123134732a2e3728c1c772ea%2Felimination3.png?alt=media)

然后还原成方程组，发现第3行只有z，那么从下往上依次求解z、y、x就行了（代入，substitution）

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-07d6228a7fd6f4d3debe319cd930d85a281bbcfa%2Felimination4.png?alt=media)

向量乘以矩阵的行视角：向量的每个元素对矩阵每一行的线性组合

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-1b9a0ddb289abef774550db5564a1c5687adb33f%2Fvec-mul-matrix-row-view.png?alt=media)

接下来从矩阵的视角来理解消元，目标是找到一个矩阵，使得原矩阵第2行变成它减掉3倍的第1行，然后第1和第3行不变：

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-7293fb5b766e7717b28a146a7832c07c703729f0%2Felimination-matrix-view.png?alt=media)

第1行是1 0 0，因为只要右边的第一行，别的不要；第3行是0 0 1，因为只要第3行；第2行是-3 1 0，因为第一行的-3倍，加上行2行原始值；这个矩阵叫$$E\_{21}$$，因为是要把第2行第1列变成0

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-48c071f23955cf3ea8753630092869c08d007ffc%2Felimination-matrix-view2.png?alt=media)

同理，第3行减掉2倍的第2行，就得到下图

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-4a03f750c44d1bb2f1e4f9d23ae764729ef462a2%2Felimination-matrix-view3.png?alt=media)

最终就有$$E\_{32}(E\_{21}A)=U$$，但如何一次性从$$A$$到$$U$$？结合律(associative law)：$$(E\_{32}E\_{21})A=U$$

置换矩阵（permutation matrix）：交换两行的位置，可以看到就是个类似单位矩阵的东西

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-e752d389d53877b14994c970aaf529c07e1ee5b9%2Fpermutation-rows.png?alt=media)

但如果要交换列呢？P矩阵要放右边：

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-5e892de5be7284abcab7ca17cea335f8fe76fb67%2Fpermutation-cols.png?alt=media)

倒回来看那个$$E\_{21}A=U$$，如果我想变回去，即把U变回A，那就是$$?E\_{21}A=A$$，即$$?E\_{21}=I$$，其实就是求逆。因为我们$$E\_{21}$$是第2行减去第1行的3倍，那其实就是逆向操作，即第2行不变，加回第1行的3倍就行了，不要第3行

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-870a3dd1b003db79cebb3128ec8377ef77d5ebef%2Finverse-intro.png?alt=media)

### lecture3 矩阵乘法和逆

一些有趣的性质：$$AB=C$$

* 列的角度：

矩阵$$B$$有好几列，取其中一列出来，这列的每个元素作为权重，去和$$A$$里每一列相乘，再相加，就得到$$C$$的这一列（就是**对A中所有列的线性组合**）

$$
A
\begin{bmatrix}
x\y\z
\end{bmatrix}=
x(A\text{第1列})
+y(A\text{第2列})
+z(A\text{第3列})
$$

$$
(AB)*{:,j}=\sum *k b*{kj}A*{:,k}
$$

* 行的角度：

矩阵$$A$$有好几行，取其中一行出来，这行的每个元素作为权重，去和$$B$$里每一行相乘，再相加，就得到$$C$$的这一行（就是**对B中所有行的线性组合**）

$$
\begin{bmatrix}
x\&y\&z
\end{bmatrix}
B=
x(B\text{第1行})
+y(B\text{第2行})
+z(B\text{第3行})
$$

$$
(AB)*{i,:}=\sum *k a*{ik} B*{k,:}
$$

* 外积的角度

$$A$$的第$$k$$列乘以$$B$$的第$$k$$行，得到一个外积矩阵，再把所有外积矩阵加起来。

$$
AB=\sum *k A*{:,k} B\_{k,:}
$$

* 分块乘法

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-bd7e39a2d02c3be56e3197e7c1123dddbabf4417%2Fblock-mul.png?alt=media)

方阵的左逆=右逆，非方阵没这个性质，因为shape不一样 可逆、非奇异

行列式=0的矩阵(奇异矩阵)没有逆

$$
A=\begin{bmatrix}
1&2\\
3&6\\
\end{bmatrix}
$$

这个矩阵没有逆

解释1：因为这两列是平行的，不论如何线性组合都是平行于$$\begin{bmatrix} 1\ 3\ \end{bmatrix}$$那条线的，没法和$$\begin{bmatrix} 1\ 0\ \end{bmatrix}$$有交点

解释2：如果能够找到一个非0向量$$x$$，使得$$Ax=0$$，那么$$A$$没有逆。证明：

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-1e108955e8f723c92e6383557c22745409032d87%2Fproof-no-inverse.png?alt=media)

\==>不可逆矩阵、奇异矩阵，其列能通过线性组合得到0

如何求逆？高斯-若尔当（Gauss-Jordan）消元法：同时求解2个方程组

增广矩阵的思想，把单位矩阵增广进去，然后进行消元，把左边变成单位矩阵，而右边就变成了逆矩阵

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-43836784eff4b35d2c8fbd95a712beee0dc739f3%2Fgauss-jordan.png?alt=media)

为什么？如上消了2次，总的消元矩阵假设是$$E$$

$$E\[A I] = \[I E]$$, 而$$EA=I$$，说明$$E=A^{-1}$$，所以最右边那个矩阵就是$$A^{-1}$$

### lecture4 矩阵A的LU分解

如果$$A$$和$$B$$的逆均已知，那么$$AB$$的逆是多少？是$$B^{-1}A^{-1}$$，因为结合律$$(AB)(B^{-1}A^{-1})=A(BB^{-1})A^{-1}=I$$

如何求$$(A^T)^{-1}$$？因为$$AA^{-1}=I$$，两边同时转置，就有$$(A^{-1})^TA^T=I$$，所以$$(A^T)^{-1}$$就是$$(A^{-1})^T$$

\==>转置和逆这两种运算，对于同一个矩阵，顺序可以互换，即$$(A^T)^{-1}=(A^{-1})^T$$

考虑如下情况，之前学的消元，把第2行第1列消成0：

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-4c7223f7bb12f820593346b8d0574440435900e0%2Flu1.png?alt=media)

然后左右各乘一个$$E\_{21}$$的逆（第一行不变，第二行把-4变回4），这样就有如下的图的第一行，可以发现第一个是下三角矩阵（lower, L），第二个是上三角矩阵（upper, U）

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-504df98947abdff03e6ee90cc7642510fed2ddcf%2Flu2.png?alt=media)

而第二行是对U矩阵进行变换，想加一个对角矩阵进来，那就可以算出第3个矩阵。第1个还是下三角，第2个是对角矩阵，第3个还是上三角

接下来看3x3的矩阵，假设没有行交换，需要进行3步：$$E\_{32}E\_{31}E\_{21}A=U$$，所以$$A=E^{-1}*{21}E^{-1}*{31}E^{-1}*{32}U=LU$$，这里的$$L$$就是$$E*{32}E\_{31}E\_{21}$$这个乘积的逆

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-3b20dd6bca7ebd6cca2fd353f0c85717ae124d23%2Flu3.png?alt=media)

可以发现，对于$$A=LU$$，如果没有行交换，那么$$L$$是下三角，对角线是1，下面的元素是消元所用的乘数，且$$U$$是上三角，主对角线是主元即下图

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-ca12ba8c591ce5e454fc99cf334567dbb15f9ab6%2Flu%E6%80%A7%E8%B4%A8.png?alt=media)

对于一个$$n \times n$$的矩阵，消元需要进行多少次操作？假设n=100

第一次变换是把第1行第1列(主元)下面的那一列全变成0，即第一行确定了，第一列确定了，剩下的是一个$$99\times 99$$的矩阵。这一次变换是对第i行乘一个数，然后被第2行减，假设乘+减算一次操作，这里对99行做了这个操作，所以就是$$99\times 100$$，大概是$$100^2$$的量级

第二次变换就是$$99^2$$的量级，以此类推，总共就是$$n^2+(n-1)^2+...+1^2$$，由于这里是递减的，大概是$$1/3n^3$$的量级。为啥是$$1/3$$？要用微积分，因为这个其实就是对$$y=x^2$$在x=1到n的曲线下方面积，可以拆成n个小长方形面积求和，即对$$x^2$$求积分就是$$1/3x^3$$。因为微积分就是对连续的情况下的求和，而线性代数是离散的

以上是对A的操作次数，如果对增广矩阵中的b(右侧向量)呢？因为b就一列，所以这里是$$n^2$$次

### lecture5 转置、置换和向量空间

接下来讨论可以进行行交换的场景，即主元位置存在0的情况，$$A=LU$$就变成了$$PA=LU$$，即对于任意可逆矩阵$$A$$，均有$$PA=LU$$

置换（permutation）：从单位矩阵出发，对其**行进行交换**，可以得到$$A\_n^n=n!$$个置换，它们的逆就在这些置换矩阵之中(其实就是它的转置)，它们的转置也在这些置换矩阵之中，它们的两两的乘积也在置换矩阵之中，这就构成了一个矩阵乘法运算下的群。

性质：$$P^{-1}=P^T$$，然后就有$$P^TP=I$$

转置（transpose）：行列互换，即$$(A)^T\_{ij}=A\_{ji}$$

对称矩阵（symmetric）：转置后还是本身，即$$A^T=A$$

定理：对于任意一个矩阵$$R$$，$$R^TR$$是一个对称矩阵。

因为转置后的第i行=现在的第i列，转置后的第j行=现在的第j列，结果矩阵的第i行第j列=转置后的第i行和现在的第j列的内积，结果矩阵的第j行第i列=转置后的第j行和现在的第i列的内积=现在的第j列和转置后的第i行的内积，所以这两个相等，所以是对称矩阵。

证明：假设$$A=R^TR$$，$$(R^TR)^T=R^TR$$，即$$A^T=A$$

向量空间：$$R^n$$是所有n维实数列向量

举例：$$R^2$$是所有2维实数向量，即一个x-y plane(平面)，注意，不能没有原点，因为需要0乘以任何向量都=0向量，两个相反的向量加起来要是0。

性质：

1. 任意2个向量之和还在空间中
2. 数乘某向量仍在空间中
3. 可以从前2个推导出来：向量的线性组合仍在空间中

子空间(subspace)：空间里的空间

例如，$$R^2$$中的任意一条直线并不是子空间，它的子空间包括：

1. $$R^2$$自己
2. 穿过原点的任意一条直线，通常叫$$L$$
3. 一个点，即0向量，原点（origin），通常叫$$Z$$

以此类推，$$R^3$$的子空间有$$R^3$$、穿过原点的平面$$P$$，穿过原点的直线、原点

矩阵的子空间：对于一个矩阵$$A$$来讲，其任意2个列向量的线性组合都要在这个空间里，称为列空间（$$C(A)$$）。例如下面这个3行2列的例子，其子空间就是经过原点的那个平面。当然，如果这2个向量刚好共线，那得到的就是一条直线

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-0b7a2ddc38c569677973bf2142d5ef9af197c48b%2Fcolspace.png?alt=media)

### lecture6 列空间和零空间

给定2个子空间$$P$$（平面）和$$L$$（直线），它们的并集也是子空间吗？并不是，因为如果从$$P$$和$$L$$中各取一个向量，他们的和并不在$$P$$或者$$L$$中，即加法不封闭。

如果是交集呢？是，因为交点是原点

如果是更通用的情况，两个子空间$$S$$和$$T$$，$$S\cap T$$还是子空间吗？

是，因为假设从$$S\cap T$$中取出2个向量$$v$$和$$w$$，所以这2个向量都在$$S$$中，而$$S$$是子空间，所以$$v+w$$也在$$S$$中，同理，这两个向量也在$$T$$中，所以和也在$$T$$中，也就是在$$S\cap T$$ 中。

矩阵的列空间：对于一个矩阵$$A$$来讲，其列空间（$$C(A)$$）由所有列的线性组合构成。

从解方程的角度来看，$$Ax=b$$对于任意的$$b$$，是否都有解？例如：

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-2dde59bc420c836e4c9b83861a02d84286293016%2Fcolspace-axeqb.png?alt=media)

因为3个列向量的线性组合无法充满整个四维空间，所以会有非常多的$$b$$，它们并不是这3个列向量的线性组合。这里有4个方程，却只有3个未知数，大多数时候是无解的。简单理解就是，假设前3个方程确定了唯一解，第4个方程可能还是这个解，也可能破坏了这个解导致无解。

那么，什么样的$$b$$，可以使得这样的方程组有解呢？当且仅当(exactly when) $$b$$属于$$A$$的列空间$$C(A)$$

值得注意的是，上面这个例子里第3列=前两列的和，所以这3列并不是线性无关的。所以第3列其实是没有贡献的，可以直接删了，并不影响这个矩阵的列空间。前2列称为主列（pivot columns）。当然，也可以扔掉第1列

零空间（null space）：使得$$Ax=0$$的所有解构成的空间

对于$$m\times n$$的矩阵$$A$$，其列空间是$$C(A) \in R^m$$，而零空间是$$N(A) \in R^n$$

为何这个零空间是个空间？需要证明一个解$$x$$，以及另一个解$$x^*$$，他们的和$$x+x^*$$仍然在空间里

### lecture7 求解Ax=0：主变量，特解

### lecture8 可解性和解的结构

### lecture9 线性相关性，基，维数

### lecture10 4个基本子空间

### lecture11 矩阵空间，秩1矩阵，小世界图

## LLM+math

### mathscale

[【LLM-数学】MathScale 用于数学推理的指令调优扩展方法](https://mp.weixin.qq.com/s/tQUIGdViMZTb_9NNh3b3RQ)

[MathScale: Scaling Instruction Tuning for Mathematical Reasoning](https://arxiv.org/pdf/2403.02884.pdf)

### AlphaGeometry

[奥数能力金牌级：DeepMind几何推理模型登上Nature，代码开源，菲尔兹奖得主点赞](https://mp.weixin.qq.com/s?__biz=MzA3MzI4MjgzMw==\&mid=2650904746\&idx=1\&sn=d39a3d92078cecbd29bd0fc82560d1da\&chksm=84e45cd4b393d5c24747f163fa0338761690447904a1a654aacf2344d7a16d36dfa2ac3ccdb0\&scene=21#wechat_redirect)提出了AlphaGeometry

### AlphaProof & AlphaGeometry 2

[谷歌AI拿下IMO奥数银牌，数学推理模型AlphaProof面世，强化学习 is so back](https://mp.weixin.qq.com/s/LNzbyf0w412BIz71sROyzw)提出AlphaProof和AlphaGeometry 2

### WE-Math基准

[真相了！大模型解数学题和人类真不一样：死记硬背、知识欠缺明显，GPT-4o表现最佳](https://mp.weixin.qq.com/s/uU1lZV0Ymj31cmZryhffyQ)

[WE-MATH: Does Your Large Multimodal Model Achieve Human-like Mathematical Reasoning?](https://arxiv.org/pdf/2407.01284)

<https://github.com/We-Math/We-Math>

<https://huggingface.co/datasets/We-Math/We-Math>

### case-based or rule-based

[ICML 2024｜Transformer究竟如何推理？基于样例还是基于规则](https://mp.weixin.qq.com/s/aVRiGW3xU_LpvxZzjDpwzQ)

[Case-Based or Rule-Based: How Do Transformers Do the Math?](https://arxiv.org/pdf/2402.17709)

<https://github.com/GraphPKU/Case_or_Rule>

## AlphaProof(nature)

[Olympiad-level formal mathematical reasoning with reinforcement learning](https://www.nature.com/articles/s41586-025-09833-y)

[代码](https://github.com/daiwk/collections/blob/master/assets/alphaproof_pseudocode.py)，从<https://www.nature.com/articles/s41586-025-09833-y>这里的Supplementary Data下载

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-eca2580e5245b84b5327040306d561a5acbe98f3%2Falphaproof1.png?alt=media)

* 状态：Lean prover的逻辑状态，即Lean tactic state，表示已经建立的假设，和剩下的目标
* 环境：给定一个状态，和agent采取的动作，输出下一个状态
* 动作：一个证明的中间步骤，是一段文本，例如“a=2,b=2a,==>b=4”
* episode结束条件：证明完成or预算花完（例如超时）
* reward：每个tactic的reward都是-1，因为要鼓励用更少的步骤完成证明，即到达终点的分支路径最短

prover agent是把dnn和alphazero的搜索算法相结合：

* proof network：是一个3B的encoder-decoder transformer，输入Lean tactic state，输出2个东西：
  * policy：下一步要尝试的N个动作
  * value：当前**状态**的价值，即从此刻到episode结束时的每步reward之和
* tree search：和alphazero类似，使用AND-OR tree structure将证明拆成多个独立的子目标(类似[Hypertree proof search for neural theorem proving](https://arxiv.org/pdf/2205.11491))，采样使用的progressive sampling

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-cadb95a82883b687c76c5f542abd0b84b01f85b1%2Falphaproof2.png?alt=media)

* 预训练：proof network在大概300 billion tokens的代码和数学语料通过next token prediction预训练
* SFT：在300k的人类用matlab标注的证明语料(state-tactic pairs)上sft，
* main RL：
  * 用gemini的LLM搞了一个自动形式化（formalization）的系统，将大概1M的非形式化的问题形式化成了80M的问题
  * proof network+tree search和Lean环境交互，生成形式化的证明和反证（disproof），然后用Alphazero的方式基于得到的经验去RL训练
* inference：
  * 首先参考Alphazero，增加tree search的预算，例如产生更多的搜索路径
  * 如果增加了搜索路径还不够，那就用Test-time RL（TTRL）：
    * 给定一个问题，variant generator生成其变种（例如简化或者泛化）
    * 基于这些变种去进行RL训练