这周本来没什么动静，直到一篇 arXiv 预印本把我拽住了。8 月 13 日挂出来的，讲 LLM 写形式化规格到底行不行。
规格是什么级别的概念，不展开。写代码的人都知道，代码能跑和代码是对的，是两回事。形式化验证管的是后一件事。验证的前提，是你先把“什么算对”写成机器能检查的精确描述。那个东西就叫规格。
写规格比写代码还累。这个领域一直冷清，根子就在这。不是工具不好，是人写不动。
所以自然的念头就是让 LLM 来写。问题来了：你怎么知道它写得好不好？
这篇论文最有意思的地方不是答案，是它把这个问题本身拆了。
现有的评估办法，要么拿规格去对实现做一致性验证，要么证明两份规格语义等价。两条路都难。更麻烦的是，你分不清一个低分到底是规格烂，还是证明本身太难。考卷出成这样，考出来的分数没法解释。
他们提了个框架，叫 Coins，基于 Rocq 的。思路是：把待评估的规格在测试用例上实例化，生成具体的证明义务，再看这些义务能不能被证掉。
我特别喜欢里面一个设计考量，他们自己点明的：形式推理是不对称的。证出来了，是可靠证据。证不出来，什么也说明不了。可能是规格烂，可能是工具不行，可能是你笨。失败是歧义的。
这个不对称性到处都在。prompt 调了半天模型还是答错，你不知道是 prompt 的问题、模型的问题，还是题本身就没答案。能分清“成功说明了什么”和“失败说明不了什么”的评估方法，天然比把两种信号搅在一起的更可信。
结果部分说两句。他们在 HumanEval 上配了人工写的 Rocq 规格，做了大规模实验。结论不乐观：规格生成对 LLM 仍然是硬仗。而且验证的复杂性会盖住规格质量的真实差距。两个模型可能规格水平差一截，但你从证明通过率上看不出来。
论文最后那句，我直接抄意思：准确的规格评估，比单纯把模型做大，更能看清 LLM 在规格合成上的真实水平。
这句话我琢磨了一会儿。它其实是在说，这几年大家看模型能力涨没涨，看的是 benchmark 分数。但如果考卷本身有毛病，分数涨了也可能是假涨。他们用测试用例上的形式推理做尺子，声称这把尺子更有区分度。
我信一半。尺子更好，我认。但这套方法依赖人工写规格做底子，而人工写规格恰恰是那个最贵、最不想干的环节。用最贵的东西去评最想自动化的东西，这个循环短期内绕不出去。论文里没怎么面对这一点。也可能是我读漏了。这篇我只过了一遍，有些证明细节没啃动，先放在这里。
对普通人这段意味着什么？老实说，短期内不意味着什么。形式化规格离日常写代码还远。但有个思路值得白嫖：你在验证 AI 给你的任何输出时，先想想你的验证方法本身靠不靠谱。AI 答对了你能确认，AI 答错了你未必能发现。这个不对称性不是 Rocq 独有的，是所有“用工具检查工具”场景共有的。
验证答案的能力，比生成答案的能力，更值得普通人下功夫。这话我之前好像也说过一次，这次有论文撑腰了。
本周就这些。上面如果有谁真去读了那篇论文、发现我讲岔了，欢迎回来纠正我。
下周见。