差分测试无需形式化证明也能奏效，但共模故障才是隐患
差分测试让你无需知道正确答案就能发现 bug。问题在于，相关的错误看起来像是达成一致。以下是如何发现盲点。
你可以在没有形式化证明的情况下信任差分测试，但前提是你必须清楚它究竟会在哪里失效。 这个弱点叫做共模故障（common-mode failure）。当某个规范的每一个实现都做出同样的错误假设时，它们会全部达成一致，而你的测试框架会将其判定为通过。N 版本编程（N-version…
n-version-programming
6 posts
测试无法证明两个函数等价。以下方法才能真正做到。
N-version programming 假设你的实现结果一致。我们来看为什么测试远远不够，SMT solvers 如何真正证明等价性，以及如何在‘足够好’和形式化验证之间取舍。
你搭建了一个 n-version 系统。同一个关键函数的三个独立实现，一个选择多数结果的 voter，以及一种你已经规避了单点故障的满足感。 但你并没有证明这些函数是等价的。你只证明了它们能编译通过。 N-version programming 的核心思想是：如果某个实现存在 bug，其他实现大概率不会有，因此…
如果我的 LLM 变体意见不一致，哪个才是对的？
并行运行多个 LLM 能够捕捉到任何单一模型都会自信地交付的错误。以下是如何构建一个真正有效的分歧解决系统。
你把 prompt 发给 GPT-4o。它返回一个 JSON blob，置信度 0.97。你把同样的 prompt 发给 Claude 3.5 Sonnet。它返回了另一个不同的 JSON blob，置信度也是 0.97。两个模型听起来都无比确定。但它们各自以不同的方式错了。 这不是假设。如果你运行任何非平凡的…
五种实现却没有多数派：如何真正选出最佳方案
N-version programming 听起来很简单：运行多种实现，然后挑出最佳答案。但在实践中，'最佳'远比'最常见'更难定义。
你有同一个函数的五种实现。三种返回相同结果。一种略有不同。一种抛出异常。哪个才是对的？ 大多数团队默认采用多数投票。当输出完全一致、错误显而易见时，这招确实管用。但一旦各实现在细微之处产生分歧，或者每个变体都给出不同答案时，这套机制就会崩解。N-version programming…
同一个 LLM 可以写出五个版本的函数。下面介绍如何让它们真正不同。
基于 LLM 的 N 版本编程不需要多个模型。通过变化提示词、角色设定和推理约束，你可以从单个模型中提取多样化且正确的实现。
N 版本编程默认多样性来自不同的作者。对 LLM 来说，这意味着不同的模型、不同的提供商，甚至不同的训练批次。但这个假设是错的。你可以通过改变提问的方式，而不是提问的内容，从同一个模型中获得有意义的多样性。 问题在于：把 temperature 调到 1.0…
NASA 同时运行了 27 份相同的程序。Bug 们抱团投票。
N-version programming 曾承诺独立团队会犯独立的错误。Knight 和 Leveson 在 1986 年的实验证明了相反的事实，NASA 悄然放弃了这条路线。
20 世纪 80 年代初，NASA 面临着一个至今仍在困扰安全关键工程领域的问题：如何容忍那些尚未发现的 bug？他们的答案是 N-version programming。将同一份规范交给三个独立团队。并行运行三个程序。对输出结果进行投票。如果其中一个团队写出了 bug，另外两个团队会通过多数票将其压倒。…