论文里有两个数字我盯着看了很久。BigCodeBench Hard 上，相对 CodeRL，解决任务数从 16 提到 23——漂亮，43.8%。然后眼神往下扫到同一张表的下半部分，BigCodeBench Full：359 到 363。你没看错，四个任务，1.1%。
测试范围先划一下：这篇不是把 GraphAlignCoder 拉到自己机器上跑一遍实测——我没有那组训练资源，这也不是论文该有的用途——而是把论文里每个“提升百分之多少”放回它自己的口径里，重新称一遍。称完发现，最大的信号在宣传口径之外。
GraphAlignCoder 做的事，一句话可以说完：把代码生成训练从“给模型看更多对的和错的样例”改成“给模型看‘为什么这段代码是对的’的结构”。具体是两条线并行。一条线构建实现图，把程序拆成区域，区域之间的控制流和数据依赖画成一张图，这是程序的执行形状。另一条线用受限的 Lean 自动证明流水线生成证明轨迹，从轨迹里剥出形式化证明流图，这是程序的正确性形状。模型先学可执行代码加图描述，再把这两样整合进生成过程。
这里面真正有意思的是两条线怎么被“Align”到一起的。
实现图和证明图不是一个物种。前者描述的是时间性的东西——谁先跑、谁依赖谁的值、哪个分支被哪条路径跳过。后者描述的是逻辑性的东西——哪个结论从哪个前提来、哪条推理边建立在哪条推理边之上。要让模型明白这两种形状是同一个程序的两个侧面，训练数据里就必须让两个图反复成对出现，而且模型还得在生成代码的时候学会从图的一侧往代码的一侧走。这个从“为什么”到“怎么做”的映射，才是 GraphAlignCoder 训练的实质。31.6% 那个数字只是这个机制的影子，机制本身在阴影里。
（写到这跑个题又拉回来：vibe coding 社区最近半年常见有人提“形式化验证早晚要进入日常开发”，说的人多，知道 Lean 的证明可得性限制的人少。GraphAlignCoder 是把一条证明流水线直接焊在了训练集的生产线上，某种意义上这是形式化验证第一次离“日常代码生成”这么近——虽然是以训练数据的身份出现的。这条线值得单独写一篇，这篇不展开了。）
说说 31.6% 的口径。论文摘要里写的“持续优于基础模型、仅代码 SFT 和 CodeRL”，这句话单独看没有任何问题，但三个对照的分量完全不同。基础模型是地板，赢它只能说这不是负优化。仅代码 SFT 是有信息量的对照——它说明验证注入的收益不是靠“多训了一轮”这个简单事实就能解释的。而 CodeRL 是重头戏：RL 训练管线的代表。拿它做基线，等于在说“我的提升不是靠更强的抽样策略，也不是靠更复杂的奖励函数，而是靠补上了模型本来就没有的一种信息”。这是全文最该被读出来的那句话。
至于为什么 Hard 上收益大而 Full 上基本消失，我的判断是任务结构决定的。Hard 任务难的地方不在语法，在步骤间的依赖关系——第 3 行的状态会不会被第 9 行的分支带跑，第 12 行该不该用第 7 行的值，这种链条上的正确性，代码监督信号给得非常稀疏，模型只能靠蒙。证明流图恰好把这种依赖链画成了显式的边，于是组合类任务上它的增益大。而 Full 上的常规任务，逻辑链条短，正确性结构就那么几种固定形状，一张证明图给模型的增量信息趋近于零。收益梯度从 23 掉到 4，和任务的“结构需求量”梯度是对得上的。
论文的消融实验也往这个方向上指。验证图的注入给的是初始推理收益，真正决定跨基准稳健迁移的是“验证到代码的整合”那一步。我的读法是这样：注入像是一次性输血，见效快但持续性有限；整合像是让模型自己长出了造血能力，图知识进了生成分布，才能在新 benchmark 上不白给。这两个阶段的分工，比总分更能解释 43.8% 和 1.1% 这两级台阶。
然后是要挑刺的地方：“受限的 Lean 流水线”。受限这个词写得很诚实，但论文没有展开它到底限制了什么。我的理解是，受限意味着这套流水线只能覆盖 Lean 类型系统表达得到的那类程序性质。热门 benchmark 没问题，大家都在上面打磨过。但你把它搬到内部工具链、冷门领域的 DSL、到处是外部副作用的业务代码上去，证明流水线生成不出轨迹，整条训练链路就在这里断掉。这个框架的数值得乘以一个覆盖率系数，覆盖率是 1 的时候它很好看，覆盖率是 0.2 的时候你得到的只是一堆没法用的 Lean 中间产物。论文没有给出任何关于覆盖率的测量——也许下一版该有。
最后是我始终没过去的一个坎。359 到 363。这个数字没有任何宣传价值，但它比 31.6% 更诚实——它清楚地告诉了你这套方法的边界：凡是结构信息已经内化在任务里的地方，它几乎什么都没做。那些声称“效果显著”的论文大多不会给你看这种数字，这篇给了，我觉得这是个好信号，但这不改变 1.1% 这个事实本身，它摆在那里：等你复测。
我为这个没人提的数字写了整篇拆解，这可能本身就是个信号——真正的信息往往藏在没人引用的表格行里。谁拿到这套训练设置的，先在 Hard 上复现一把，再顺手把 Full 那四个任务翻出来看看是哪些，数字对不上，告诉我。
置信标签：方向大致对。跨基准的收益梯度和消融实验互相印证，“显式证明结构能帮代码模型在组合类任务上走得更远”这个方向在其实验范围内站得住。但 1.1% 那个数字样本太薄、方差未知，先当参考，不当结论。