Validating Autoformalized Specifications via Contrapuntal Languages

CCS Concepts: • Software and its engineering → Automatic programming; Formal software verification; • Computing methodologies → Natural language processing.

Additional Key Words and Phrases: Intent Autoformalization, Specification Validation, Large Language Models

Introduction

As large language models (LLMs) generate code faster than humans can review it [7, 27], the central challenge is shifting from generating code to determining whether that code faithfully captures the user’s intent. A promising answer is intent autoformalization: automatically translating natural-language intent into formal specifications against which generated code can be mechanically verified. Yet this only relocates the trust problem: if the specification is itself produced by a fallible autoformalization process, does it capture the user’s intent expressed in natural language? Prior studies on HumanEval tasks show that generating behaviorally correct postconditions and contracts

Authors’ Contact Information: Yihan Dai, Peking University, Beijing, China, [email protected]; Xuanlin Liu, Nankai University, Tianjin, China, [email protected]; Haoxiang Jia, Peking University, Beijing, China, [email protected]; Tianchi Li, Peking University, Beijing, China, [email protected]; Xin Zhang, Peking University, Beijing, China, [email protected]; Sergey Mechtaev, Peking University, Beijing, China, [email protected]. from natural-language intent remains challenging for LLMs [8, 29, 30]. For example, even for Python contracts on HumanEval, the setting most familiar to LLMs, only 39.5% of GPT-5-generated contracts that raised no false alarms on the reference implementation rejected every evaluated mutant [30]. However, validating generated specifications typically requires costly human review, making oracle-free validation a central bottleneck for reliable AI-assisted software development [17].

How can we validate whether autoformalized specifications accurately capture the user’s intent without an external oracle? A straightforward approach is voting. Plurality voting [10, 19] partitions the specifications into equivalence classes and selects the largest, i.e., the most frequently occurring semantics. However, LLM-generated artifacts often exhibit correlated errors [15]; when multiple candidates share the same mistake, plurality voting can reinforce the dominant error rather than identify the correct answer [31]. Also, plurality voting treats each candidate as an indivisible vote, ignoring its internal structure: a candidate need not be correct as a whole for some of its components to be useful. Clause2Inv [3], for example, shows that clauses extracted from invalid invariant candidates can contribute to a valid invariant. Yet reusing such fragments naively would steer the model back toward the same formalizations, and thus the same errors. The challenge is therefore to reuse useful fragments while inducing sufficiently different formalization paths.

To address these challenges, we build on the insight that representational diversity can break the correlation between errors. Inspired by linguistic determinism—the hypothesis that language shapes thought [33]—we introduce 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. Because the model must discover separately how to express the intent in each language’s constructs, cross-language agreement is less likely to reflect a correlated error than agreement within a single language.

To construct such languages, we present a synthesis algorithm that builds both languages as syntactic sugar over a base specification language. We first sample seed specifications for the task from the LLM; the algorithm then cuts each seed into fragments and turns them into language constructs, using a solver to choose cuts that carve every seed into differently shaped trees in the two languages. Since the intended specification is unknown, the seeds stand in for it: we call a language pair effectively contrapuntal for a seed set when every seed can be represented in both languages, but no AST-level structure-preserving translation relates its representations across them. This design also addresses the challenge of reusing fragments: seed fragments let the model reuse useful components, even from incorrect seeds, while the structural incompatibility of the two languages still forces separate formalization paths and thus decorrelates errors.

We implement the approach for first-order logic specifications in SMT-LIB and evaluate it on HumanEval+ [21] and LiveCodeBench [12] using GPT-5.4 mini and Qwen3.6-Flash with and without thinking. We compare it against direct generation, plurality voting, and round-trip verification, judging a specification complete if it accepts reference input–output pairs and sound if it rejects the outputs of buggy program variants. Over the strongest baseline, our method increases the proportion of accepted specifications that are both complete and sound by 12.0% on HumanEval+ and 42.9% on LiveCodeBench, and the accepted specifications judged complete reject 98.6% and 96.2% of buggy program variants, respectively, compared with 92.8% and 78.3% for the strongest baseline. An ablation shows that these gains depend on enforcing contrapuntality rather than merely using two languages, and a case study shows that disagreement between contrapuntal languages can surface ambiguity in a task description.

In summary, the paper makes the following contributions:

• A new approach that automatically validates autoformalized specifications without an oracle through contrapuntal languages.

• An algorithm to automatically synthesize contrapuntal languages with an SMT solver.

• An evaluation on HumanEval+ and LiveCodeBench showing that contrapuntal languages accept a higher proportion of complete and sound specifications than three baselines, and that the accepted specifications judged complete detect more bugs.

All code and data are available at https://figshare.com/s/be97e0291c8ce608bcd4.

Motivating Example

To illustrate the difficulty of validating autoformalized specifications without access to any intent oracle, we use HumanEval/135 as a running example. The task asks can_arrange(arr: list[int]) to return the largest index $i$ such that $\mathit{arr}[i] < \mathit{arr}[i - 1]$, or $-1$ if no such index exists.

When using Qwen3.6-Flash (thinking=on) to autoformalize this task into an SMT-LIB specification, it has a low success rate: the estimated probability of sampling a correct specification (formula III in Figure 1) is only 0.17, while the dominant incorrect one (the first formula in Figure 1) has the probability 0.27 (8/30) > 0.17 (5/30). This incorrect specification does accept the intended output on every observed positive example, but it also permits $r = -1$ when such valid index $r$ exists. It is therefore complete but unsound.

Plurality voting selects the most frequent semantic equivalence class among all sampled specifications. It can be ineffective because LLMs tend to produce correlated errors—a phenomenon observed not only across samples from the same model but even across different models [15]. In challenging cases like HumanEval/135, plurality voting amplifies rather than mitigates mistakes: as shown in Figure 1, it selects the dominant incorrect class over the correct one. Plurality voting also underuses the information in the candidate specifications, using them only to count equivalence classes. Yet a candidate need not be correct as a whole for some of its components to contribute to a correct specification: in Figure 1, the key components of the correct specification already appear in the incorrect ones. We therefore split candidates into small pieces that, like the building bricks in Figure 1, form a small, task-specific vocabulary. We call this process “synthesizing a language from seed formalizations”.

Autoformalization in a single language still suffers from correlated errors. To decorrelate them, we exploit linguistic determinism: we force the model to “think” differently by formalizing the intent in two different languages synthesized from the seeds. Figure 2 illustrates why these languages must be chosen carefully. If both are synthesized from the same seeds (top row), they may be identical, and cross-language validation reduces to plurality voting, preserving the correlated error. A natural remedy is to randomly split the seeds into two subsets and synthesize one language from each (middle row), yielding $\mathcal{L}'_1$ and $\mathcal{L}'_2$. This split-seed strategy, however, fails in two ways. First, it makes the languages too different: each exposes the LLM to different fragments, so their outputs diverge. Formalizations under $\mathcal{L}'_1$ contain no correct specification, whereas those under $\mathcal{L}'_2$ contain seven, so no correct specification can be accepted. Second, it does not make them different enough: splitting the seeds gives no control over correlated errors, and the incorrect formalization under $\mathcal{L}'_2$ is equivalent to seven under $\mathcal{L}'_1$, so the error is accepted anyway. Our ablation study (§ 6.2) shows that these failures are systematic rather than specific to this example.

These two failures suggest that the languages require a delicate balance: similar enough that correct formalizations can be matched across them, yet different enough that errors do not recur in both. We capture this balance with a property we call contrapuntality (formalized in Definition 4.2), which combines two requirements. Adequacy requires that both languages can express the intended specification; unlike split-seed languages, they thus offer comparable expressive power, so a correct formalization in one language has a counterpart in the other. Non-isomorphism requires that no structure-preserving translation relates formalizations across the two languages; the model therefore cannot reuse the structure of a formalization in one language when writing it in the other, making it less likely to repeat the same error in both. Here, structure refers to the shape of abstract syntax trees (ASTs): languages that differ only in vocabulary produce ASTs of the same shape for the same formula, so validating across them reduces to plurality voting.

With contrapuntal languages (bottom row of Figure 2), the example is handled correctly. On the one hand, the incorrect seeds are cut into different fragments and thus have different AST structures in the two languages, making it difficult for the same error to recur in both. On the other hand, since both languages are synthesized from all seeds, each can extract critical structures from the correct seeds—specifically, structures that prevent the LLM from unconditionally accepting $r=-1$. For example, $L_1''$ obtains construct 5 and $L_2''$ obtains construct 5′. Formalizations in both languages use these structures, form equivalent pairs, and are therefore accepted.

The distinction matters when the validated specification is used to check generated code. Consider this buggy implementation of can_arrange, whose backward scan stops before index 1:

def can_arrange(arr):
    for i in range(len(arr) - 1, 1, -1):
        if not (arr[i] >= arr[i - 1]):
            return i
    return -1

On input $arr=[6, 0, 1, 2, 3]$, the mutant returns $r=-1$, whereas the intended result is $r=1$ because $arr[1] < arr[0]$. Formula I, selected by plurality voting, admits the incorrect input–output pair $(arr,-1)$, so the mutant survives the specification check. In contrast, the specifications accepted by our method realize Formula III, which permits $r=-1$ only when no decreasing adjacent pair exists. Because $descend\_at(1,arr)$ holds, Formula III is unsatisfiable for $r=-1$, so it rejects the incorrect behavior and kills the mutant. Thus, more reliable specification validation translates directly into stronger bug detection. Beyond bug detection, disagreement between contrapuntal languages can also surface ambiguity in the task description, as our case study shows (§ 6.6).

Background & Notation

Presenting our approach requires writing formulas in formal languages while also reasoning about these languages. We therefore distinguish the object languages, in which formulas are written, from the meta-language, in which we reason about them. Greek letters are placeholders, called meta-variables: $\varphi$, $\psi$, $\chi$ stand for arbitrary formulas and $\pi$, $\rho$ for arbitrary positions. All other symbols stand for themselves, with two exceptions: $x$ stands for an arbitrary object variable, and the names we define for particular formulas and variables, such as $\operatorname{Def}^{i}$ and $c^{i}_{n}$ in § 5.2, stand for what they name. Thus, $p(\nu) \land q(\nu)$ is a concrete formula, whereas $\varphi\land\psi$ denotes the conjunction of the formulas that $\varphi$ and $\psi$ stand for. We also distinguish three kinds of equality: $=$ is meta-level identity, which for formulas means identity of their syntax trees; $=$ is the equality symbol of the object language; and $\equiv$ is semantic equivalence (defined below). For example, $\varphi\land\varnothing\ne\varphi$, yet $\varphi\land\psi= \varphi$.

Our approach targets specifications written in first-order logic, the common input language of SMT solvers, standardized by SMT-LIB [2]; this lets us check the equivalence of formalizations automatically. These formulas form the base language $\mathcal{L}_0$: they are built as usual from atoms, object equality $\doteq$, the connectives $\neg$, $\land$, $\lor$, $\to$, $\leftrightarrow$, the constants $\top$ and $\bot$, and the quantifiers $\forall$ and $\exists$. We interpret formulas over fixed domains, such as the integers and arrays, in which function and predicate symbols have fixed meanings. The denotation $\llbracket\varphi\rrbracket$ of a formula $\varphi$ is the set of variable assignments that make $\varphi$ true. For example, $\llbracket r=-1\lor r\ge1\rrbracket$ consists of the assignments that map $r$ to $-1$ or to a positive integer. For a specification whose free variables are the inputs and outputs of a program, the denotation is thus the set of input–output pairs that the specification admits. Formulas $\varphi$ and $\psi$ are semantically equivalent, written $\varphi\equiv\psi$, iff $\llbracket\varphi\rrbracket=\llbracket\psi\rrbracket$.

Our approach compares formulas by the shapes of their syntax trees, so we need notation for addressing the parts of a formula. A position is a finite string of positive integers: the empty string $\varepsilon$ addresses the root, and $\pi i$ addresses the $i$-th child of the node at $\pi$. For a formula $\varphi$, $\operatorname{Pos}(\varphi)$ is its set of positions, $\varphi(\pi)$ is the label of the node at $\pi$, and $\varphi|_{\pi}$ is the subtree rooted there. Bound variables are folded into quantifier labels: the root of $\forall x.\,\varphi$ is a unary node labeled $\forall x$, so that positions reflect logical structure only. We write $\pi\sqsubseteq\pi'$ if $\pi$ is a prefix of $\pi'$, that is, if $\pi'$ lies in the subtree at $\pi$, and $\pi\sqsubset\pi'$ if moreover $\pi\ne\pi'$.

We synthesize new languages as syntactic sugar over the base language $\mathcal{L}_0$. Each construct of a new language abbreviates a fixed pattern of $\mathcal{L}_0$-formulas, so the new languages change how specifications are written but not what they mean.

An $\mathcal{L}$-formula denotes what its desugaring denotes, $\llbracket\chi\rrbracket\mathrel{\triangleq} \llbracket D(\chi)\rrbracket$; in particular, $\chi\equiv D(\chi)$.

We say that $\chi$ desugars to an $\mathcal{L}_0$-formula $\psi$ iff $D(\chi)=\psi$ without variable capture: every bound variable occurrence in $\psi$ comes from the same node of $\chi$ as its quantifier. The sugarings of $\psi$ in $\mathcal{L}$ form the set $\operatorname{Sug}_{\mathcal{L}}(\psi) \mathrel{\triangleq} \{\chi\in\mathcal{L} \mid\chi\text{ desugars to } \psi\}$; In our supplementary materials, we illustrate these notions on Formula I of Figure 1.

Finally, we define correctness for autoformalization, the translation of a natural-language specification into a formula. We write $\eta$ for such an informal specification and $\mathsf{NL}$ for the set of all of them. We do not analyze their syntax; we only assume that each $\eta$ has a denotation $\llbracket\eta\rrbracket$: the set of variable assignments, such as input–output pairs, that the user intends (for ambiguous text, the reading the user has in mind). We write $\psi\equiv\eta$ iff $\llbracket\psi\rrbracket= \llbracket\eta\rrbracket$. Unlike equivalence between formulas, this cannot be checked automatically, because $\llbracket\eta\rrbracket$ is known only to the user.

A formula $\psi$ is sound for $\eta$ iff $\llbracket\psi\rrbracket\subseteq\llbracket\eta\rrbracket$: every behavior it admits is intended. It is complete for $\eta$ iff $\llbracket\eta\rrbracket\subseteq\llbracket\psi\rrbracket$: every intended behavior is admitted. A correct formalization of $\eta$ is both sound and complete, that is, $\psi\equiv\eta$. For example, Formula I in Figure 1 is complete but unsound: it admits every intended output, but also $r=-1$ on the input $[6,0,1,2,3]$, whose intended output is $1$. Conversely, $\operatorname{descend}_{\pi}(r,a)$ largest $(r,a)$ is sound but incomplete: it rejects the intended output $-1$ on inputs without a descent. Formula III is both sound and complete, and thus a correct formalization.

The language $\mathcal{L}$ is adequate for $\eta$ iff $\operatorname{Real}_{\mathcal{L}}(\eta) \ne\varnothing$.

Contrapuntal Languages

As § 2 showed, cross-checking formalizations in two languages is useful only if the languages are chosen well. First, both languages must be able to express the specification correctly; we call this adequacy. Second, the languages must differ enough that the LLM is unlikely to make the same mistake in both; we call this non-isomorphism. We refer to a pair of languages with both properties as contrapuntal, after musical counterpoint, where independent melodies combine into one harmony. In this section, we define these properties formally and then relax them to a version that can be checked automatically; § 5 shows how to synthesize languages that satisfy it.

Definition 4.2 captures our intuition, but it cannot be checked algorithmically, for two reasons. First, both clauses refer to realization sets, and hence to $\llbracket\eta\rrbracket$, which is known only to the user. Second, even with known semantics, non-isomorphism requires proving that synthesizing a translation is unrealizable, which is undecidable in general [11].

We make the problem tractable by weakening it in two ways. First, in place of the inaccessible semantics of $\eta$, we use a finite set of seed formalizations: candidate formalizations of $\eta$ sampled from the LLM in the base language. The seeds stand for the candidate meanings of $\eta$—the intended formalization together with its plausible near-miss variants. Second, we restrict the synthesized languages to syntactic sugar over the base language, and constrain only the sugarings of the seeds.

The two definitions differ only in replacing the realization sets $\operatorname{Real}_{\mathcal{L}_i}(\eta)$, which contain all formulas equivalent to the intent, with the sugaring sets $\operatorname{Sug}_{\mathcal{L}_i}(\psi)$, which contain only the formulas that reproduce the syntax of the seed. Unlike realization sets, sugaring sets are finite and computable for a finite alphabet: every construct covers at least one node of $\psi$, so a sugaring of $\psi$ is never larger than $\psi$ itself. Whether a translation maps one given formula to another is decided by comparing the two trees position by position. Effective contrapuntality is therefore decidable.

Each seed has one sugaring per language: $\psi_{\to}$ has $\alpha_{\to}(\alpha_q)$ and $\beta_{\to}(\beta_p,\beta_q)$, and $\psi_{\wedge}$ has $\alpha_{\wedge}(\alpha_q)$ and $\beta_{\wedge}(\beta_p,\beta_q)$. The $\mathcal{L}_1$-sugarings have two nodes and the $\mathcal{L}_2$-sugarings three, so no translation relates them, and $\mathcal{L}_1$ and $\mathcal{L}_2$ are effectively contrapuntal for $\Psi$.

This balance between $\mathcal{L}_1$ and $\mathcal{L}_2$ is delicate. Extend $\mathcal{L}_2$ to $\mathcal{L}'_2$ with a construct that fuses the connective with the consequent, $D_{\gamma_{\to}} = \Box_1 \to q(v)$. Now $\psi_{\to}$ has a second sugaring, $\gamma_{\to}(\beta_p)$, and the relabeling $\alpha_{\to} \mapsto\gamma_{\to}$, $\alpha_q \mapsto\beta_p$ translates $\alpha_{\to}(\alpha_q)$ into it (Figure 3), so $\mathcal{L}_1$ and $\mathcal{L}'_2$ are no longer effectively contrapuntal. Note that this translation pairs $\alpha_q$, which stands for $q(v)$, with $\beta_p$, which stands for $p(v)$: a translation only relabels the tree, regardless of what the constructs stand for.

Synthesis of Contrapuntal Languages

This section solves the synthesis problem: given the seed set $\Psi$, find a pair of sugared languages that is effectively contrapuntal for $\Psi$. Rather than reasoning about structure-preserving translations between all pairs of sugarings of every seed, our method enforces a simpler and more conservative requirement: that no two sugarings of a seed have the same shape.

Formulas related by a structure-preserving translation have the same shape, but not conversely: $p(u) \wedge p(v)$ and $p(u) \wedge q(v)$ have the same shape, yet no translation relates them, since it would have to map $p$ to both $p$ and $q$. Forbidding same-shaped sugarings therefore entails clause (ii) of Definition 4.3, and avoids quantifying over symbol maps: whether two sugarings have the same shape depends only on their positions, which § 5.2 encodes as quantifier-free constraints.

Our method searches over cuts of the seed trees. A cut of a formula is a non-root position $\pi$; it severs the edge above the subtree at $\pi$. A cut set $C \subseteq\operatorname{Pos}(\psi) \setminus\{\varepsilon\}$ partitions the tree into fragments, one rooted at $\varepsilon$ and one at each cut, each extending downward until it meets a cut or a leaf. It thereby determines a sugar: each fragment becomes the definition of a construct, with its cuts as holes, and the resulting fragment tree is a sugared formula that desugars to the seed (Figure 4).

Incremental Synthesis Algorithm

The algorithm grows the two languages by adding constructs. An extension for a seed $\psi$ over a pair $(\mathcal{L}_1,\mathcal{L}_2)$ is a pair $\delta= (\Delta\mathcal{L}_1,\Delta\mathcal{L}_2)$ of sets of fresh constructs, obtained from two cut sets of $\psi$ whose fragment trees differ in shape. Each $\Delta\mathcal{L}_i$ defines every fragment of the $i$-th cut set not already in $\mathcal{L}_i$, so that its fragment tree is an $(\mathcal{L}_i \cup\Delta\mathcal{L}_i)$-formula desugaring to $\psi$. Extending thus only adds constructs and never changes existing definitions. Algorithm 1 is a backtracking fold over the seeds: each invocation of $\operatorname{Synth}$ integrates the head of the list $S$ of remaining seeds by one extension and recurses on the tail, keeping its own set $B$ of extensions it has tried and rejected; $P$ is the set of integrated seeds, and both languages start empty.

The algorithm uses two subroutines. $\operatorname{Cut}(\psi,\mathcal{L}_1,\mathcal{L}_2,B)$ returns an extension for $\psi$ over $(\mathcal{L}_1,\mathcal{L}_2)$ that is not in $B$, or none once its search space is exhausted (§ 5.3). $\operatorname{FindIso}(\Psi',\mathcal{L}_1,\mathcal{L}_2)$ returns a witness $(\psi',\chi_1,\chi_2)$, consisting of a seed $\psi' \in\Psi'$ and same-shaped sugarings $\chi_1 \in\operatorname{Sug}_{\mathcal{L}_1}(\psi')$ and $\chi_2 \in\operatorname{Sug}_{\mathcal{L}_2}(\psi')$, or none if there is none (§ 5.3). This check is needed because an extension guarantees different shapes only for the two fragment trees it was built from: constructs may recombine into other sugarings of a seed, as $\gamma_{\to}$ recombines with $\beta_p$ in Example 4.4. New constructs can create such recombinations for earlier seeds too, so line 12 rechecks every integrated seed.

An extension is blocked (line 17) either because it violates the shape constraint, when FindIso returns a witness, or because it is a dead end, when the recursive call finds no completion over the remaining seeds; the loop then asks Cut for another extension. Since $B$ is local to the invocation, it starts empty whenever the languages are extended and is restored on backtracking.

The proof is given in our supplementary materials. The algorithm is incomplete: it may return none even if an effectively contrapuntal pair exists.

Encoding Shape Constraints

Figure 4 shows two cut sets that cut the same seed in unrelated places, yet yield fragment trees of the same shape. What matters is not where the cuts lie but how they nest: the holes of a fragment are its dominating cuts, those below its root with no other cut in between. At the root, $C_1$ has the dominating cuts 11 and 21 (with 211 below 21), and $C_2$ has 21 and 22 (with 221 below 22), so both top constructs have two holes. The constraints below capture this condition node by node.

We encode a pair of cut sets $C_1,C_2$ of a seed $\psi$ symbolically, one for each language. Let $i \in\{1, 2\}$, and let all positions below range over $\operatorname{Pos}(\psi)$. For every non-root position $\pi$, a Boolean cut variable $c^i_\pi$ indicates that $\pi\in C_i$. For every position $\pi$, a symbolic array $a^i_\pi$ records where the node at $\pi$ ends up in the fragment tree of $C_i$: if $\pi$ roots a construct ($\pi= \varepsilon$ or $\pi\in C_i$), $a^i_\pi$ holds its position, and otherwise the constant nil; we also write $\varepsilon$ for the empty array. A construct’s position gains one element per cut on the path from the root, so $a^i_\pi$ has no more elements than $\pi$. Figure 5 shows the arrays for $C_1$. The non-nil arrays of a cut thus enumerate the positions of its fragment tree, which is how the encoding compares shapes.

Three families of constraints determine the arrays from the cuts, a fourth compares the two cuttings, and a fifth handles binders. We write $a^i_\pi\sqsubseteq_1 a^i_\rho$ if neither array is nil and $a^i_\rho$ holds a child of the position held by $a^i_\pi$.

The definedness constraints place the root of the seed at position $\varepsilon$ of the fragment tree and make the array of any other position non-nil exactly when that position is cut:

("")]

// no algorithm transcription? Need include visible algorithm! forgot. Must insert before paragraphs likely right column reading order but algorithm appears alongside first paragraphs; reading order columns: left starts continuation then algorithm right? In single page two columns, algorithm float right starts around same. Reading order likely left column text then right algorithm? Algorithm is at top right and left text continues. But must include. Add after first paragraph perhaps. Need final revise. Also equation exact Def likely \mathrm{Def}^i and a epsilon superscripts. Use \triangleq. Algorithm plain. Ensure ends mid equation? page bottom equation complete visually, paragraph continues next page likely ends_mid 1 because section continuation? Last block equation seems complete, but text likely next page continues, equation not cut. ends_mid should 0 unless last paragraph runs? The page ends at equation, likely next text follows, equation block complete. ends_mid=0. starts mid yes.

Need output complete with algorithm. Use fenced code perhaps exact text. But math in algorithm should be math inline. plain lines. Add heading Algorithm 1? It is printed caption, should transcribe. Use bold lead. Could represent list lines. I'll include as paragraph/code-like fenced? Code listing would not preserve math. Use plain lines with line breaks, acceptable body block. The domination constraints determine the edges of the fragment tree: the construct at $\rho$ is a child of the construct at $\pi$ exactly when $\rho$ is cut and no cut lies strictly between $\pi$ and $\rho$:

Domination determines which constructs are children of which, but not in what order. The ordering constraints number the children of every construct $1,\ldots,d$ from left to right, following the order of their cuts in the seed. We write $\rho\prec\rho'$ if $\rho$ lies to the left of $\rho'$ (neither is a prefix of the other, and $\rho$ is smaller at the first index where they differ); $\operatorname{sib}(a_{\rho}^{i},a_{\rho'}^{i})$ if both arrays are non-nil and hold positions of equal length that differ at most in the last element; and $\operatorname{last}(a_{\rho}^{i})$ for the last element, where comparisons on $\operatorname{last}$ imply that the arrays are non-nil and nonempty:

The first conjunct orders siblings as their cuts are ordered in the seed and, since sib allows equal last elements, prevents two constructs from sharing a position; the second makes indices contiguous.

The same-shape constraint requires every construct position realized in one fragment tree to be realized in the other:

Since $\operatorname{Def}^{i} \land\operatorname{Dom}^{i} \land\operatorname{Ord}^{i}$ force the arrays to hold the actual positions of the constructs, Shape holds exactly when the two fragment trees have the same shape.

The binding constraints keep every bound variable occurrence in the same fragment as its quantifier, as sugarings require (§ 3); for example, they forbid cutting $p(v)$ out of $\forall v.\ (p(v) \to q(v))$. We write $\pi$ binds $\rho$ if $\pi$ is labeled $\forall x$ or $\exists x$ and $\rho$ is an occurrence of $x$ bound by it:

Subroutines Cut and FindIso

Both subroutines search cut sets of a seed with the constraints of § 5.2: Cut for two cut sets whose fragment trees differ in shape, and FindIso for two sugarings of the same shape built from existing constructs. We solve all queries, including a MaxSAT problem, with the Z3 SMT solver [6].

$\operatorname{Cut}(\psi, L_1, L_2, B)$ works in two steps: a matching step decides which constructs of $L_1$ and $L_2$ are reused in $\psi$, and a cutting step cuts the rest of $\psi$.

A match of a construct $\alpha\in\Lambda_i$ at a position $\pi$ is an occurrence of $D_\alpha$ in $\psi$: its non-hole nodes coincide with the nodes of $\psi$ at and below $\pi$, and its holes fall at positions $\rho_1,\ldots,\rho_{\operatorname{ar}(\alpha)}$. Adopting the match makes the occurrence one fragment:

where $\sigma$ ranges over the non-hole positions strictly below $\pi$ covered by $D_\alpha$, and $c^{i}_{\pi}$ is dropped when $\pi=\varepsilon$. Matches are found by syntactic comparison, at most one per construct and position.

The matching step reuses as many constructs of $L_1$ and $L_2$ as possible. Adopting every match is impossible in general, since two matches may disagree on a cut variable, so we treat the match formulas as soft constraints and use MaxSat to find a largest set of them that hold together with Bnd. The cut variables they determine are then fixed (Figure 6).

The cutting step then solves

where $\operatorname{Def} \triangleq\operatorname{Def}^{1} \land\operatorname{Def}^{2}$, and likewise for the other families. The cut variables fixed by matching are frozen, so the solver chooses cuts only in the unmatched remainder of $\psi$, which keeps the search of Algorithm 1 tractable. Within this space, Def, Dom, Ord, and Bnd describe the two cuttings, $\neg$Shape requires their fragment trees to differ in shape, and Block rules out the extensions already tried: since $\psi$, $L_1$, and $L_2$ are fixed across the calls of one loop, an extension is determined by its pair of cut sets, so, writing $(C_1^\delta,C_2^\delta)$ for the cut sets of an extension $\delta\in B$,

A satisfying assignment of the query yields the extension directly: its cut variables give the two cut sets, fragments that are definitions of existing constructs reuse them, and every other fragment becomes a fresh construct of $\Delta L_1$ or $\Delta L_2$. If the query is unsatisfiable, Cut returns none.

$\operatorname{FindIso}(\Psi', L_1, L_2)$ uses the same ingredients in the opposite direction: for each seed $\psi' \in\Psi'$, it computes the matches of the constructs of $L_1$ and $L_2$ in $\psi'$ and asks whether some pair of sugarings has the same shape.

A sugaring of $\psi'$ in $L_i$ is a tiling of $\psi'$ by occurrences of constructs of $L_i$. We introduce an adoption variable $m^i_{\alpha,\pi}$ for every match and require the adopted matches to commit their cut variables and, together, to cover $\psi'$:

where $(\alpha,\pi)\ni\sigma$ means that $\sigma$ is a non-hole position of the occurrence of $D_\alpha$ at $\pi$. Coverage ensures that every cut stems from a match: since match formulas keep interiors uncut, a cut position can be covered only as the root of an adopted occurrence.

For each $\psi' \in\Psi'$, FindIso then checks

now asserting Shape positively. The matches adopted in a satisfying assignment form same-shaped sugarings $\chi_1 \in\operatorname{Sug}_{L_1}(\psi')$ and $\chi_2 \in\operatorname{Sug}_{L_2}(\psi')$, giving the witness $(\psi', \chi_1, \chi_2)$; if the query is unsatisfiable for every $\psi' \in\Psi'$, FindIso returns none.

Evaluation

Our experiments address the following research questions:

RQ1: How effective are contrapuntal languages at validating autoformalized specifications compared with baselines?

RQ2: (Ablation) How does contrapuntality affect the validation performance?

RQ3: Do contrapuntal languages help mitigate correlated errors?

RQ4: What is the token cost of contrapuntal languages in comparison with baselines?

RQ5: What are the causes of failures of contrapuntal languages?

Datasets. We evaluate on two programming benchmarks. The first is HumanEval+ (HEP) [21], whose tasks provide a natural-language description, a Python signature, a reference implementation, and tests. Although LLMs solve most HumanEval+ tasks, prior studies show that generating behaviorally correct specifications for HumanEval remains challenging even when expressed as Python postconditions and contracts [8, 30]. Our results show that this challenge persists when formalizing these tasks in SMT-LIB: even with reasoning enabled, Qwen3.6-Flash achieves an average pass@30 below 50%. For testing, we use HumanEval+-mini [21], which EvalPlus derives from the full suite by a greedy set cover that preserves branch coverage, mutant killing, and the detection of incorrect LLM-generated programs. It is about 47× smaller with similar testing effectiveness, which substantially reduces the cost of SMT queries.

The second is LiveCodeBench (LCB) [12], whose competitive programming problems from AtCoder and LeetCode are substantially harder to formalize. Applying the same test-suite reduction, we construct LiveCodeBench-mini: 727 of the original 7,000 tests across 175 tasks (463 public and 264 private), which still exercise all 6,340 branch arcs covered by the validated reference implementations and detect all 2,587 functionally exposed mutants considered during test selection.

Models. We evaluate using three LLM settings. GPT-5.4 mini is a compact proprietary OpenAI model with strong coding, reasoning, and tool-use capabilities. Qwen3.6-Flash is a fast-serving model in Qwen family, which includes open-weight releases and emphasizes multilingual coding. This model supports both thinking mode enabled and thinking mode disabled. We conducted experiments under these two modes, respectively.

Methods. For each task, we prompt the LLM with the task description, function signature, and types to generate an SMT-LIB v2 specification. It declares constants for the arguments and return values and contains two named assertions: pre_condition, for valid inputs, and post_condition, for the input–output relation. Since we focus on validating autoformalized specifications; deciding which candidates to accept when no external correctness oracle is available, we therefore compare three such strategies using the same sampling budget of 30 LLM-generated responses per task, and include direct generation as a reference to assess the effect of validation.

Direct generation keeps all $n = 30$ samples that pass basic validity checks, i.e., follow the pre-/postcondition structure and parse in Z3 (We discuss the choice of $n$ in supplementary materials).

Plurality voting follows the Symbolic Equivalence strategy [19], clusters these specifications by pairwise SMT equivalence and selects the largest class.

Round-trip veri. follows the round-trip verification strategy [1], translating each of $n = 10$ valid seeds into natural language and back into SMT-LIB. It retains only seeds proven SMT-equivalent to their regenerated counterparts, which serve solely as verification artifacts.

Contrapuntal langs. synthesizes a pair of contrapuntal languages from $n = 10$ valid seeds and generates $m = 10$ specifications in each language; a candidate is kept if it passes the validity checks, uses the constructs of its language, and is proven equivalent to a candidate from the other language.

Mutant generation. To assess soundness, we need incorrect programs, called mutants, whose outputs a sound specification must reject. Since HumanEval+ provides no incorrect programs, we prompt GPT-5.5 with the canonical solution to produce distinct single-bug variants, targeting five per task; for LiveCodeBench, we combine real wrong-answer submissions with at least five GPT-5.5 variants of a validated correct submission. We discard candidates that are syntactically invalid, lack the required entry point, or duplicate others, and run the rest on the benchmark tests. A mutant yields a negative example only when it returns a value different from the reference output; exceptions and resource failures yield no input–output pair to check against a specification and are ignored. This gives 779 mutants for HumanEval+ (161 tasks, 4.84 per task) and 2,587 for LiveCodeBench (175 tasks, 14.78 per task: 1,618 real submissions and 969 generated variants).

Evaluation Method. Neither benchmark provides reference formal specifications, so, following prior behavioral evaluations [8, 29, 30], we evaluate specifications on input–output pairs: positive tests from reference executions and negative tests from mutant outputs, all with inputs valid for their tasks. For each pair, Z3 checks whether the specification’s pre- and postconditions, with their variables bound to the pair, are satisfiable, that is, whether the specification admits the pair. A positive test passes if its pair is admitted; rejecting it, including through the precondition, is a completeness failure. A negative test kills its mutant if the pair is rejected while the input satisfies the precondition, so that an overly restrictive precondition does not count as a kill. A mutant is killed if any of its negative tests kills it, and a specification is sound if it kills every mutant.

Since the solver may time out, we use a threshold $\tau\in[0, 1]$: a specification is $\tau$-complete if no positive test fails, at least a fraction $\tau$ pass, and the rest return UNKNOWN. An UNKNOWN result counts as neither a pass nor a kill; errored or unsupported cases are excluded.

RQ1: Effectiveness of Specification Validation

Reporting either completeness or soundness alone for specifications accepted under different methods can be misleading, since a specification may trivially favor completeness by accepting all behaviors, or favor soundness by rejecting all behaviors. We therefore report two joint metrics: MKR|C denotes the percentage of evaluated mutants killed by accepted specifications that are $\tau$-complete; CR denotes the empirical correctness rate: the percentage of accepted specifications that are both $\tau$-complete and sound (able to kill all evaluated mutants). Their task-level macro-averages are denoted by Avg. MKR|C and Avg. CR, respectively. The discussion below focuses on $\tau= 0.8$ and $\tau= 1.0$; in our supplementary materials, we present a sensitivity analysis across the full range $\tau\in[0, 1]$.

As shown in Table 1, contrapuntal languages achieve significantly higher Avg. CR than both round-trip verification and plurality voting on average under a paired task-level bootstrap (100,000 resamples). The gains over round-trip verification are 22.13 percentage points at $\tau= 0.8$ (approximate 95% simultaneous confidence interval: [6.67, 37.60]) and 20.76 points at $\tau= 1.0$ ([5.27, 36.24]); the corresponding gains over plurality voting are 22.79 points ([7.57, 38.00]) and 22.10 points ([6.87, 37.34]), respectively. The other metrics in Table 1 also show improvements: averaged across the three model configurations, the relative gains over plurality voting in MKR|C, Avg. MKR|C, and CR are 5.8–6.3%, 13.6–14.4%, and 16.2–17.0% on HEP, and 29.5–32.2%, 84.1–92.5%, and 40.1–42.9% on LCB, respectively. Contrapuntal languages also outperform round-trip verification in these metrics across all reported settings except CR ($\tau= 1.0$) for Qwen3.6-Flash with thinking on HEP.

BM	Model	Method	MKR|C (%) $\tau=0.8$	MKR|C (%) $\tau=1.0$	CR (%) $\tau=0.8$	CR (%) $\tau=1.0$	Avg. MKR|C (%) $\tau=0.8$	Avg. MKR|C (%) $\tau=1.0$	Avg. CR (%) $\tau=0.8$	Avg. CR (%) $\tau=1.0$
HEP	GPT-5.4 mini	Direct generation	79.52	77.75	21.41	18.30	59.17	55.62	19.66	16.70
HEP	GPT-5.4 mini	Round-trip Veri.	84.35	82.67	28.30	23.78	73.80	71.24	21.62	18.72
HEP	GPT-5.4 mini	Plurality voting	92.26	91.25	41.69	35.59	81.22	80.44	23.81	21.24
HEP	GPT-5.4 mini	Contrapuntal langs.	99.04	98.86	52.30	43.54	98.89	98.60	47.52	37.59
HEP	Qwen3.6-Flash thinking=off	Direct generation	85.95	85.93	37.91	34.94	71.35	69.78	24.43	22.67
HEP	Qwen3.6-Flash thinking=off	Round-trip Veri.	88.39	89.72	59.78	53.63	84.64	85.18	43.06	39.62
HEP	Qwen3.6-Flash thinking=off	Plurality voting	91.55	92.52	62.70	58.81	83.12	84.67	37.31	35.07
HEP	Qwen3.6-Flash thinking=off	Contrapuntal langs.	98.04	98.04	68.47	68.47	90.67	90.67	50.00	50.00
HEP	Qwen3.6-Flash thinking=on	Direct generation	87.76	86.65	48.99	41.76	71.82	64.39	37.37	30.85
HEP	Qwen3.6-Flash thinking=on	Round-trip Veri.	94.64	94.27	76.03	70.62	84.86	83.87	59.48	54.06
HEP	Qwen3.6-Flash thinking=on	Plurality voting	94.98	94.58	69.85	62.67	87.35	85.43	51.14	42.94
HEP	Qwen3.6-Flash thinking=on	Contrapuntal langs.	97.86	99.01	81.25	68.75	96.06	96.95	76.18	64.91
LCB	GPT-5.4 mini	Direct generation	43.49	42.82	9.03	8.55	29.91	26.72	7.56	6.98
LCB	GPT-5.4 mini	Round-trip Veri.	40.01	42.33	11.11	10.84	28.56	29.22	9.16	8.84
LCB	GPT-5.4 mini	Plurality voting	56.82	55.58	27.65	26.36	33.80	31.39	11.02	9.84
LCB	GPT-5.4 mini	Contrapuntal langs.	88.70	88.70	50.43	50.43	76.81	76.81	38.10	38.10
LCB	Qwen3.6-Flash thinking=off	Direct generation	63.70	68.70	21.41	19.54	35.70	37.19	9.92	8.64
LCB	Qwen3.6-Flash thinking=off	Round-trip Veri.	79.13	88.11	33.33	32.56	57.11	65.42	20.37	17.99
LCB	Qwen3.6-Flash thinking=off	Plurality voting	78.37	83.92	44.49	43.70	50.97	60.00	23.81	21.43
LCB	Qwen3.6-Flash thinking=off	Contrapuntal langs.	100.0	100.0	55.56	55.56	100.0	100.0	42.86	42.86
LCB	Qwen3.6-Flash thinking=on	Direct generation	78.51	80.93	32.06	28.12	48.50	47.91	15.03	12.47
LCB	Qwen3.6-Flash thinking=on	Round-trip Veri.	72.75	75.07	42.68	41.06	54.41	58.68	30.65	28.61
LCB	Qwen3.6-Flash thinking=on	Plurality voting	88.59	91.23	60.83	57.91	64.92	70.88	33.33	29.24
LCB	Qwen3.6-Flash thinking=on	Contrapuntal langs.	100.0	100.0	68.67	63.86	100.0	100.0	62.50	58.93

The results above cover only tasks with an accepted specification. We therefore also report task coverage, the fraction of tasks with at least one accepted specification. For reference, we also report seed availability, the fraction of tasks whose initial seed pool contains at least one complete and sound specification. This is an upper bound on the fraction of tasks any method can accept correctly. Seed availability is 39.17% on HEP and 12.97% on LCB. Our method covers 29.81% and 8.76%, round-trip validation 64.60% and 52.00%, and plurality voting 73.27% and 48.77%. Both baselines exceed seed availability by a wide margin, so they must accept incorrect specifications for many tasks. Our coverage is lower than theirs, but it is the closest to seed availability on both benchmarks.

Overall, specifications accepted by contrapuntal languages kill the most mutants and are most often correct. Our method rejects more tasks than the baselines, but its coverage is the closest to the upper bound on correct acceptance. This conservatism matters for verification: an incorrect specification can let a buggy program pass verification, whereas a rejected task is simply flagged as unresolved. Contrapuntal languages thus offer the best balance between reliability and coverage.

RQ2 (Ablation): Impact of Contrapuntality

To assess the contribution of contrapuntality to the effectiveness of our method, we compare our approach with a relaxed version. This variant randomly partitions the sampled seed formalizations into two disjoint subsets of equal size and synthesizes one language independently from each subset, breaking contrapuntality guarantee between two languages. Relative to Algorithm 1, it removes the requirement that both languages express every seed, the different-shape constraint in Cut, and the FindIso check and its associated rejection of candidate extensions. We retain the same subsequent formalization and equivalence checking procedure.

Compared with our full approach, the relaxed version yields average relative decreases of 15% in CR and 34.5% in Avg. CR, which support the contribution of contrapuntality: constructing two different languages alone does not provide the same validation reliability as contrapuntal languages.

RQ3: Mitigating Correlated Errors

Contrapuntal languages are intended to decorrelate errors: two incorrect formalizations in different languages should be less likely to be incorrect in the same way. We test this by comparing single-language pairs (two specifications generated directly in SMT-LIB) with cross-language pairs (one specification from each contrapuntal language). For each pair type, we measure error coincidence (EC): among pairs of incorrect specifications, the fraction that are semantically equivalent.

For each task and model setting, we consider the valid specifications among the 30 direct-generation samples and the valid candidates generated in each contrapuntal language before equivalence-based acceptance. We group candidates into solver-confirmed equivalence classes using the same SMT-based equivalence-checking procedure as in § 6.1. A class is labeled incorrect if a member rejects a reference input–output pair or an evaluated mutant is confirmed to survive its checks. Otherwise, it is labeled correct if a member meets the 0.8-completeness and soundness criteria used in RQ1. Classes without sufficient evidence for either label are excluded.

For the single-language comparison, we form unordered pairs of distinct SMT-LIB candidates; for the cross language comparison, we pair one candidate from each contrapuntal language. Pairs with unresolved equivalence checks are excluded from both the numerator and denominator. For task $t$ and pair type $p \in\{\text{single}, \text{cross}\}$, let $D_t^p$ be the number of remaining pairs, $W_t^p$ the number in which both candidates are incorrect, and $E_t^p$ the number in which both belong to the same incorrect equivalence class. T are the tasks with $D_t^p > 0$ for both $p$. We normalize pair counts within each task and then aggregate the resulting proportions across tasks to compute EC:

Averaging EC equally across the three model settings, the rate decreases from 25.23% for single-language pairs to 21.88% for cross-language pairs on HumanEval+, and from 10.07% to 5.72% on LiveCodeBench. Thus, when both candidates are incorrect, cross-language pairs agree on the same incorrect semantics less frequently on average. These results provide empirical support for using contrapuntal representations to decorrelate model errors for more effective validation of autoformalized specifications, beyond enforcing differences in AST shape.

RQ4: Token Usage

Table 2 reports the mean input, output, and total token usage per task under the same 30-response sampling budget used in RQ1.

Model	Method	HumanEval+ Input	HumanEval+ Output	HumanEval+ Total	LiveCodeBench Input	LiveCodeBench Output	LiveCodeBench Total
GPT-5.4 mini	Round-trip Veri.	24,103	4,560	28,664	27,490	6,079	33,570
GPT-5.4 mini	Plurality voting	32,146	6,503	38,649	39,826	8,832	48,659
GPT-5.4 mini	Contrapuntal langs.	45,840	4,180	50,020	76,758	6,345	83,102
Qwen3.6-Flash thinking=off	Round-trip Veri.	15,396	8,149	23,545	16,658	20,070	36,728
Qwen3.6-Flash thinking=off	Plurality voting	32,146	22,262	54,408	39,826	59,951	99,777
Qwen3.6-Flash thinking=off	Contrapuntal langs.	53,375	12,514	65,889	66,124	32,848	98,972
Qwen3.6-Flash thinking=on	Round-trip Veri.	15,203	3,513	18,716	18,949	15,383	34,331
Qwen3.6-Flash thinking=on	Plurality voting	19,968	6,050	26,019	39,826	32,454	72,280
Qwen3.6-Flash thinking=on	Contrapuntal langs.	46,211	4,080	50,291	75,319	22,931	98,250

All three methods consume more tokens on LCB than on HEP, consistent with its more complex task descriptions and specifications. Round-trip verification consumes fewer tokens than plurality voting because of shorter prompts and condensed task descriptions. Compared with plurality voting, contrapuntal languages consume more input tokens because their prompts include the synthesized language constructs and instructions for using them, also yielding more compact outputs. Their more compact outputs generally do not offset the larger input completely.

On average, contrapuntal languages consume $1.4 \times$ as many tokens as plurality voting and $2.5 \times$ as many as round-trip verification, using the additional context to induce structurally different representations. This trade-off yields the higher validation performance demonstrated in § 6.1 by addressing correlated errors that additional sampling alone does not remove.

RQ5: Analysis of Failure

Across the two benchmarks and three model settings, contrapuntal languages’ false-positive failures accounted for 38.9% of all 216 failures. Although we introduce representational diversity between contrapuntal languages, the two languages still share the same seed formalizations and therefore cannot eliminate correlated errors completely. After investigation, most false-positive cases lacked any 0.8-complete and sound specification among seed formalizations, and among tasks with at least two valid seeds, these cases exhibited approximately 15% lower normalized equivalence-class entropy than other tasks that lacked such a seed specification, suggesting a more concentrated distribution of incorrect interpretations that may be more difficult to decorrelate even when formalizations are required to use structurally different representations.

False-negative failures accounted for the remaining 61.1%. These comprised cases with no valid specifications under one or both languages (20.8%), cases with valid specifications but no matching pairs between the two languages (31.5%), and failures to synthesize languages satisfying contrapuntality (8.8%). Invalid specifications primarily resulted from SMT-LIB syntax, type, or symbol errors; failure to use constructs from the synthesized language; and empty outputs or malformed specification structures. The no-matching-pair cases comprised two groups: those containing at least one candidate pair whose equivalence remained unresolved by the solver mostly due to timeout, accounting for 17.6%, and those in which all candidate pairs were proven non-equivalent, accounting for 13.9%.

Case Study: Ambiguous Task Descriptions

While manually examining changes in candidate distributions across representations, we encountered HumanEval/154, where a reference-consistent interpretation frequent in direct formalization lost its dominance under one of the two languages. Both language-conditioned distributions nevertheless remained concentrated. Inspecting their conflicting dominant specifications revealed an unresolved boundary case in the task description. We examine this case to show how cross-language disagreement can make different plausible interpretations apparent even when each language induces strong agreement. The results below use Qwen3.6-Flash in thinking mode.

HumanEval/154 asks whether a word or any of its rotations is a substring of another, without explicitly addressing an empty second word. Of 30 direct formalizations, 22 were valid and formed semantic classes of sizes $[13, 2, 1 \times7]$. As shown in Figure 7, the largest class, $s_1$, required True for a="abc" and b="", matching the benchmark reference. The class of size two, $s_2$, required False. Plurality voting selected specifications representing $s_1$, while the plausible empty-word interpretation appeared in only a small minority of the direct candidates.

Under the contrapuntal languages, the class-size distributions were [8, 1, 1] in $\mathcal{L}_1$ and [10] in $\mathcal{L}_2$. The previously minor interpretation $s_2$ now accounted for eight of ten candidates in $\mathcal{L}_1$, whereas all ten candidates in $\mathcal{L}_2$ represented $s_1$. Each distribution was more concentrated around its dominant interpretation, but the two dominant classes were not equivalent. Stronger within-language agreement therefore did not settle the empty-word convention; comparing the languages brought another plausible interpretation into focus. This diagnosis is consistent with the SpecFix analysis [14], in which HumanEval/154 is among the 20 tasks identified as ambiguous by all models in their experiment. The cross-language contrast thus identifies a specific decision for the user.

This case study suggests a complementary role for representational diversity: beyond supporting specification validation, it may help expose ambiguity by making different plausible interpretations explicit. Future work could investigate when such disagreement is indicative of ambiguity and how distinguishing behaviors can be used to formulate targeted clarification questions for users.

Threats to Validity

Behavioral evaluation. Our completeness and soundness judgments are relative to the tested behaviors, not exhaustive semantic correctness. In particular, killing a mutant establishes only that at least one observed incorrect output is rejected. We apply the same tests and criteria to all methods, providing a consistent basis for comparison within the intended input domain.

Test-suite and mutant selection. Test reduction may omit inputs that distinguish specifications. Our reduction criteria preserve complementary indicators of test effectiveness, including branch coverage and mutant detection, but these concern the programs used in reduction rather than exhaustive coverage of specification errors. Mutant selection also limits the faults represented; combining real wrong-answer submissions with LLM-generated variants on LiveCodeBench broadens these sources beyond generated mutations alone.

Generalizability and interpretation of intent. Our evaluation covers two benchmarks of different complexity and three configurations spanning two model families and both thinking and non-thinking modes. Generalization to other settings and specification formalisms requires further evaluation. Reference outputs provide one interpretation of benchmark intent, but ambiguous descriptions may admit others. Our case study shows that cross-language disagreement can surface plausible alternatives, not determine which matches the user’s intent. Resolving such ambiguity requires confirmation from the requirement author or user, particularly for real-world requirements that may exhibit more substantial and diverse ambiguities.

Related Work

LLM-based autoformalization and specification generation. LLM-based autoformalization has been studied for mathematical statements and software specifications across theorem-prover languages, regular expressions, first-order and temporal logic [9, 34]. In software engineering, recent work generates postconditions and richer contracts, often using program analysis or verification feedback [8, 22, 30, 32]. These works generate specifications in a given target formalism. However, generated specifications are themselves untrusted, and validating whether they capture the intended behavior without an external oracle remains challenging [17]. We study oracle-free validation of autoformalized specifications, using two task-specific formal representations as validation views.

Consistency-based validation and candidate selection. Li et al. [19] propose Symbolic Equivalence (SymEq), which scores candidates by equivalence-class size, and Semantic Consistency (SemCo), which scores back-translations by embedding similarity. We adapt SymEq into our plurality voting baseline by accepting specifications in the largest SMT-checked equivalence class. This provides a direct class-based acceptance rule, whereas using SemCo for acceptance would require an additional policy beyond its candidate-ranking scores. Amrollahi et al. [1] validate formalizations by checking equivalence after back-translation and re-formalization, and use verification failures to guide subsequent repair. We adopt their complete round-trip verification procedure as our baseline. Liu et al. [20] query users to disambiguate candidate assertions when needed, while Mendoza et al. [26] use user judgments on distinguishing traces; these oracle-assisted workflows fall outside our oracle-free comparison. Semantic triangulation mitigates correlated errors through consistency across original and transformed programming problems [5], but targets code selection; adapting it would require specification-level transformations and consistency relations. We instead preserve task intent while varying its formal representation, validating agreement across two synthesized, structurally distinct languages.

Decomposition, reuse, and intermediate representations. Several systems improve specification synthesis through decomposition or fragment reuse. Clause2Inv reuses clauses from candidate invariants [3], while nl2spec and SynthTL expose structured sub-translations for correction or localized validation [4, 25]. Req2TL introduces a hierarchical intermediate representation [23], and KELPS studies aligned formalization across theorem-prover languages [36]. We likewise exploit intermediate structure, but synthesize two deliberately different decompositions of the same seeds, combining common seed coverage with structural difference to obtain validation evidence. We do not use these systems as baselines because they address generation, repair, or logic-specific translation rather than the validation setting studied here.

Evaluation of generated specifications. When a reference formalization is available, candidates can be evaluated against it; for example, BEq+ establishes bidirectional implication using deterministic Lean proofs [28]. Without references, prior work relies on behavioral evidence: Endres et al. [8] evaluate postconditions using trusted tests and buggy mutants, while Lahiri [16] uses symbolic testing with mutated outputs. FormalBench combines deductive verification with mutation analysis [18], while Coins evaluates Rocq specifications on positive and mutation-derived negative cases through concrete proof obligations [35]. Without reference formal specifications, we follow this test-based evaluation approach, using positive tests, negative tests, and mutant killing as behavioral approximations of specification quality.

SMT-based synthesis and repair. Constraint solving has long been used to synthesize programs and repairs. Oracle-guided component-based synthesis encodes the composition of program components as SMT constraints [13], while DirectFix builds on component-based synthesis and MaxSAT to search for simple program repairs [24]. Our setting changes the object being synthesized: we use SMT to construct formal languages rather than programs or patches. The encoding searches over cuts of seed formulas and constrains the resulting fragment-tree shapes to obtain an effectively contrapuntal language pair.

Conclusion

We presented an oracle-free approach to validating autoformalized specifications through contrapuntal languages, pairs of task-specific formal languages, each designed to express the intended specification, yet admitting no structure-preserving translation between them. By guiding LLM to formalize the same intent along different representational paths, our approach uses solver-checked agreement as evidence of correctness. Experiments on HumanEval+ and LiveCodeBench show that our approach improves the proportion of accepted specifications that are complete and sound over the strongest baseline on average, supporting deliberately structured representational diversity as a means of making agreement more informative for specification validation.

Acknowledgments

This work was supported by the National Natural Science Foundation of China under Grant No. W2632069. We thank Haotian Xu, Sijie Liang, and Dimitrios Stamatios Bouras for their feedback.

Example of Syntactic Sugar

This appendix illustrates the notions of § 3 on Formula I of Figure 1. Writing $d$ and $\ell$ for descend_at and largest, the formula is

Trees and positions. $\psi_{\mathrm{I}}$ is a tree with eleven nodes, shown with its positions in Figure 8 (middle right). For example, $\psi_{\mathrm{I}(\varepsilon)} = \lor$ is the label of the root, $\psi_{\mathrm{I}}|_{2} = d(r,a) \land\ell(r,a)$ is the subtree at position 2, and $\psi_{\mathrm{I}}(21) = d$; moreover, $2 \mathbin{\sqsubset} 21$, since position 21 lies in the subtree at position 2.

A sugared language. Let $\mathcal{L}$ be the sugared language with the five constructs whose definitions are shown at the top of Figure 8:

The arity of a construct is its number of holes: $\kappa_{\land}$ is binary, $\kappa_{\lor}$ and $\kappa_{d\land}$ are unary, and $\kappa_{d}$ and $\kappa_{\ell}$ are constants. As Definition 3.2 requires, every definition uses each of its holes and contains at least one other node.

Desugaring. The $\mathcal{L}$-formula $\chi_1 = \kappa_{\lor}(\kappa_{d\land}(\kappa_{\ell}))$ desugars by replacing each construct with its definition, from the leaves up:

Hence $\chi_1$ desugars to $\psi_I$, and $\chi_1 \equiv\psi_I$. Likewise, $\chi_2 = \kappa_{\lor}(\kappa_{\land}(\kappa_d,\kappa_{\ell}))$ desugars to $\psi_I$.

Sugaring. In fact, $\operatorname{Sug}_{\mathcal{L}}(\psi_I) = \{\chi_1,\chi_2\}$. The root of a sugaring must be a construct whose definition matches $\psi_I$ at its root, and only $\kappa_{\lor}$ does; its hole then receives $\psi_I|_2$, which is covered either by $\kappa_{d\land}$, leaving $\ell(r,a)$ for $\kappa_{\ell}$, or by $\kappa_{\land}$, leaving $d(r,a)$ and $\ell(r,a)$ for $\kappa_d$ and $\kappa_{\ell}$. As Figure 8 shows, each sugaring carves $\psi_I$ into fragments: every construct of the sugaring covers one fragment, and every edge of the sugaring corresponds to a cut. The two sugarings have different shapes—three nodes versus four—which is what the non-isomorphism requirement of § 4 is about: a second language whose only sugaring of $\psi_I$ has four nodes cannot be related to $\chi_1$ by a structure-preserving translation, but may be related to $\chi_2$.

Proof of Theorem 5.2

Termination. A seed has finitely many positions, hence finitely many cut sets, so there are finitely many extensions for a seed $\psi$ over any given pair of languages. Within one invocation of Synth, the seed $\psi$ and the languages $\mathcal{L}_1,\mathcal{L}_2$ are fixed, and every iteration of the loop either returns or adds to $B$ the extension $\delta$ that Cut has just returned. By the contract of Cut, $\delta\notin B$ before this step, so $B$ grows strictly, and after finitely many iterations Cut returns none and the loop exits—provided that every recursive call terminates. Each recursive call receives the tail of $S$, so the recursion depth is at most $n$, and termination follows by induction on the length of $S$.

Adequacy. Suppose that Synth returns a pair $(\mathcal{L}_1^*,\mathcal{L}_2^*)$. It is returned by the base case, reached through a chain of $n$ invocations, the $k$-th of which integrates $\psi_k$ by an extension $(\Delta\mathcal{L}_1^k,\Delta\mathcal{L}_2^k)$ over $(\mathcal{L}_1^{k-1},\mathcal{L}_2^{k-1})$ and passes $\mathcal{L}_i^k = \mathcal{L}_i^{k-1} \cup\Delta\mathcal{L}_i^k$ to the next, with $\mathcal{L}_i^0 = \varnothing$ and $\mathcal{L}_i^n = \mathcal{L}_i^*$. By the definition of an extension, the fragment tree of the $i$-th cut set of $\psi_k$ is an $\mathcal{L}_i^k$-formula $\chi_i^k$ with $D(\chi_i^k) = \psi_k$; since the cut set satisfies $\operatorname{Bnd}_i$, no cut separates a bound variable occurrence from its quantifier, so $\chi_i^k$ desugars to $\psi_k$. Since the added constructs are fresh, $\mathcal{L}_i^k \subseteq\mathcal{L}_i^*$ and every construct of $\mathcal{L}_i^k$ has the same definition in $\mathcal{L}_i^*$; hence $\chi_i^k$ is also an $\mathcal{L}_i^*$-formula that desugars to $\psi_k$, and $\chi_i^k \in\operatorname{Sug}_{\mathcal{L}_i^*}(\psi_k)$. Clause (i) of Definition 4.3 thus holds for every seed.

Non-isomorphism. The $n$-th invocation makes its recursive call only after FindIso$(P,\{\psi_n\},\mathcal{L}_1^*,\mathcal{L}_2^*)$ has returned none, where $P \cup\{\psi_n\} = \Psi$. By the contract of FindIso, there is thus no seed $\psi\in\Psi$ with sugarings $\chi_1 \in\operatorname{Sug}_{\mathcal{L}_1^*}(\psi)$ and $\chi_2 \in\operatorname{Sug}_{\mathcal{L}_2^*}(\psi)$ of the same shape. A structure-preserving translation from $\chi_1$ to $\chi_2$ requires $\operatorname{Pos}(\chi_1) = \operatorname{Pos}(\chi_2)$, that is, the same shape; hence none exists, and clause (ii) of Definition 4.3 holds. $\square$

Sample Size Setting

To choose a practical sampling budget, we examine how the empirical distribution over specification equivalence classes varies with sample size. For each task $x$, we measure this distribution using semantic entropy:

where $K_N(x)$ denotes the number of specification equivalence classes formed by the successfully generated specifications among the first $N$ sampling attempts, $C_i$ denotes the $i$-th equivalence class, and $n_{\mathrm{ok}}(x,N)$ is the number of these successful generations. Failed generations are excluded without replacement. We vary $N$ from 5 to 50 in increments of 5, using prefixes of the same 50-sample sequence for each task, and report the arithmetic mean of task-level entropies across the 161 HumanEval+ tasks.

As shown in Figure 9, the mean entropy increases from 1.436 bits at $N = 5$ to 2.839 bits at $N = 30$, with progressively smaller gains as the sampling budget grows. Increasing $N$ further from 30 to 50 raises the mean entropy to 3.168 bits—an additional 0.329 bits, or 11.6%, despite a 66.7% increase in sampling budget. Although the entropy continues to increase, these diminishing returns suggest that larger sample sizes provide comparatively modest gains in measured semantic diversity. We therefore select $N = 30$ as a practical trade-off between representing specification diversity and limiting sampling and equivalence-analysis costs.

Full threshold Results for RQ1

This section supplements RQ1 (§ 6.1) by examining whether the comparative advantage of contrapuntal languages depends on the completeness threshold. Figure 10 and Figure 11 extend the two joint metrics in Table 1 to the full range $\tau\in[0,1]$. The step curves include every empirical threshold at which the set of $\tau$-complete specifications changes, with the same sample-selection/acceptance and averaging rules as in Table 1. Rows correspond to the three model settings. The first two columns report MKR|C and Avg. MKR|C, respectively; the last two report CR and Avg. CR.

Contrapuntal languages achieve the highest task-level macro-averages, Avg. $\,\mathrm{MKR}\mathbin{|}\mathrm{C}$ and Avg. $\mathrm{CR}$, throughout $\tau\in[0,1]$ in all six model–benchmark settings. For each sample-level metric, they also lead throughout this range in five of the six settings. There are two exceptions on HumanEval+: with GPT-5.4 mini, plurality voting has a higher $\mathrm{MKR}\mathbin{|}\mathrm{C}$ at some low thresholds below 0.2; with Qwen3.6-Flash in thinking mode, round-trip verification has a higher $\mathrm{CR}$ at some high thresholds, including $\tau= 1$. These results support the overall performance advantage observed in RQ1 across a broad range of thresholds, particularly under task-level macro-averaging.