Validating AI formal code specs using paired distinct languages
Validating Autoformalized Specifications via Contrapuntal Languages
Software Engineering
Summary
When AI turns natural language into formal rules for computer programs, these rules can still have mistakes. The authors show a way to check these rules by translating the task into two very different formal languages that express the same idea but cannot be easily converted into each other. If the AI produces matching rules in both languages that a solver proves equivalent, the rules are much more likely to be correct. This approach improves detecting good program specifications without needing human reviewers.
What this means in practice
- •For software developers: Validate AI-generated formal program specifications to reduce bugs and increase confidence without needing costly human review.
- •For automated testing teams: Improve automated testing suites by accepting only formally verified task specifications derived from natural language descriptions.
Authors
Yihan Dai, Xuanlin Liu, Haoxiang Jia, Tianchi Li, Xin Zhang, Sergey Mechtaev
Abstract
Formal specifications can make AI-generated code mechanically checkable. Because user intent is typically expressed in natural language rather than formal logic, specifications must first be derived from it, e.g., via LLM-based autoformalization. Yet autoformalized specifications are themselves untrusted, so a key challenge is validating whether they capture user intent without relying on a costly oracle such as human review. In this oracle-free setting, a natural strategy is to vote among model outputs, but because model errors are often correlated, agreement among outputs may reflect shared mistakes rather than correctness. Our key insight is that these errors can be decorrelated through representational diversity. We achieve this diversity with contrapuntal languages: pairs of task-specific formal languages, each designed to express the intended specification, yet admitting no structure-preserving translation between them. An LLM formalizes the intent independently in each language, and we accept a specification only if a solver proves the two formalizations equivalent. To construct such languages, we present a synthesis algorithm that reuses fragments of sampled seed specifications as syntactic sugar over a base specification language. We implement the approach for first-order logic specifications and evaluate it on HumanEval+ and LiveCodeBench using GPT-5.4 mini and Qwen3.6-Flash with and without thinking. Over the strongest baseline, our method increases the proportion of accepted specifications that are correct, i.e., complete and sound, by 12.0% on HumanEval+ and 42.9% on LiveCodeBench. The accepted specifications judged complete reject 98.6% of buggy program variants on HumanEval+ and 96.2% on LiveCodeBench, compared with 92.8% and 78.3% for the strongest baseline.