SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems
This work addresses the challenge of assessing AI for formal modeling in critical computing infrastructures, providing a foundational tool for research, though it is incremental as it builds on existing specification languages and evaluation methods.
The authors tackled the problem of evaluating AI's ability to formally model large, complex real-world systems, such as concurrent and distributed systems, by introducing SysMoBench, a benchmark that automates metrics like syntactic correctness and conformance to system code, and includes nine diverse system artifacts like Raft implementations and OS components.
Formal models are essential to specifying large, complex computer systems and verifying their correctness, but are notoriously expensive to write and maintain. Recent advances in generative AI show promise in generating certain forms of specifications. However, existing work mostly targets small code, not complete systems. It is unclear whether AI can deal with realistic system artifacts, as this requires abstracting their complex behavioral properties into formal models. We present SysMoBench, a benchmark that evaluates AI's ability to formally model large, complex systems. We focus on concurrent and distributed systems, which are keystones of today's critical computing infrastructures, encompassing operating systems and cloud infrastructure. We use TLA+, the de facto specification language for concurrent and distributed systems, though the benchmark can be extended to other specification languages. We address the primary challenge of evaluating AI-generated models by automating metrics like syntactic and runtime correctness, conformance to system code, and invariant correctness. SysMoBench currently includes nine diverse system artifacts: the Raft implementation of Etcd and Redis, the Spinlock and Mutex in Asterinas OS, etc.; more artifacts are being actively added. SysMoBench enables us to understand the capabilities and limitations of today's LLMs and agents, putting tools in this area on a firm footing and opening up promising new research directions.