源自 Christopher Alexander 形式理论的人工智能辅助软件开发设计理论

不能假定大语言模型 (LLM) 生成的代码满足指定的要求。审查、测试和静态分析仍然适用，但其中哪些足够的Harness需要，以及它们的作用是什么，是开放的。我们提出了一种源自克里斯托弗·亚历山大形式理论的设计理论，以及应用它的方法。在亚历山大的解释中，形式与其背景之间的契合度只能被负面地感知，因为没有发现不契合的地方。我们使组织的传统变得明确，并从它和问题的分类中得出不适应的地方。该理论将大语言模型建模为非本地白话构建者，接受过许多代码库的训练，但没有本地代码库，其输出往往倾向于主流惯例而不是当地传统。我们设计了四种机制：问题的明确表示（杰克逊的问题框架）和传统的表示（四种形式的模式语言）；确定性失配检测器；固定循环；以及管理代表和探测器的人为门控立法电路。我们将由此产生的方法（一种Harness工程实践）称为“失配治理开发”(MGD)。它的双循环过程将一个自主的内循环与一个人类外循环分开，其中大语言模型根据门进行迭代，而人类的外循环则根据世界来判断规范。它们共同构成了 S = P = T = W 保证模型（规范、程序、测试、世界），其等号表示关系，而不是身份。我们报告了根据 64 个问题框架规范构建和重建由四个事件源聚合组成的 Scrum 系统的证据，并通过大约 1,300 个生成的测试和 28 个阻塞门（其中一个应用了 188 条规则）进行了验证。这解决了 Alexander 1996 年 OOPSLA 挑战的生成维度。道德维度，规范是否仍然符合世界，需要人的判断，属于外循环。