可执行JavaScript作为一种可检查的规范语言：关于SysMoBench的JS-SAM案例研究
Executable JavaScript as a Checkable Specification Language: A JS-SAM Case Study on SysMoBench
浏览论文内容
中文总结 AI 辅助
研究大语言模型用不同语言为真实系统写规范的情况，以SysMoBench为平台，通过添加JS-SAM进行控制比较，涵盖多个模型和系统，发现一致性是区分模型关键，规范契约决定保真度，最小契约有转录无语义推导，将可执行JavaScript作为规范基础作案例研究。
中文摘要 AI 辅助
我们研究大语言模型能否为真实系统编写可靠的形式规范，以及用它们少见的形式语言或训练数据中丰富的主流语言编写是否有影响。在SysMoBench上进行研究，其分四个阶段对生成的规范评分，关键阶段重放从运行系统捕获的执行跟踪。我们添加了首个非形式后端JS-SAM，规范是用SAM模式编写的可执行JavaScript，其语义反映TLA+。进行了控制比较，分离了普通直接比较中纠缠的三个变量：语言、规范契约和提示。研究涵盖四个前沿模型和三个系统，有反例驱动修复。得出三个发现：与真实系统的一致性是区分模型的唯一阶段；规范契约而非语言决定保真度；最小契约有转录但无语义推导。我们将可执行JavaScript构建为可检查的规范基础，补充而非取代TLA+提供的验证，并将此研究作为案例研究呈现。
英文摘要
Can large language models write faithful formal specifications of real systems, and does it matter whether they write in a formal language they have seen rarely or in a mainstream language abundant in their training data? We study this on SysMoBench, which grades a generated specification in four phases, the decisive one replaying execution traces captured from the running system. We add JS-SAM, its first non-formal backend, in which a specification is executable JavaScript written in the SAM pattern, a pattern whose semantics mirror TLA+, and run a controlled comparison that separates three variables an ordinary head-to-head entangles: the language, the specification contract (the shape the model must fill), and the prompt. The study spans four frontier models and three systems (an operating-system spinlock, a distributed lock service, and the Etcd Raft consensus implementation), with counterexample-driven repair. Three findings emerge. First, conformance against the real system is the only phase that discriminates among models; internal consistency is inexpensive to satisfy, and a specification that looks right is not thereby right. Second, once the comparison is drawn like for like, the specification contract, not the language, governs fidelity: JavaScript in the shape of the TLA+ transition relation is as faithful as TLA+. Third, a minimal contract carries transcription but not semantic derivation: at consensus scale the difficulty becomes understanding the protocol, which no contract shape and no language supplies. We frame executable JavaScript as a checkable specification substrate that complements, rather than replaces, the verification TLA+ provides, and present the study as a case study.
