Basis 用 LLM 与 Lean 证明 WHILE 解释器语义与 RISC-V 二进制一致

Basis 团队让 LLM 为小型语言 WHILE 编写形式语义，并用 Lean 证明该语义与编译到 RISC-V 的解释器二进制在任意程序上输出一致。实验中证明一度达到约 100 万行 Lean，后压缩到 20 万行以内，并据此在三天内构建类型检查器、程序逻辑、抽象解释器和经过验证的编译器四个工具。团队下一步计划把方法扩展到 Lua 5.4.7 和 OCaml，长期目标是 CPython。