人类判断作为规范

# 人类判断作为规范 来源：https://blog.brownplt.org/2026/06/09/pick.html 标签：大型语言模型（https://blog.brownplt.org/tags/LLMs/），语义学（https://blog.brownplt.org/tags/semantics/），工具（https://blog.brownplt.org/tags/tools/），线性时序逻辑（https://blog.brownplt.org/tags/LTL/） *发布于2026年6月9日。* 编程领域生成式AI的兴起，显然需要形式化方法同步跟进，以确认那些不受控的AI系统确实产出了我们真正想要的解决方案。而这又要求我们先明确我们“想要”什么。这种规范必然是数学化的，才能借助形式化方法工具。但大多数程序员对形式化规范的了解远不及对编程的了解。他们能怎么做呢？ ### 获取规范的糟糕方式 我们面临的核心问题是：如何从非形式化（通常是散文式描述）过渡到形式化。一个自然的解决方案是：使用LLM将散文翻译成形式化规范。一方面，这并非荒谬之举：LLM在生成许多当代形式化符号的项方面表现相当不错。这里引用Ron Minsky（https://signalsandthreads.com/future-of-programming/#5515-1）的半开玩笑说法： > 我在想，一个更合理的模式是不是这样：你去找大语言模型，说‘请帮我写一个排序列表函数的规范。’然后它就会吐出点什么。接着你看看它，心想，嗯，看起来差不多。 Richard Eisenberg对此的回应触及了问题的核心：我们如何确信生成的规范是“正确”的那个？人类可能一开始就错了。他们可能明显错了，也可能错得微妙。他们可能表述模糊，而LLM可能采纳了错误的理解。还可能存在对该语言的常见（https://blog.brownplt.org/2022/11/05/little-tricky-logics.html）误解（https://blog.brownplt.org/2024/07/07/little-tricky-logics-2.html）（这些误解可能也嵌入了语言模型中）。或者他们可能指的是没有明确事实依据的东西，唯一的事实只存在于他们脑中：他们的意思取决于他们自身的“上下文”。这些问题都无法单靠LLM解决。 ### 人在回路中 因此，我们认为在形式化规范的过程中让人参与进来至关重要。一个真正的“氛围编程者”（vibe-coder）按照定义是不会在乎这些的。相反，我们要瞄准的是“负责任的”程序员：他们在乎工作质量，但同时又是人，即忙碌、懒惰等等。我们能做些什么来帮助他们呢？ 我们认为任何解决方案都应具备两个关键特征： 1. **必须有意义**。要求人类对复杂抽象的陈述做出判断很难有效。懒惰、自动化偏见、无法形成良好判断以及急于完成任务的心态，都会导致无意义的确认。 2. **必须适度**。询问过多的问题，无论多简单，都会令人疲惫，并且随着问题数量增加，错误也会增多。我们应该尽量让每个人的每次操作都产生重大影响，且不要要求用户执行太多操作。 请注意，很容易只满足其中一点而忽略另一点。告诉人们“你必须阅读LLM生成的所有代码”肯定有意义——但这完全不适度（所以大多数人不会这么做）。经典的安全警报只问一个是/否问题，这算是适度努力，但没有意义（因为不这样做的后果是完不成任务）。挑战在于，沿着这两个维度推进到刚好能获得真正价值、但又不会把人吓退的程度。 ### 我们的解决方案 几个月前，我们发布了关于PICK（https://blog.brownplt.org/2025/12/11/pick-regex.html）的文章，这是我们构建的一个工具，旨在帮助我们更好地利用LLM生成正则表达式。你给LLM一个提示，得到的不是一条正则表达式，而是几个看似合理的候选。通常的选择是直接接受模型给出的结果，或者自己阅读这些正则表达式并试图找出正确的那一个。PICK做了别的事：它会向你展示一些精心挑选的“具体字符串”，目的是“区分”各个候选，然后请你给每个字符串点赞或点踩。最终存活下来的正则表达式就是获胜者。值得一读那篇文章，了解其工作流程。 那篇文章没有提到两个重要的事情。 第一，我们现在有了实验结果表明这个工作流程非常有效。 第二，这并不仅限于正则表达式。我们目前已经为三个有代表性的领域构建了PICK，并且有意选择了彼此不同的领域：“正则表达式”、“线性时序逻辑（LTL）”和“基于属性的访问控制（ABAC）”。在这三个领域中，算法都是相同的：生成候选，从集合差中采样，呈现一对场景，更新分数，收敛或承认失败。工作流程无需针对每个领域重新设计。（读过我们之前关于差异分析（https://blog.brownplt.org/2024/06/27/differential-analysis.html）那篇文章的读者会看出其中的家族相似性。PICK是带有人机交互的版本，其中仍然可行的候选之间的语义差异会驱动下一个问题。） 同一算法能在三个领域奏效的原因，在于它们共享两个关键性质： 1. **对否定和交集封闭**——这样两个候选之间的差异本身就可以被表达出来。 2. **从该差异中采样**——这样系统可以向用户展示候选产生分歧的具体案例。 这里用到的机制并不新奇。这是大二计算理论课程的内容：封闭性质、集合差异以及见证生成。程序员日常使用的许多形式化系统已经具备这些性质——要么是固有的（布尔逻辑、网络路由规则、包版本约束），要么是通过标准技巧限定论域（几乎任何可以用SAT/SMT求解器处理的东西）。那些在课堂上被告诉很重要、但从未真正看到应用的性质，在2026年，它们是区分你得到一个自信但错误的访问控制策略的关键。而且，其动机竟然来自认知科学原理。所以至少，也许我们可以改进计算理论的教学方式！ ### 综合也如何微妙地失效 所以是的，PICK是一个“验证”工作流程：你有一些意图，模型提出候选，PICK帮助你检查这些候选是否符合你的本意。但这种框架描述低估了它的意义。PICK实际还做了另一件事：它恢复了综合往往抹去的东西——用户意图的独立见证。 要理解这个见证为何重要，有必要回想一下验证的初衷。 验证著名的写法是*P*⊧ ɸ：一个程序*P*实现了属性ɸ。这种检查之所以有信息量，正是因为*P*和ɸ是“独立”编写的。如果两者编码了相同的误解，那么一致性并不能排除任何问题；冗余性就消失了。（而这正是让LLM生成验证硬币的两面所带来的危险。PICK介入正是为了确保LLM不是ɸ的“唯一”来源。） 现在考虑综合：ɸ ⟹ *P*。程序是正确构建的。然而，这意味着它也是“不”正确构建的。当ɸ错误时，生成的*P*会以完全相同的方式出错，而用*P*对ɸ的交叉检查无法发现这一点。这在经典演绎综合和示例编程中已经成立。在LLM综合中，这更加成立。LLM只看到用户的自然语言，而自然语言只是用户真实需求的失真提示。 简单地堆砌更多LLM未必能解决这个问题。它们共享训练数据，共享先验知识，并且常常共享误解。更多模型能让你更快地获得更多“一致性”。但它们未必能给你更多“冗余性”，而这正是验证一贯追求的目标。两者都无法知道用户的真实意图：这正是PICK要处理的问题。 ### 人类判断作为规范 在PICK中，这个独立见证不是另写的规范——它存在于用户的分类中：每一次接受或拒绝都是对具体行为的一种承诺，存活下来的候选必须与所有这些承诺一致。整体来看，这些承诺揭示了原始提示中未明确说明的内容。假设提示是“一个匹配日期的正则表达式”，模型返回了几个候选。PICK把字符串摆在你面前：对`1/15/2025`点“是”，对`13/01/2025`点“否”，这就表明了你对“日-月-年”与“月-日-年”的立场——这是提示中隐含的问题，用户可能从未正式回答过，甚至对自己都没有明确过。用户带着模糊的意图而来；PICK帮助使其清晰——不妨称之为规范“阐明”——不是通过盘问他们关于公式的问题，而是迫使他们就提示中隐含的问题做出承诺。 这也是为什么PICK可以“有用”地失败。有时模型的所有候选都不对，PICK最终没有幸存者。按照规范阐明的解读，这个结果意味着：你通过分类所做的承诺，模型产出的任何东西都无法满足。与其将正则表达式发出去，不如知道这一点。 这也是为什么我们不相信随着模型改进，PICK会变得不那么有用。更好的模型并不能让用户意图更明确——当被要求“匹配北美国家的正则表达式”时，更强大的模型仍然无法告诉你，你是否想把加勒比地区包括进来，或者你想往南划到哪里为止。更好的模型能更快地生成更好的候选——这正好将用户的工作量“转向”了PICK设计所支持的方向。 要了解更多，请阅读我们的ECOOP 2026论文（https://www.siddharthaprasad.com/papers/pafk-pick.pdf），或者尝试在VS Code中使用PICK:Regex工具（https://marketplace.visualstudio.com/items?itemName=SiddharthaPrasad.pick-regex）。 如果你有一种具有上述封闭性质的形式化语言——我们怀疑你会惊讶于有多少语言具备——我们非常希望能收到你的来信。