Source note
Faithful Autoformalization of Natural Language Assertions
Code IntelligenceAutomated Software ProductionSoftware Foundation ModelGenerative EngineeringHuman AI Interaction
Summary
Monty improves the reliability of translating natural-language method assertions into executable JML specifications by combining LLM generation, testing, clausal-conformance scoring, and user-guided disambiguation. On 541 tasks across 22 Java collection-like classes, it increased precision by as much as 20 percentage points over naive LLM translation while retaining high recall.
Problem
- Writing formal contracts for software testing and verification is labor-intensive, yet incorrect translations can either flag correct code or allow buggy code to pass.
- Natural-language assertions are ambiguous, and existing autoformalization methods often assume that the assertion should be valid for the implementation, which is unsuitable for testing code or validating AI-generated code.
Approach
- Monty prompts an LLM to generate multiple candidate JML assertions from a natural-language assertion and a Java class or method context.
- It filters candidates with syntax checks, fuzz-safety checks, and fuzz-semantic tests generated with Randoop, while retaining both likely test-valid and test-invalid interpretations.
- Its clausal coverage metric has an LLM describe each formal assertion in natural language and score bidirectional clause matching against the original assertion; candidates below a 0.6 conformance threshold are removed in the experiments.
- When valid and invalid candidates remain, active learning produces a distinguishing program valuation for the programmer or an oracle to resolve the ambiguity.
Results
- The evaluation covers 541 natural-language/formal-specification pairs from 22 Java classes representing collection-like data structures, including both valid and invalid assertions.
- With Qwen2.5-Coder, a 32B-parameter model, Monty increased precision from 75% to 91.6% on one dataset and from 64% to 85% on another.
- These gains amount to improvements of 16.6 and 21 percentage points, respectively, while the paper reports that recall remained high.
- Ablation studies found clausal coverage more effective for conformance checking than the evaluated baseline approaches, and showed that precision gains were more pronounced with smaller models.
- The excerpt does not provide exact recall values, full baseline configurations, or confidence intervals, so the reported improvement is bounded to the supplied benchmark and experimental settings.