TLDR: This paper introduces NL2Contract, a novel approach that enables Large Language Models (LLMs) to infer complete formal functional contracts, including both preconditions and postconditions, from natural language descriptions in code. The research demonstrates that these AI-generated contracts significantly improve automatic software verification by reducing false alarms and effectively discriminating between buggy and correct behavior. Evaluations with various LLMs show that NL2Contract outperforms previous postcondition-only methods, leading to more accurate detection of real-world bugs and uncovering inconsistencies between documentation and implementation.
In the world of software development, ensuring that programs work exactly as intended is a monumental challenge. Automatic software verifiers, tools designed to check code against formal specifications, have become increasingly powerful. However, their widespread adoption has been hindered by a fundamental problem: real-world code often lacks these crucial formal specifications. Developers typically rely on informal natural language descriptions, like comments and function documentation, to explain what their code should do.
Previous attempts to bridge this gap have explored using Large Language Models (LLMs) to infer formal postconditions – descriptions of what should be true after a function executes – from these natural language hints. While promising, these postcondition-only specifications often led to a high number of ‘false alarms’ during verification, where the verifier incorrectly flagged potential issues that weren’t actual bugs. This happens because LLMs, when only asked for postconditions, tend to overlook important input assumptions, leading to specifications that are only valid for a subset of inputs.
Introducing NL2Contract: A Comprehensive Approach
To tackle this limitation, researchers Cedric Richter and Heike Wehrheim from Carl von Ossietzky Universität Oldenburg introduced a new task called NL2Contract. This approach leverages LLMs to translate informal natural language into complete formal functional contracts, which include both preconditions (assumptions about inputs) and postconditions (expected output behavior). The goal is to create specifications that are not only sound but also highly effective at distinguishing between correct and buggy software behavior, ultimately making automatic software verification more practical.
The paper, titled “Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?”, outlines key metrics to validate and compare different NL2Contract approaches. These metrics focus on the soundness of the generated contracts, their power to discriminate bugs, and their overall usability within automatic software verification systems.
Key Findings from the Evaluation
The researchers evaluated NL2Contract using various LLMs, including GPT-5 (Chat), GPT-4o, and CodeQwen 2.5, and compared it against the existing nl2postcond approach. The results were compelling:
-
Effective Contract Generation: LLMs are generally effective at generating functional contracts that are sound for all possible inputs. This means the contracts accurately reflect the intended behavior without flagging correct code as faulty.
-
Bug Discrimination: The generated contracts are sufficiently expressive to differentiate between buggy and correct behavior. This is crucial for identifying real problems in the code.
-
Reduced False Alarms: When automatic verifiers are supplied with LLM-inferred functional contracts (both pre- and postconditions), they produce significantly fewer false alarms compared to when they are given postconditions alone. This dramatically improves the efficiency and trustworthiness of verification tools.
Further investigations revealed that LLM-inferred preconditions align well with developers’ intentions. This allows automatic software verifiers to catch real-world bugs more accurately. For instance, in an example involving a 24-hour clock conversion, the LLM-generated preconditions correctly identified invalid inputs, preventing false alarms and guiding the verifier to a genuine bug.
Also Read:
- Beyond Functional Correctness: A New Framework for Evaluating Code Generation LLMs’ Adherence to Software Contracts
- TyFlow: Guiding Language Models to Master Type Correctness in Code Generation
Practical Impact and Future Potential
The study highlights the practical benefits of NL2Contract. On the HumanEval+ benchmark, LLMs using NL2Contract were significantly better at producing verification-sound specifications. When applied to the Python-by-Contract dataset, which contains real-world bugs, the NL2Contract specifications enabled software verifiers to automatically detect 14 out of 19 identifiable bugs, while also drastically reducing false alarms. This demonstrates a clear advantage over postcondition-only methods.
The research also uncovered an interesting aspect: LLM-inferred specifications can help identify inconsistency bugs. For example, in an approximation of a square root function, the LLM-generated postcondition revealed a subtle discrepancy between the natural language documentation (which stated ‘less than eps’) and the actual implementation (which allowed ‘less than or equal to eps’). Such insights can help developers refine both their code and documentation for greater consistency and reliability.
In conclusion, NL2Contract represents a significant step forward in leveraging LLMs for formal specification inference. By enabling LLMs to generate comprehensive functional contracts, including both preconditions and postconditions, this research paves the way for more effective software validation and automatic bug detection, ultimately contributing to the development of more robust and reliable software systems.
