Search papers, labs, and topics across Lattice.
This paper introduces Monty, an autoformalization framework that synthesizes executable assertions from natural-language specifications, addressing the labor-intensive and error-prone nature of writing formal contracts for software testing. By employing a novel conformance score metric and validity scores from code testing, Monty effectively filters formalizations to enhance the reliability of assertion generation. The evaluation on 541 tasks derived from Java classes demonstrates a significant improvement in precision, achieving up to 20 points higher than naive LLM translation methods.
Monty achieves up to 20 points higher precision in generating executable assertions from natural language compared to naive LLM approaches, revolutionizing software verification processes.
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.
