Basis 用 LLM 写编程语言语义，Lean 证明解释器编译到 RISC-V 无误

patrickmineault · x · 2026-10-17

Basis 团队发布研究文章《Ship Your Interpreter》：让 LLM 为一门小编程语言写出精确的数学规则（形式语义），再用 Lean 证明其解释器——即使被编译成 RISC-V 芯片的底层指令——严格遵循这些规则。

核心观点与脉络：

程序验证需要程序、规约（specification）和语义（semantics）三要素，但 Python、Ruby、Lua 等主流语言都没有形式语义，因为手写语义太痛苦。
直接让 LLM 写语义会有错，但语言本身有解释器/编译器可作为「真值来源」用来校验。
团队判断：随着 LLM 能力增强，验证的瓶颈正从定理证明转向规约与语义——如何确保你证明的命题确实捕捉了你关心的行为。他们提出的方法有望扩展到所有编程语言。
背景进展：4 月其 agent 构建了 JS→WebAssembly 编译器但无法证明行为保持；之后验证了 Linux nftables 编译器；9 月 MIT 的 Kaashoek 与 Zeldovich 用 AI agent 把 xv6 内核验证到机器码级。
目标是让关键基础设施软件「by design」安全，跟上 AI 辅助攻击的增长速度。

「编程与Agent」频道最新