Djinnlang：通过编译器中的LLM进行无歧义规范的高级编程
Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compiler
- Harvard University（哈佛大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文提出Djinnlang，一种基于无歧义规范的高级语言，利用LLM在编译器中生成代码并由验证器检查，实现规范即编程，并展示自托管能力。
AI中文摘要：
程序员编写形式化规范，LLM实现它们，并证明每个实现与其规范匹配。将其推向极致，这使得规范语言成为新的编程语言。我们认为无歧义约束是关键：除了证明其实现满足规范外，LLM还必须证明任何其他满足该规范的实现必须在相同输入上产生相同输出，即由约束形成的关系是确定性的。这使LLM在程序语义上没有回旋余地：与传统编译器一样，生成的代码永远不需要被阅读，并且可以随时从规范重新生成。在此约束下，借助强大的LLM，规范语言与编程语言之间的差异变得基本上无关紧要，LLM实质上成为编译器工具链的一部分。这种安排兼作一种强形式的AI控制：不受信任的模型编写代码，但其工作受到验证器的严格检查。为了证明我们由无歧义约束支持的LLM-in-the-compiler范式是可行的，我们提出了Djinnlang，一种为这一未来而构建的高级规范语言。Djinnlang程序仅由规范组成——程序员从不编写可执行代码。代替传统编译器，符号转换器将每个规范降级为Dafny桩和证明义务，驱动程序编排LLM填充实现和证明，所有内容均由Dafny验证器检查。我们在多个示例上评估了我们的语言和实现，并展示了其自托管性：LLM可以从其规范实现Djinnlang转换器，并且重新实现可以验证自身。
英文摘要：
Programmers write formal specifications, and LLMs implement them, proving that each implementation matches its spec. Taken to its extreme, this makes specification languages the new programming languages. We argue that an unambiguity constraint is key: in addition to proving that its implementation satisfies the specification, the LLM must also prove that any other implementation satisfying it must produce the same outputs on the same inputs, i.e. that the relation formed by the constraints is deterministic. This leaves the LLM no leeway on program semantics: as with a conventional compiler, the generated code never needs to be read and can be regenerated from the spec at any time. Under this constraint and with a powerful LLM, the difference between a specification language and a programming language becomes essentially meaningless, and the LLM essentially becomes a part of the compiler toolchain. The arrangement doubles as a strong form of AI control: an untrusted model writes the code, yet its work is tightly checked by a verifier. To demonstrate that our LLM-in-the-compiler paradigm is feasible when supported by our unambiguity constraint, we present Djinnlang, a high-level specification language built for this future. A Djinnlang program consists only of specifications --- the programmer never writes executable code. In place of a traditional compiler, a symbolic translator lowers each spec to Dafny stubs and proof obligations, and a driver harness orchestrates an LLM that fills in implementations and proofs, all checked by the Dafny verifier. We evaluate our language and implementation on multiple examples and we show that it is self-hosting: an LLM can implement the Djinnlang translator from its specification and the reimplementation can verify itself.
