Validating Autoformalized Specifications via Contrapuntal Languages

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.