Reproduce “Supporting Software Formal Verification with Large Language Models: An Experimental Study” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Weiqi Wang, Marie Farrell, Lucas C. Cordeiro, Liping Zhao
A framework named SpecVerify automates the transformation of natural language requirements into C code assertions for formal verification, leveraging Large Language Models to streamline the process. The approach achieved full automation, matched traditional tools in verification rates, and identified previously undetected errors, particularly subtle floating-point issues, showing 79.31% logical equivalence to manually created properties.
Key insights
- Large Language Models can significantly automate the formal verification workflow, reducing manual intervention in requirements formalization and property generation, thereby lowering barriers to entry for formal methods.
- LLM-driven property generation enhances expressiveness, enabling the formalization of complex requirements by automatically incorporating auxiliary variables for intricate temporal and historical conditions.
- The quality and clarity of input natural language requirements are paramount, as ambiguities or poorly formalized descriptions lead to inadequate verification properties even with advanced LLMs.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.