This screencast demonstrates the potential of Large Language Models (LLMs) in formal methods, specifically for working with TLA+. The presenter showcases an off-the-shelf LLM (identified as "Code Llama at 37") attempting to convert a semi-formal text specification of the "Die Hard with a Vengeance" bomb-defusing scenario into a TLA+ model. The LLM iteratively uses TLA+ tools integrated into VS Code (a "pass tool," "list symbol tool," and a "model check and simulate tool") to parse, refine the specification, fix errors in the configuration, and run the TLC model checker. The process culminates in the LLM identifying a counter-example and providing an explanation. While acknowledging the demo's specific nature and the need for multiple attempts, the presenter highlights the productivity gains experienced in real-world applications.
The video then announces the "GenAI Accelerated TLA+ Challenge" (also dubbed the "TL-AI Challenge"), a competition organized by the TLA+ Foundation in collaboration with Nvidia. The challenge encourages the TLA+ community to develop novel ideas combining Generative AI and LLMs with TLA+. A key emphasis is on ensuring that AI-generated outputs are "grounded in reality" and verifiable, for instance, by using TLC to validate models or find counter-examples. Prizes include a GeForce RTX 4090 GPU and GitHub Copilot subscriptions. The challenge aims to foster practical and reliable AI-assisted tools for formal methods.
Leveraging LLMs for TLA+ and Announcing the TL-AI Challenge
00:00:02 AI for TLA+ Demonstration: The presenter introduces a screencast recorded over several days, showcasing an experiment with AI and TLA+, noting that AI is not perfect but has utility.
00:00:14 "Die Hard" Specification Task: The AI is tasked with converting a text-based, semi-formal specification of the "Die Hard with a Vengeance" bomb diffusion problem into a TLA+ model, checking it with the TLC model checker, and providing the solution.
00:00:50 Iterative AI Process: The LLM, an "off-the-shelf Code Llama at 37" (01:44), initially produces a PlusCal version and then iteratively uses TLA+ tools available in a VS Code extension (parser, list symbol tool, model check & simulate tool) to refine the specification.
00:01:24 AI Debugging and Model Checking: The LLM interacts with TLC output to identify and fix errors in the generated specification and configuration files, eventually arriving at a parseable model. It then runs model checking with TLC.
00:02:02 Counter-Example Identification: The LLM successfully identifies a counter-example from the TLC output and explains what is happening.
00:02:19 Demo Limitations & Real-World Value: The presenter acknowledges that the "Die Hard" example might be in the AI's training data and the demo required multiple attempts. However, they have found this AI-assisted approach beneficial for real-world productivity.
00:02:45 Announcing the "GenAI Accelerated TLA+ Challenge": The TLA+ Foundation, in collaboration with Nvidia, launches a challenge (nicknamed the "TL-AI Challenge") to encourage novel integrations of GenAI/LLMs with TLA+.
Second and Third prizes: One-year subscriptions to GitHub Copilot and GitHub Copilot Plus, sponsored by the TLA+ Foundation.
00:03:58 Core Challenge Requirement - Grounded Results: Submissions should focus on practical applications where LLM outputs are "grounded in reality" and verifiable (e.g., using TLC for model checking), rather than unverified or "artistic" generations.
00:04:37 Tooling and Jury: Participants can use any tools (TLA+ tools, TLC, VS Code refactorings). The jury will be the TLA+ Specification Language Committee (SLC).