PaperlayerView exact revision on arXiv

Source-linked AI summary

Validating Autoformalized Specifications via Contrapuntal Languages

Yihan Dai, Xuanlin Liu, Haoxiang Jia, Tianchi Li, Xin Zhang, Sergey Mechtaev

arXiv:2610.30059v1cs.SE

TL;DR

Autoformalized specifications are untrusted, and validating them without costly human review is challenging when model errors are correlated. The paper synthesizes structurally incompatible formal languages and accepts specifications only when a solver proves their formalizations equivalent. Across HumanEval+ and LiveCodeBench, it reports more accepted specifications that are complete and sound than the strongest baseline.

  • Problem

    Autoformalized specifications may not capture user intent, while costly human review makes oracle-free validation a central bottleneck and correlated model errors can undermine voting.

    Source: §1 · p. 1

  • Method

    The approach independently formalizes intent in two synthesized, structurally incompatible task-specific languages and accepts a specification only when a solver proves the formalizations equivalent.

    Source: §1 · p. 2

  • Results

    12.0% on HumanEval+ and 42.9% on LiveCodeBench higher proportions of accepted specifications are complete and sound than under the strongest baseline.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The results support deliberately structured representational diversity as a way to make agreement more informative for specification validation.

    Source: §9 · p. 19

    Evaluation covers two benchmarks and three configurations; other settings and formalisms need further evaluation, and cross-language disagreement surfaces plausible alternatives but cannot determine user intent.

    Source: §7 · p. 17

Abstract

from arXiv · show

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.

1 Introduction

Autoformalized specifications need validation because they are fallible, while human review is costly and model outputs can share errors. The paper uses structurally incompatible languages and solver-checked equivalence to validate specifications, reporting gains on two benchmarks.

1 Introduction

  • Autoformalization shifts trust to whether a fallible specification captures intent, and costly human review makes oracle-free validation important.LLMs struggle to generate behaviorally correct postconditions and contracts; on HumanEval, only 39.5% of GPT-5-generated contracts that raised no false alarms rejected every evaluated mutant.Source: §1 · pp. 1–2
  • Voting can reinforce correlated errors, while treating each candidate as indivisible overlooks useful components in incorrect specifications.Reusing fragments naively may steer models toward the same formalizations and errors.Source: §1 · p. 2
  • Contrapuntal languages express the intended specification but lack a structure-preserving translation between them; independent formalizations are accepted only when a solver proves equivalence.The approach is implemented for first-order logic in SMT-LIB and evaluated with GPT-5.4 mini and Qwen3.6-Flash, with and without thinking.Source: §1 · p. 2
  • A synthesis algorithm cuts sampled seed specifications into fragments and uses a solver to choose differently shaped representations across the two languages.Every seed must be representable in both languages, but its representations must lack an AST-level structure-preserving translation.Source: §1 · p. 2
  • 12.0% on HumanEval+ and 42.9% on LiveCodeBench more accepted specifications are complete and sound than under the strongest baseline; complete accepted specifications reject 98.6% and 96.2% of buggy variants, respectively.The strongest baseline rejects 92.8% of buggy variants on HumanEval+ and 78.3% on LiveCodeBench.Source: §1 · p. 2

2 Motivating Example

The HumanEval/135 example shows why plurality voting and naive seed splitting can fail, and how contrapuntal languages reuse useful fragments while forcing different formalization paths.

2 Motivating Example

  • For can_arrange, the dominant incorrect specification is sampled with probability 0.27 (8/30), exceeding the correct specification’s 0.17 (5/30).The incorrect specification is complete but unsound: it also permits −1 when a valid index exists.Source: §2 · p. 3
  • Plurality can select a correlated error over the correct specification and ignores useful components that incorrect candidates may contain.The example uses those fragments as a task-specific vocabulary for synthesizing a language from seed formalizations.Source: §2 · pp. 3–4
  • Splitting seeds can make languages too different to match correct formalizations, yet not different enough to prevent the same error from recurring.In the example, L′1 has no correct specification, while an incorrect L′2 specification is equivalent to seven under L′1.Source: §2 · p. 4
  • Contrapuntality balances adequacy, so both languages can express the intended specification, with non-isomorphism preventing structure-preserving translations between them.Here, structure refers to AST shape; vocabulary-only differences leave the tree shape unchanged and reduce validation to plurality voting.Source: §2 · pp. 4–5
  • In the example, contrapuntal languages reuse structures from correct seeds and reshape incorrect fragments, yielding equivalent formalizations that are accepted.The two languages obtain constructs 5 and 5′, which prevent unconditional acceptance of r = −1.Source: Figure 2 · p. 4, §2 · p. 5
  • On arr = [6, 0, 1, 2, 3], the plurality-selected specification admits the mutant’s incorrect −1 output, while Formula III rejects it because index 1 has a descent.The mutant’s backward scan stops before index 1; the intended result is 1, so the specification check kills this mutant under Formula III.Source: §2 · p. 5

3 Background & Notation

The paper defines formulas by their syntax and semantics, distinguishes intended behavior from formalized behavior, and builds task-specific languages as syntactic sugar over first-order logic.

3 Background & Notation

  • The base language L0 is first-order logic interpreted over fixed domains, and formulas are equivalent when they admit the same variable assignments.SMT-LIB provides the common solver input language used to check equivalence automatically.Source: §3 · p. 5
  • A language has an alphabet, well-formed formula trees, and a semantics mapping formulas to sets of variable assignments; positions address nodes and subtrees in those trees.The paper distinguishes object-language symbols from meta-language notation, including syntax-tree identity and semantic equivalence.Source: §3 · pp. 5–6
  • Sugared-language constructs abbreviate fixed L0-formula patterns, and desugaring recursively replaces each construct with its definition.A construct’s definition uses holes for its arguments, and an L-formula denotes what its desugaring denotes.Source: §3 · p. 6
  • A formula’s sugarings are the language formulas that desugar to it without variable capture.Bound variables in the desugared formula must originate from the same node as their quantifier in the sugared formula.Source: §3 · p. 6
  • A formalization is correct when its denotation equals the assignments intended by the natural-language specification; soundness and completeness are the two subset conditions.The intended denotation is known only to the user, so equivalence between a formula and the intent cannot be checked automatically.Source: §3 · p. 6
  • A language is adequate for an informal specification when its realization set—the correct formalizations in that language—is nonempty.Adequacy therefore requires at least one correct formalization in the language.Source: §3 · p. 6

4 Contrapuntal Languages

Contrapuntal languages must both express the intended specification while preventing structure-preserving translations between correct formalizations. Because this ideal cannot be checked directly, the section replaces it with a decidable, seed-based criterion.

4 Contrapuntal Languages

  • Contrapuntal languages require both adequacy and non-isomorphism: each language can express the intent, but their correct formalizations have no structure-preserving translation.The section presents these paired properties as the conditions that make cross-checking formalizations useful.Source: §4 · p. 7
  • The ideal definition is not algorithmically checkable because intent semantics are inaccessible and proving non-isomorphism is undecidable in general.The latter difficulty remains even if the semantics are known.Source: §4 · p. 7
  • The effective criterion substitutes a finite set of seed formalizations for intent semantics and checks only their syntactic sugarings.For each seed, both languages must admit a sugaring, and no sugaring in one may translate structure-preservingly to one in the other; these finite sets make the criterion decidable.Source: §4 · p. 7
  • In the example, L1 and L2 sugar the same seeds into differently sized trees, but extending L2 creates a sugaring that L1’s tree can reach by relabeling.This shows how adding a construct can remove effective contrapuntality even when the language pair previously satisfied it.Source: §4 · p. 8

5 Synthesis of Contrapuntal Languages

The synthesis method searches cuts of seed formula trees, turning fragments into constructs while requiring paired fragment trees to differ in shape. It encodes these constraints and uses matching and cutting subroutines to build and check the languages.

5 Synthesis of Contrapuntal Languages

  • Cuts partition a seed into fragments, each of which becomes a construct with holes; the resulting fragment tree desugars to the seed.The synthesis search requires the two cut sets to yield fragment trees of different shapes.Source: §5 · p. 8

5.1 Incremental Synthesis Algorithm

  • The incremental backtracking algorithm adds constructs seed by seed, rechecks integrated seeds for same-shaped sugarings, and terminates with an effectively contrapuntal pair if it returns one.It may return none even when such a pair exists.Source: §5.1 · pp. 8–9

5.2 Encoding Shape Constraints

  • The shape encoding records fragment-tree positions in arrays and constrains definedness, domination, sibling order, and matching shapes; binder constraints keep bound occurrences with their quantifiers.A same-shape constraint holds exactly when the two fragment trees have the same positions.Source: §5.2 · pp. 9–10

5.3 Subroutines Cut and FindIso

  • Cut reuses compatible construct matches where possible, then chooses cuts in the unmatched remainder so the two fragment trees differ in shape.MaxSat selects a largest compatible set of matches; the cutting query freezes their cuts and searches the remainder.Source: §5.3 · p. 11
  • FindIso searches existing construct matches for same-shaped sugarings, returning a witness when it finds one and none when no seed admits such a pair.The adopted matches define the sugarings that witness the violation of the shape constraint.Source: §5.1 · p. 8, §5.3 · pp. 11–12

6 Evaluation

The evaluation tests contrapuntal-language validation on two benchmarks and finds higher correctness than comparison methods, alongside lower task coverage. It also examines the role of contrapuntality, error agreement, token costs, failures, and an ambiguous task description.

6 Evaluation

  • The evaluation uses HumanEval+ and LiveCodeBench, three model settings, a 30-response sampling budget, and input–output pairs from reference tests and mutants.Mutants provide negative examples for assessing whether specifications reject buggy program behavior.Source: §6 · pp. 12–13

6.1 RQ1: Effectiveness of Specification Validation

  • At τ=0.8/1.0, Avg. CR gains over round-trip are 22.13/20.76 percentage points and over plurality voting are 22.79/22.10 points.Table 1 reports the validation results for accepted specifications; the paper also reports gains in other joint metrics.Source: §6.1 · p. 13, Table 1 · p. 14
  • Contrapuntal languages cover 29.81% of HumanEval+ tasks and 8.76% of LiveCodeBench tasks, below both baselines but closest to seed availability, the upper bound on correct acceptance.The authors characterize this lower coverage as conservative: an incorrect specification can let a buggy program pass, while a rejected task is flagged unresolved.Source: §6.1 · p. 14

6.2 RQ2 (Ablation): Impact of Contrapuntality

  • Compared with the full approach, the relaxed variant has average relative decreases of 15% in CR and 34.5% in Avg. CR.The relaxed variant breaks the contrapuntality guarantee while retaining the subsequent formalization and equivalence-checking procedure.Source: §6.2 · pp. 14–15

6.3 RQ3: Mitigating Correlated Errors

  • Average error coincidence falls from 25.23% to 21.88% on HumanEval+ and from 10.07% to 5.72% on LiveCodeBench for cross-language versus single-language pairs.Error coincidence measures how often two incorrect specifications belong to the same semantic equivalence class.Source: §6.3 · p. 15

6.4 RQ4: Token Usage

  • Contrapuntal languages use 1.4× as many tokens as plurality voting and 2.5× as many as round-trip verification on average.Their prompts include synthesized language constructs, increasing input tokens; more compact outputs generally do not offset that increase.Source: §6.4 · pp. 15–16, Table 2 · p. 16

6.5 RQ5: Analysis of Failure

  • False-positive failures account for 38.9% of 216 failures, while false negatives account for the remaining 61.1%.The languages still share seed formalizations, so representational diversity does not eliminate correlated errors; false negatives include invalid candidates, unmatched language pairs, and failed language synthesis.Source: §6.5 · p. 16

6.6 Case Study: Ambiguous Task Descriptions

  • For HumanEval/154, the empty-second-word interpretation requiring False forms 8 of 10 candidates in L1, while all 10 L2 candidates require True.The cross-language disagreement makes the unresolved empty-word convention explicit as a decision for the user; the figure depicts the contrasting interpretations.Source: §6.6 · p. 17, Figure 7 · p. 17

7 Threats to Validity

The evaluation is limited by behavioral test coverage, mutant selection, and the scope of the benchmarks and intent interpretations. These constraints bound what the reported completeness and soundness judgments establish.

Behavioral evaluation

  • Completeness and soundness are judged against tested behaviors, not exhaustive semantic correctness; killing a mutant shows only that an observed incorrect output is rejected.The same tests and criteria are applied to all methods, enabling comparison within the intended input domain.Source: §7 · p. 17

Test-suite and mutant selection

  • Test reduction may omit inputs that distinguish specifications, and the selected mutants represent only a limited set of faults.Reduction criteria preserve branch coverage and mutant detection for the programs used, while LiveCodeBench combines real wrong-answer submissions with LLM-generated variants.Source: §7 · p. 17

Generalizability and interpretation of intent

  • Evaluation covers two benchmarks and three configurations across two model families, so generalization to other settings and specification formalisms requires further evaluation.Reference outputs represent one interpretation of benchmark intent; ambiguous descriptions may admit alternatives, and resolving them requires confirmation from the requirement author or user.Source: §7 · pp. 17–18

8 Related Work

Related work addresses autoformalization, consistency-based selection, specification synthesis, and behavioral evaluation. This paper instead validates specifications by checking agreement across synthesized, structurally distinct formal representations.

LLM-based autoformalization and specification generation

  • Prior autoformalization work generates specifications in a target formalism, while oracle-free validation of whether they capture intent remains challenging.The paper studies validation using two task-specific formal representations as validation views.Source: §8 · p. 18

Consistency-based validation and candidate selection

  • The plurality baseline accepts specifications in the largest SMT-checked equivalence class, while round-trip verification checks equivalence after back-translation and re-formalization.User-assisted disambiguation workflows are outside the oracle-free comparison; adapting semantic triangulation would require specification-level transformations and consistency relations.Source: §8 · p. 18

Decomposition, reuse, and intermediate representations

  • Unlike systems that reuse clauses or expose structured sub-translations, this approach synthesizes two deliberately different decompositions of the same seeds for validation.The cited systems address generation, repair, or logic-specific translation rather than the validation setting studied here.Source: §8 · p. 18

Evaluation of generated specifications

  • Without reference formal specifications, the paper follows test-based evaluation using positive tests, negative tests, and mutant killing as behavioral approximations of specification quality.Prior approaches also use tests and mutated outputs, while other methods rely on reference formalizations or deductive verification.Source: §8 · p. 18

SMT-based synthesis and repair

  • Unlike SMT-based synthesis of programs or repairs, this work uses SMT to construct formal languages by constraining cuts of seed formulas and resulting fragment-tree shapes.The constraints aim to obtain an effectively contrapuntal language pair.Source: §8 · pp. 18–19

9 Conclusion

The paper presents an oracle-free method that validates autoformalized specifications through solver-checked agreement across contrapuntal languages. On two benchmarks, it improves the proportion of accepted specifications that are complete and sound over the strongest baseline on average.

9 Conclusion

  • The approach improves the proportion of accepted specifications that are complete and sound over the strongest baseline on average across HumanEval+ and LiveCodeBench.The experiments support deliberately structured representational diversity as a way to make agreement more informative for specification validation.Source: §9 · p. 19
  • Contrapuntal languages are task-specific formal-language pairs designed to express the intended specification but lacking a structure-preserving translation between them.The method guides an LLM to formalize the same intent along different representational paths and uses solver-checked agreement as evidence of correctness.Source: §9 · p. 19
  • The conclusion presents solver-checked agreement across these languages as evidence for oracle-free validation of autoformalized specifications.The languages are designed to express the intended specification while differing structurally.Source: §9 · p. 19

Supplementary Materials

The appendix illustrates syntactic sugar by showing how two differently shaped sugarings of Formula I desugar to the same formula. The example identifies the constructs, fragments, and cuts that define those sugarings.

Supplementary Materials

  • Formula I is represented as a tree with eleven nodes, and positions identify its root and subtrees.The appendix uses d and ℓ as abbreviations for descend_at and largest.Source: A Example of Syntactic Sugar · p. 22
  • The example language L has five constructs, including unary, binary, and constant constructs whose definitions contain holes and non-hole nodes.Their definitions include the disjunction, conjunction, descend_at, and largest fragments used in Formula I.Source: A Example of Syntactic Sugar · p. 22
  • Two sugarings, χ1 and χ2, desugar to the same Formula I while carving it into fragments in different tree shapes.The example states that the sugarings have three versus four nodes, illustrating the non-isomorphism requirement.Source: Figure 8 · p. 22, A Example of Syntactic Sugar · p. 23

B Proof of Theorem 5.2

The proof establishes that Synth terminates, preserves each seed through desugaring, and returns languages with no structure-preserving translation between them.

B Proof of Theorem 5.2

  • Synth terminates because each loop iteration adds a previously absent extension, and recursive calls consume a finite seed list.The proof bounds recursion depth by the number of seeds.Source: B Proof of Theorem 5.2 · p. 23
  • Each seed is preserved: its cut-set fragment tree belongs to the constructed language and desugars back to the seed.The bound on cuts prevents separating a bound-variable occurrence from its quantifier.Source: B Proof of Theorem 5.2 · p. 23
  • The returned languages admit no structure-preserving translation, because no seed has same-shaped sugarings in both languages.The proof uses the absence of such a seed pair to establish the theorem’s non-isomorphism condition.Source: B Proof of Theorem 5.2 · p. 23

C Sample Size Setting

The sample-size study tracks semantic entropy across specification equivalence classes on HumanEval+ tasks. Entropy gains diminish as the sampling budget grows, motivating N=30 as a practical trade-off.

C Sample Size Setting

  • The study measures semantic entropy over equivalence classes among successful generations, excluding failed generations.The class probabilities use each class’s share of successful generations in the first N sampling attempts.Source: C Sample Size Setting · p. 23
  • Mean entropy rises from 1.436 bits at N=5 to 2.839 bits at N=30, then gains only 0.329 bits (11.6%) from N=30 to 50 despite 66.7% more sampling.The reported mean averages task-level entropies across 161 HumanEval+ tasks; Figure 9 plots mean entropy against sample size.Source: C Sample Size Setting · p. 24, Figure 9 · p. 24
  • The authors select N=30 as a practical trade-off between representing specification diversity and limiting sampling and equivalence-analysis costs.The entropy curve continues to rise beyond N=30, but with progressively smaller gains.Source: C Sample Size Setting · p. 24

D Full threshold Results for RQ1

Across the tested thresholds, contrapuntal languages lead in task-level macro-averages in all six model–benchmark settings. They lead sample-level metrics in five settings, with two HumanEval+ exceptions at particular thresholds.

D Full threshold Results for RQ1

  • The analysis extends Table 1’s joint metrics across τ∈[0, 1], using the same sample-selection, acceptance, and averaging rules.The step curves include every empirical threshold at which the set of τ-complete specifications changes.Source: D Full threshold Results for RQ1 · p. 24
  • Contrapuntal languages lead Avg. MKR|C and Avg. CR throughout τ∈[0, 1] in all six model–benchmark settings.Figures 10 and 11 show threshold sensitivity on HumanEval+ and LiveCodeBench; rows denote models and columns denote metrics.Source: Figure 10 · p. 24, Figure 11 · p. 25, D Full threshold Results for RQ1 · p. 25
  • They lead both sample-level metrics throughout the range in five of six settings, with two exceptions on HumanEval+.Plurality voting has higher MKR|C with GPT-5.4 mini below τ=0.2; round-trip verification has higher CR with Qwen3.6-Flash in thinking mode at some high thresholds, including τ=1.Source: D Full threshold Results for RQ1 · p. 25
Loading 2610.30059v1…