LLM 无法证明你的代码正确，但它们可以撰写实现证明的样板代码
净室验证需要生成并消解证明义务。以下介绍 LLM 如何自动化注解和验证条件生成，让你可以专注于真正困难的证明。
净室软件工程要求你在编译之前就证明代码的正确性。这听起来很高尚，直到你花三个小时为一个对十个整数进行排序的函数编写循环不变式。 瓶颈不在于证明本身，而在于样板代码。生成验证条件、用不变式注解循环、以及为 Dafny、Why3 或 Z3 格式化断言，这些工作枯燥乏味、容易出错，而且毫无乐趣。LLM…
llm
9 posts
先向LLM解释代码，让我的缺陷率降低了85%
我花了30天时间，在向LLM索要代码之前先撰写设计说明。结果改变了我对rubber-ducking的看法。
大多数开发者把LLM用反了。我们用五个词描述需求，拿回200行代码，然后花下一个小时调试模型做出的假设。 我花了三个月时间运行相反的流程：在索要哪怕一行代码之前，先写一份完整的设计说明。结果代码缺陷更少了，但真正的进步在于我自己的理解。 Donald Knuth在1984年提出了"literate…
你的 Claude 对话已经是文档了。只是它会在 12 小时后消失。
LLM 对话包含意图、被拒绝的替代方案以及可运行的代码。这正是文档应该包含的内容。以下是将 ephemeral chat 转换为持久、可搜索的文档，同时不丢失叙事的方法。
你花了 45 分钟和 Claude 设计一个 retry circuit。你解释了 failure modes，因为 exponential backoff 会掩盖 cascading pressure 而拒绝了它，确定了 token-bucket rate limiting with…
大语言模型可以预先审查你的代码，但它无法主持会议
费根审查需要四到六个人、两小时才能审完250行代码。大语言模型可以通过承担准备工作和检查清单的执行来削减这部分成本，但它无法取代人类角色去发现最昂贵的缺陷。
一次完整的费根审查需要一名主持人、一名朗读员、两到四名审查员，以及作者本人。团队以每小时125行的速度，花费两小时审查大约250行代码。这意味着一次小小的改动就要消耗八到十二人时。 大语言模型可以在不到一秒内读完250行代码。它可以执行检查清单、标记可疑模式，并在任何人打开文件之前就生成一份结构化的缺陷记录。…
LLM可以生成Rust代码，但形式化证明完全是另一回事。
大语言模型能写出质量惊人的Rust代码，但当你要求形式化证明时，它们会幻觉出不变量，并编造出没有任何验证器接受的语法。本文介绍它们真正做对了什么、在哪里崩溃，以及如何善用它们。
LLM能写出可以编译甚至通过的Rust代码。但它们目前还无法可靠地写出形式化证明，来证实代码对所有可能的输入都是正确的。…
语法约束解码: 让每个 token 都强制 LLM 输出有效语法
LLM 会对语法产生幻觉，因为它们以概率方式采样 token。语法约束解码在每一步过滤词表，只输出保持语法有效性的 token。
让 LLM 生成一个 JSON 对象，它最终一定会输出一个末尾逗号、字符串里未转义的换行符，或者在一个本该有引号键的位置输出 bare word。这个错误不是模型的 bug。它是自回归采样工作方式的必然结果：在每一步，模型都会把自己的词表里每个 token 都当作候选，包括那些会让部分输出在语法上 invalid 的…
从英语翻译到主题很容易。使其具备确定性才是真正的问题。
你可以从简单的英语描述中生成设计令牌，但前提是将该描述视为带有模式契约和快照测试的限界上下文DSL。
是的，你可以用英语描述一个主题，并得到一个可用的设计系统。关键在于，这段英语描述不是提示词。它是源文件。和任何源文件一样，它需要编译器、类型系统和测试。…
如果我的 LLM 变体意见不一致，哪个才是对的？
并行运行多个 LLM 能够捕捉到任何单一模型都会自信地交付的错误。以下是如何构建一个真正有效的分歧解决系统。
你把 prompt 发给 GPT-4o。它返回一个 JSON blob，置信度 0.97。你把同样的 prompt 发给 Claude 3.5 Sonnet。它返回了另一个不同的 JSON blob，置信度也是 0.97。两个模型听起来都无比确定。但它们各自以不同的方式错了。 这不是假设。如果你运行任何非平凡的…
同一个 LLM 可以写出五个版本的函数。下面介绍如何让它们真正不同。
基于 LLM 的 N 版本编程不需要多个模型。通过变化提示词、角色设定和推理约束，你可以从单个模型中提取多样化且正确的实现。
N 版本编程默认多样性来自不同的作者。对 LLM 来说，这意味着不同的模型、不同的提供商，甚至不同的训练批次。但这个假设是错的。你可以通过改变提问的方式，而不是提问的内容，从同一个模型中获得有意义的多样性。 问题在于：把 temperature 调到 1.0…