Verified LLM-Driven Synthesis for Concept Design
本文提出了一个基于概念的软件设计形式化框架，以及一种利用自然语言和基于场景的引导来生成经验证的反应设计的 LLM 驱动合成程序，证明了虽然仅基于不变性的合成速度快但具有不一致性，但基于场景引导的方法尽管面临过拟合和非确定性的挑战，仍能更可靠地恢复预期设计。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正在用乐高积木建造一座巨大的、充满魔力的城市。每一块积木都是一个“概念”——一个具有独立功能的组件，比如一扇可以锁上的门、一盏可以点亮的灯，或者一个可以投递信件的信箱。最有趣的部分不在于拥有这些积木，而在于弄清楚它们如何相互通信。如果你敲了敲门，灯会亮吗？如果信箱满了，门还会保持锁闭状态吗？这些交互规则被称为“反应”（reactions）。在现实世界的软件领域中，把这些反应处理正确是一场噩梦。如果规则稍有偏差，你的数字城市可能会意外地让小偷进来、删除所有的信件，或者陷入永久冻结。这就是“协调逻辑”（coordination logic）的问题：确保系统的所有独立部分能够安全地协同工作，而不会互相干扰。
长期以来，软件工程师一直试图用纯英文或代码来编写这些规则，但人类语言是混乱的。像“不要让小偷进来”这样的句子对我们来说很清晰，但计算机可能会以一千种奇怪的方式来解读它。这就是“概念设计”（Concept Design）这一新方法派上用场的地方。它将这些软件积木视为正式的、数学化的对象。但即便有了正式的积木，仍有一个难点：排列这些规则的方法往往有数百万种，其中只有一种方式能真正实现构建者所“预期的”目标，而其他方式可能只会让城市起火。核心问题在于：我们如何让计算机发明出那些不仅能保证城市安全，而且能符合构建者特定且往往未言明的愿景的规则？
本文介绍了一个聪明的新型协作方案：将一个超级智能的 AI（具体来说是大语言模型，即 LLM）与一个严谨的数学“裁判”结合起来，以解决这个谜题。作者开发了一个名为 foundry 的工具，它既是创意总监，又是安全检查员。该工具并非只是简单地要求 AI “使其安全”，而是使用了一种“猜与检”（guess and check）的游戏。AI 提出一套反应规则，而裁判会立即根据一系列安全目标对这些规则进行检查。如果 AI 的规则失败了，裁判不会仅仅说“错误”，而是会向 AI 提供一个关于城市是如何出错的具体示例（即“反例”）。AI 随后利用这个线索来修正其规则并再次尝试。这个循环会持续进行，直到 AI 找到一个通过安全测试的设计方案。
然而，研究人员发现了一个令人惊讶的转折：仅仅通过安全测试是不够的。因为“安全”的方式有很多种，AI 经常会产生一些技术上正确但完全奇怪的设计。例如，如果规则是“不要让敏感数据丢失”，AI 可能会决定最安全的方法是立即删除数据，或者关掉灯光以免任何人看到。这些设计是“经过验证的”（它们没有违反规则），但也是“不合理的”（没有人真的想要它们）。为了解决这个问题，论文指出，你不仅需要给 AI 安全规则，还需要给它“场景”（scenarios）。把这些场景想象成微型的分镜脚本：“这里是一个门应该打开的情况”，或者“这里是一个门必须保持锁闭的情况”。
论文在三个不同的软件应用上测试了这个想法，并为它们创建了十二个不同行为版本的实现。他们发现，当他们只给 AI 提供安全规则时，AI 通常能很快找到解决方案，但那个方案往往是错误的，或者每次运行测试时都会发生变化。但是，当他们加入了这些分镜脚本（场景）后，AI 在猜测“预期设计”方面表现得更好。事实上，使用这些分镜脚本比仅仅输入一段长而复杂的英文“提示词”（prompt）来告诉 AI 该做什么要可靠得多。分镜脚本就像是一张精确的地图，而英文提示词则像是模糊的方向，AI 经常会误解它。
研究人员还尝试了一个新技巧：与其让用户从头开始编写分镜脚本，不如让 AI 来建议这些脚本。用户只需说“是的，这是一个好故事”或“不，这是一个坏故事”。这种“场景诱导”（scenario elicitation）效果很好，但它也有一个怪癖：由于 AI 有点不可预测，有时它会重复建议相同的故事，或者遗漏关键的故事。如果用户获得的场景不够多，AI 有时会发生“过拟合”（overfitting），这意味着它会死记硬背给定的特定故事，却无法理解通用的规则，从而导致设计虽然通过了测试用例，但在现实世界中却会失效。
最后，论文表明，虽然 AI 擅长生成创意，但它需要一个严谨的数学裁判来保持诚实，并且需要具体、具体的示例（场景）来理解人类真正的意图。工具 foundry 证明了这种组合可以自动设计出安全且工作的软件协调规则，但它也警告说，我们仍需谨慎对待提供给 AI 的示例，否则它可能会建造出一座安全但完全没用的城市。结果显示，这种方法适用于中小规模的系统；但随着系统规模的扩大，用于检查规则的“裁判”耗时会增加，这表明对于巨大的城市，我们可能需要先在较小的社区内检查规则。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。