AI Insight
Researchers developed Monty, a framework that uses large language models to automatically convert natural language software specifications into formal, executable assertions for code testing and verification. The system addresses validity and ambiguity issues through a novel conformance scoring metric and validity testing against actual code. Testing on 541 assertion-generation tasks from 22 Java classes showed that Monty improves precision by up to 20 percentage points compared to naive LLM translation approaches.
Why it matters
This work could significantly reduce the time and errors involved in writing formal software contracts, which are critical for ensuring software reliability and correctness. By bridging the gap between informal developer intentions and formal specifications, it has potential to make rigorous software verification more accessible and practical for developers.
Understand the Science
arXiv:2607.13303v2 Announce Type: replace-cross
Abstract: Formal contracts are essential for software testing and verification, yet writing them remains labor-intensive and error-prone. LLMs offer a promising path toward autoformalization: synthesizing executable assertions from natural-language specifications and thereby bridging the gap between informal developer intent and formal executable specifications. We present Monty: an autoformalization framework for assertions that tackles the challenges of expectations of validity of assertions and ambiguity in natural-language. Our techniques are based on filtering formalizations using a novel conformance score metric and validity scores obtained from testing the code against formalized assertions. We evaluate our approach on 541 assertion-generation tasks derived from 22 collection-like Java classes, and show that our technique produces the ground truth more reliably (improving upto 20 points in precision on average) than when using LLMs naively to translate assertions.
Source: Faithful Autoformalization of Natural Language Assertions