LLMs 不擅长编写“氛围式”规范

<h3>下周没有通讯</h3> <p>我将在 <a href="https://qconlondon.com/" target="_blank">InfoQ London</a> 发表演讲。不过请看下面的赠书活动!</p> <hr /> <h1>LLMs 不擅长编写“氛围式”规范</h1> <p>大约一年前，我写了 <a href="https://buttondown.com/hillelwayne/archive/ai-is-a-gamechanger-for-tla-users/" target="_blank">AI is a gamechanger for TLA+ users</a>，指出人工智能是“规范的倍增器”。那是从一位使用这些工具的 TLA+ 专家的角度写的。现在 <a href="https://github.com/search?q=path%3A*.tla+NOT+is%3Afork+claude&amp;type=code" target="_blank">GitHub 上 4% 的 TLA+ 规范</a> 中出现了“Claude”这个词。这对我来说很有趣，因为它表明人们一直对形式化方法感兴趣，只是缺乏实践技能。</p> <p>这也很有趣，因为它让我了解到初学者使用 AI 编写形式化规范时会发生什么。情况并不乐观。</p> <p>作为案例研究，我们将使用 <a href="https://github.com/myProjectsRavi/sentinel-protocol/tree/main/docs/formal/specs" target="_blank">这个项目</a>，它很友好地提供了由 AI 生成的 TLA+ 和 Alloy 规范。</p> <h3>查看项目</h3> <p>从 <a href="https://github.com/myProjectsRavi/sentinel-protocol/blob/main/docs/formal/specs/threat-intel-mesh.als" target="_blank">Alloy 规范</a> 开始。以下是完整内容：</p> <div class="codehilite"><pre><span></span><code>module ThreatIntelMesh sig Node {} one sig LocalNode extends Node {} sig Snapshot { owner: one Node, signed: one Bool, signatures: set Signature } sig Signature {} sig Policy { allowUnsignedImport: one Bool } pred canImport[p: Policy, s: Snapshot] { (p.allowUnsignedImport = True) or (s.signed = True) } assert UnsignedImportMustBeDenied { all p: Policy, s: Snapshot | p.allowUnsignedImport = False and s.signed = False implies not canImport[p, s] } assert SignedImportMayBeAccepted { all p: Policy, s: Snapshot | s.signed = True implies canImport[p, s] } check UnsignedImportMustBeDenied for 5 check SignedImportMayBeAccepted for 5 </code></pre></div> <p class="empty-line" style="height:16px; margin:0px !important;"></p> <p>这里有一点需要注意：首先，这段代码实际上无法编译。它使用了布尔（Boolean）标准模块，因此需要 <code>open util/boolean</code> 才能运行。其次，在这里使用 Boolean 是错误的做法；你应该使用子类型。</p> <div class="codehilite"><pre><span></span><code>sig Snapshot { <span class="w"> </span> owner: one Node, <span class="gd">- signed: one Bool,</span> <span class="w"> </span> signatures: set Signature } <span class="gi">+ sig SignedSnapshot in Snapshot {}</span> pred canImport[p: Policy, s: Snapshot] { <span class="gd">- s.signed = True</span> <span class="gi">+ s in SignedSnapshot</span> } </code></pre></div> <p>所以我们知道这个人实际上并没有运行这些规范。在 TLA+ 中，这个问题 <em>稍微</em> 好一些，因为 TLA+ 有一个官方的 MCP 服务器，可以让 Agent 运行模型检查。即便如此，我还是经常看到一些我认为肯定无法通过模型检查的规范，比如使用了 <code>Reals</code> 或者假设 <code>NULL</code> 是内置常量而不是用户自定义常量。</p> <p>规范更大的问题是 <code>UnsignedImportMustBeDenied</code> 和 <code>SignedImportMayBeAccepted</code> <em>实际上没有做任何有用的事情</em>。<code>canImport</code> 被定义为 <code>P || Q</code>。<code>UnsignedImportMustBeDenied</code> 检查的是 <code>!P && !Q => !canImport</code>。<code>SignedImportMayBeAccepted</code> 检查的是 <code>P => canImport</code>。这些在逻辑上永远是成立的！如果它们有任何作用，那也只是检查 <code>canImport</code> 的定义是否正确。</p> <p>在 <a href="https://github.com/myProjectsRavi/sentinel-protocol/blob/main/docs/formal/specs/serialization-firewall.tla" target="_blank">TLA+ 规范</a> 中也能看到同样的问题：</p> <div class="codehilite"><pre><span></span><code>GadgetPayload == /\ gadgetDetected&#39; = TRUE /\ depth&#39; \in 0..(MaxDepth + 5) /\ UNCHANGED allowlistedFormat /\ decision&#39; = &quot;block&quot; NoExploitAllowed == gadgetDetected =&gt; decision = &quot;block&quot; </code></pre></div> <p class="empty-line" style="height:16px; margin:0px !important;"></p> <p>AI 只编写了“显而易见的属性”，这些属性会因为“遗漏了守卫子句”或“忘记更新变量”等原因而失败。它似乎不擅长编写会由于并发、非确定性或相隔多个步骤的不良行为而失败的“微妙”属性。显而易见的属性对于定位自身和确保系统按预期运行很有用，但使用形式化方法的真正价值在于那些微妙的属性。</p> <p>（这与 <a href="https://buttondown.com/hillelwayne/archive/some-tests-are-stronger-than-others/" target="_blank">强属性与弱属性</a> 相关。LLM 生成的属性是弱的，而预期的属性需要是强的。）</p> <p>这是我在几乎所有由 AI 编写的形式化规范中看到的问题。LLM 没有做到规范的核心功能之一。像 <a href="https://martin.kleppmann.com/2025/12/08/ai-formal-verification.html" target="_blank">预测：AI 将使形式化验证成为主流</a> 和 <a href="https://leodemoura.github.io/blog/2026/02/28/when-ai-writes-the-worlds-software.html" target="_blank">当 AI 编写世界上的软件时，谁来验证它？</a> 这样的文章认为，LLM 将使形式化方法成为主流，但如果规范实际上不能验证任何东西，那么能够轻松编写规范对正确性并无帮助。</p> <h3>这是用户的错误吗？</h3> <div class="subscribe-form"></div> <p>我第一次对 LLM 和 TLA+ 产生兴趣是通过 <a href="https://zfhuang99.github.io/github%20copilot/formal%20verification/tla+/2025/05/24/ai-revolution-in-distributed-systems.html" target="_blank">分布式系统中即将到来的 AI 革命</a> 这篇文章。该文的作者后来 <a href="https://github.com/zfhuang99/lamport-agent/blob/main/spec/CRAQ/CRAQ.tla" target="_blank">通过提示生成了一份规范</a>，其中包含了一个相当复杂的属性：</p> <div class="codehilite"><pre><span></span><code>NoStaleStrictRead == \A i \in 1..Len(eventLog) : LET ev == eventLog[i] IN ev.type = &quot;read&quot; =&gt; LET c == ev.chunk IN LET v == ev.version IN /\ \A j \in 1..i : LET evC == eventLog[j] IN evC.type = &quot;commit&quot; /\ evC.chunk = c =&gt; evC.version &lt;= v </code></pre></div> <p>这比我之前看到的 <code>(P => Q && P) => Q</code> 这样的属性要复杂得多！这可能是由于 <a href="https://github.com/deepseek-ai/3FS/tree/main/specs/DataStorage" target="_blank">相应系统已经有一个用 P 语言编写的完整规范</a>。但也可能是因为 Cheng Huang 已经是一位专家级的规范编写者，这意味着他比普通开发者能更好地利用 LLM。我还注意到，我通常能比我的大多数客户从 LLM 中诱导出更有趣的东西。这对我目前的生计有利，但对于 LLM 使形式化方法成为主流的希望却是不利的。如果你需要了解形式化方法才能让 LLM 执行形式化方法，那它真的有帮助吗？</p> <p>（是的，如果它降低了技能门槛——意味着你可以用 20 小时的练习而不是 80 小时来应用形式化方法。但关于它 <em>到底</em> 降低了多少门槛，尚无定论。如果它只从 80 降到了 75 呢？）</p> <p>另一方面，似乎也有一些属性是 AI 难以处理的，即使有明确的指示。上周，我和一位客户试图让 Claude 生成一个良好的 <a href="https://www.hillelwayne.com/post/safety-and-liveness/" target="_blank">活性</a> 或 <a href="https://www.hi