为了确保软件在设计上是安全的，研究人员经常使用形式化验证——这是一个利用数学证明来排除整个类别漏洞的过程。该领域的一个主要障碍是“规范”问题：为了证明一个程序是正确的，必须首先定义正式语义（即对每个语句和循环行为的精确数学描述）。虽然像 WebAssembly 或 C 这样的某些语言已有建立的语义，但许多其他语言并没有。如果没有精确的规范，就没有可以用来证明程序安全性的基准真理。

Basis 的研究人员通过使用大语言模型（LLM）为一种名为 WHILE 的小型命令式语言生成这些语义来解决这一问题。然而，由于 LLM 可能会犯错，错误的语义将使随后的任何证明失效。为了解决这个问题，团队提出了一种“激进”的方法：将现有的解释器（即实际运行代码的程序）视为基准真理。他们将基于 C 语言的解释器编译成具有正式定义指令集的 RISC-V 机器代码。然后，他们要求 LLM 编写一套可读的规则（即语义）以及一个在 Lean（一种证明辅助工具）中的数学证明，以证明这些规则能够完美预测编译后二进制文件的行为。

一个展示程序输入、机器状态以及语义迭代修正之间关系的技術图表。
该研究方法使用反馈循环，将失败的证明义务返回到语义中进行修正，直到它们与编译后的二进制文件行为一致。www.basis.ai

该图表说明了使用编译后的解释器作为基准真理来调试和完善高层语义的“激进”方法。

这种方法迫使 LLM 去考虑那些在人类编写的规范中经常被忽略的细微实现细节。例如，最初证明失败是因为 LLM 生成的语义没有考虑到 C 解释器在将函数名渲染为字符串时存在的 63 字节限制。只有当语义被修正以匹配二进制文件的实际行为时，证明才得以“完成”。通过使用编译后的解释器作为锚点，研究人员创建了一个系统，其中证明过程本身充当语义的调试器。如果证明失败，则表明高层规则与底层执行之间存在差异，这将迫使模型不断完善规则，直到它们与机器代码完美对齐。

一个三车道开发图表，显示固定输入、LLM 生成的组件和经过检查的输出。
开发流水线将 RISC-V 内核等固定输入与 LLM 生成的语义以及由此产生的细化定理分开。www.basis.ai

此视觉效果解释了项目在固定硬件/软件锚点与 LLM 生成组件之间的结构划分。