Ship Your Interpreters · Kiran Gopinathan
Talk by Kiran Gopinathan (kirancodes.me): Ship Your Interpreters: Validating LLM-Written Semantics against the Binary
Can language models write semantics for real world languages that can be trusted? Large language models are rapidly reducing the manual effort required to write the proofs for formal verification. However, the cost of writing specifications remains a bottleneck. Language semantics are one such specification, and are often large, subtle and hard to review, so an LLM-generated semantics cannot simply be checked by reading it. We propose a novel technique to make LLM-generated semantics trustworthy by verifying them against the binary implementation people actually run. We compile the language's interpreter to a machine with a formal model and prove that the binary refines the semantics, that is, “ship your interpreters”.
We carry this out for a small WHILE language, whose C interpreter we compile to RISC-V. LLMs wrote the big-step semantics and a Lean 4 proof that the binary, run on the Sail RISC-V model, halts with a program's output exactly when the semantics derives it. The proof uses a port of MachCSL's machine-code separation logic to iris-lean, and along the way it exposed errors in the semantics' rules. The validated semantics becomes a foundation for verified tools whose guarantees reach the binary, such as a type system, a program logic, an abstract interpreter and a compiler.
Schedule: 3:00–3:30 PM introductions · 3:30–4:30 PM talk · 4:30–6:00 PM social
First time at NYC Lean? Please register with your real first and last name: NYU checks every visitor against a guest list. If you have registered for an NYC Lean meetup before, you should already be on the list.
More at lean.nyc/calendar