PaperlayerView exact revision on arXiv

Source-linked AI summary

Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation

Srijith Nair, Aditya Vempaty, Jia Liu, Ashish Jagmohan

arXiv:2610.10604v1cs.SEcs.AI

TL;DR

A checked proof can establish correctness against a contract that misrepresents user intent, and SpecGen lacks a definitive check for that gap. The paper unifies evaluation signals and applies them to existing Lean tasks; results show that measurement coverage affects comparisons and authored controls expose a blind spot in postcondition-only scores.

  • Problem

    SpecGen lacks a definitive feedback mechanism for determining whether a generated specification captures user intent, unlike proof generation's deterministic prover feedback.

    Source: §1 · p. 2

  • Method

    The paper unifies formal-validity, reference-based, and behavioral evaluation signals and applies them to existing VERINA and CLEVER Lean tasks.

    Source: §1 · p. 3, §2.3 · p. 5

  • Results

    The results show that comparisons depend on measurement coverage, while authored controls demonstrate that perfect postcondition scores can coexist with exclusion of every required input.

    Source: §1 · p. 3, §5 · p. 9

  • Takeaways & Limitations

    Evaluating complete contracts requires separate attention to input-domain coverage and output constraints, with each signal's scope and availability reported.

    Source: §5 · p. 9

    The study covers one model and two Lean datasets, and does not establish that its metrics improve generation when used as feedback.

    Source: §4 · p. 9

Abstract

from arXiv · show

When generating verifiable code, natural language requirements are mapped to machine checked code using LLMs and agentic workflows. A crucial component of this pipeline is specification generation (SpecGen), which produces a formal contract against which an agent can prove implementation correctness. Proof generation can obtain deterministic feedback from a theorem prover, but SpecGen lacks a definitive check that a generated specification captures the user's intent. A checked proof can therefore establish correctness against a specification that misrepresents the intended behaviour. We take a step towards holistic SpecGen evaluation with a unified dataset assembled from $350$ existing Lean tasks, including $189$ from VERINA and $161$ from CLEVER, and a framework covering formal validity, reference similarity and equivalence, and behavioural adequacy. We distinguish acceptance of required inputs from acceptance of valid outputs and rejection of invalid outputs, while making each metric's evidence scope explicit. Across four SpecGen configurations, restricting the generalized tree edit distance (GTED) comparison, a reference similarity measure, to $32$ jointly measurable VERINA tasks changes the VERINA configuration's position from second to fourth in mean similarity, showing the importance of measurement coverage. In an authored control, a specification achieves $100\%$ positive test recall and negative test rejection while accepting $0\%$ of required inputs. This demonstrates that perfect postcondition scores can miss an unusable input contract, motivating separate feedback on input coverage and output constraints.

1 Introduction

Verifiable code generation depends on specifications that capture user requirements, but proof checking alone cannot verify that a specification reflects user intent. The paper introduces a multi-signal evaluation framework and applies it to existing Lean tasks, with authored controls illustrating why input coverage and output constraints need separate feedback.

1 Introduction

  • A checked proof establishes implementation correctness relative to the formal contract and its assumptions, so assurance about user intent also depends on the contract capturing the requirement.The pipeline maps natural-language requirements to a formal contract, then generates code and a proof against that contract.Source: §1 · p. 2
  • SpecGen lacks a definitive feedback mechanism, while type-checking can accept a well-typed predicate that expresses the wrong relation.The framework asks which dimensions of specification quality different evaluation signals reveal and what feedback they provide.Source: §1 · p. 2
  • The framework unifies evaluation signals by the questions they answer and the evaluation modalities they require.The paper also builds on benchmarks that already treat specification generation as distinct from code and proof generation.Source: §1 · p. 2
  • The unified dataset contains 350 existing Lean tasks from VERINA and CLEVER, preserving source provenance rather than introducing newly authored problems.The evaluation uses 189 VERINA and 161 CLEVER tasks; adapters support the two evaluation harnesses.Source: §1 · pp. 2–3
  • In an authored control, perfect postcondition-test scores coexist with zero required-input recall, showing that input coverage and output constraints need separate feedback.The finding demonstrates a blind spot of postcondition-only feedback, not its prevalence in model outputs.Source: §1 · p. 3

2 Benchmark Design

The benchmark evaluates generated specifications through complementary evidence sources, covering formal validity, reference comparison, and behavior on labeled examples. Its metrics are conditional on available artifacts and dependencies, with evidence scope and status recorded explicitly.

2.1 Evaluation-system Overview

  • Each task’s candidate is evaluated against the Lean environment, dataset reference, natural-language intent, and optionally labeled examples, with scope and evidence status recorded.The system distinguishes unavailable evidence from observed metric failures.Source: §2.1 · p. 3

2.2 Datasets and SpecGen agents

  • Four configurations using the same GPT-5.6 (Sol) base agent are evaluated on 189 VERINA and 161 CLEVER tasks, differing in prompts, representations, retries, and post-processing.The configurations are direct prompting, VERINA, CLEVER few-shot, and a LeanAide adapter.Source: §2.2 · p. 3

2.3 Supported SpecGen Evaluation Metrics

  • The framework groups metrics into formal validity, reference similarity, reference equivalence, and behavioral adequacy, defining binary and graded metrics only when required artifacts and dependencies are available.Lean type checking tests declaration acceptance but does not establish agreement with a reference or natural-language requirement.Source: §2.3 · p. 4
  • Reference similarity compares candidates with dataset references textually, symbolically, and structurally, but resemblance scores cannot establish logical equivalence.The measures include normalized exact match, signature and logical-atom F1, and generalized tree-edit similarity.Source: §2.3 · p. 4
  • The logical-atom tokenizer omits numeric literals and the Unicode operators ≤, ≥, and ≠, limiting sensitivity to changes in those features.GTED uses elaborated operator trees and normalizes edit distance by the larger tree size; a score of 1 indicates identical operator trees under the adopted construction.Source: §2.3 · pp. 4–5
  • Reference equivalence seeks bidirectional implication proofs for projected statements; successful checks require Lean kernel-checked evidence, while proof-search failure is inconclusive.Equivalence proof construction can itself be challenging.Source: §2.3 · p. 5
  • Behavioral adequacy measures positive-test recall, negative-test rejection, balanced accuracy, and VERINA pass@1, while required-input recall evaluates the precondition independently.Finite-example scores neither prove universal correctness nor show that the test oracle fully captures the natural-language requirement.Source: §2.3 · pp. 5–6
  • LeanScorer provides an auxiliary requirement-conditioned LLM assessment, while conditional metrics report applicable denominators and evidence status, representing unavailable evidence as ⊥ rather than zero.LeanScorer judgments are aggregated using a Sugeno fuzzy integral.Source: §2.3 · p. 6

3 Experimental Results

Across four SpecGen configurations, the experiments evaluate validity, reference resemblance, natural-language alignment, and behavioral outcomes on VERINA and CLEVER. Their results show that measurement coverage and evaluator compatibility constrain comparisons, while behavioral evidence does not establish intent fidelity.

3.1 Implementation details

  • The experiments compare complete configurations with differing generation budgets and repair procedures, and metric availability and evaluation compatibility limit cross-configuration interpretation.The runs configure the same GPT-5.6 reasoning effort and token limits, but prompts and harnesses vary, so realized token use is not guaranteed equal.Source: §3.1 · p. 6

3.2 VERINA and CLEVER results

  • Across attempted tasks, recorded type-checking rates were often high, but candidate production varied, so conditional success could conceal missing candidates.On CLEVER, LeanAide recorded a 100% conditional type-checking rate while returning 135/161 candidates (83.9%).Source: §3.2 · p. 6
  • Available-measurement mean GTED favored different configurations across datasets, but the averages covered different subsets and do not provide a controlled semantic-quality ranking.On VERINA, the prompted baseline scored 0.349 on 46/189 measurements; on CLEVER, the CLEVER configuration scored 0.321 on 124/161.Source: §3.2 · p. 6
  • On 32 jointly measurable VERINA tasks, the VERINA configuration’s mean GTED fell from 0.335 to 0.288, moving from second to fourth; the intersection was metric-selected and not representative.On CLEVER, the 85-task intersection preserved the ordering among three configurations.Source: Figure 3 · p. 7, §3.2 · p. 7
  • Logical-atom F1 means ranged from 0.241 to 0.269 on VERINA and 0.298 to 0.414 on CLEVER, yet neither signal provides a correctness threshold.The selected declaration still requires inspection: a CLEVER example selected a reference helper instead of the intended contract.Source: §3.2 · p. 8
  • On VERINA, mean LeanScorer values were 0.655, 0.752, 0.755, and 0.681 for VERINA, CLEVER, Prompted, and LeanAide, respectively; LeanScorer is an LLM-based judge, not a formal guarantee.The corresponding available-generation counts were 189, 189, 189, and 181.Source: §3.2 · p. 8, Figure 4 · p. 8
  • Across VERINA configurations, 357 of 469 behavioral nonpasses had explicit harness errors, and 112 lacked enough evidence to identify a witnessed semantic failure.For the VERINA configuration, all 165 behavioral nonpasses had harness errors; its precondition and postcondition declarations were not consistently preserved by the behavioral projection.Source: §3.2 · p. 8
  • CLEVER finite-test outcomes were historical rather than independently revalidated, and the runs lacked CLEVER behavioral measurements and required-input recall for real outputs.Authored controls were used to check whether three behavioral metrics respond separately to known postcondition and input-domain defects.Source: §3.2 · p. 8

4 Related Work, Limitations, and Future Work

The paper situates its framework alongside work on specification generation, reference certification, semantic evaluation, and requirement-level validation. It identifies limits in the study’s evidence and outlines ways to strengthen future evaluation.

Related work

  • The framework complements VERINA, CLEVER, LeanEuclid, and VeriSpecGen by relating evaluation signals to feedback roles and demonstrating why input-domain coverage merits separate assessment.The authors state that semantic evaluation is not their novelty and do not claim prior work ignored the intent gap.Source: §4 · p. 9

Limitations

  • The study covers one model and two Lean datasets; uneven metric coverage, projection failures, and historical evaluation errors constrain comparisons, while intent fidelity and metric benefits remain unestablished.The prevalence of input-coverage failures in generated outputs is unmeasured.Source: §4 · p. 9

Future work

  • Future work proposes preserving complete contracts across evaluators, checking references and counterexamples, testing more models and domains with matched budgets and held-out tasks, and adding datasets and languages.The authors also propose testing whether combined signals improve specification quality over type-checking feedback alone and at what generation cost.Source: §4 · p. 9

5 Conclusion

The conclusion argues that SpecGen evaluation requires multiple signals interpreted according to their evidence scope. It also points to unresolved questions about intent fidelity and the evaluation of concrete benchmark examples.

5 Conclusion

  • The framework’s results show that measurement coverage affects comparisons and evaluator failures can resemble specification failures; authored controls show perfect postcondition scores can coexist with exclusion of every required input.Whether richer feedback improves agents’ fidelity to user intent remains an open next step.Source: §5 · p. 9

A Actual VERINA and CLEVER examples

  • The appendix examples are saved benchmark-run records, and required-input recall is unavailable for all four rows.All four rows use the CLEVER configuration; a dash denotes unavailable evidence, and BEq 0 means no equivalence proof was obtained, not proof of inequivalence.Source: A Actual VERINA and CLEVER examples · p. 12

A.1 Integer square root: equivalence despite moderate similarity

  • The VERINA task verina_basic_65 asks for the largest natural number r whose square is at most N while N is less than (r + 1) squared.This is the integer-square-root task stated in the source excerpt.Source: §A.1 · p. 12

Reference specification (precondition / postcondition)

One VERINA example combines successful equivalence and finite-test outcomes with only moderate structural resemblance. The accompanying sorted-deduplication task asks for duplicate removal and ascending order.

Reference specification (precondition / postcondition)

  • 5 positive and 13 negative examples pass, and the equivalence check succeeds, despite GTED similarity of 0.435.NEM is zero, while logical-atom F1 is 0.444; the comparison concerns a generatedSpec wrapper and an explicit reference formula.Source: Reference specification (precondition… · p. 12

A.2 Sorted deduplication: behavioral zeros without counterexamples

  • The VERINA row is verina_advanced_81, whose task asks for duplicate removal and ascending ordering of a list of integers.The natural-language excerpt specifies a Lean 4 function.Source: §A.2 · p. 13

Reference specification (precondition / postcondition)

The sorted-deduplication example records failed behavioral evaluation despite a successful type check, while the supplied addition example gives only its task identity and request.

Reference specification (precondition / postcondition)

  • The sorted-deduplication candidate and reference use different predicates for the same intended sorted set, but saved BEq does not establish equivalence.Logical-atom F1 is 0.171; GTED is 0.423 from distance 15 over a larger tree of size 26.Source: Reference specification (precondition… · p. 13
  • 0/5 positive successes and 0/15 negative rejections are recorded, but evaluator decidability failures mean these zeros do not establish output acceptance or rejection.The candidate typechecks; a negative test’s output is excluded by Nodup, but the attempted test fails to obtain decidability.Source: Reference specification (precondition… · p. 13

A.3 Integer addition: an inconclusive equivalence search

  • CLEVER row 52 concerns integer addition: its natural-language request is to add two numbers, x and y.The supplied passages identify the task but do not report its comparison outcome here.Source: §A.3 · p. 14

Reference specification

The addition comparison is algebraically consistent but remains unproved, while the triangle-area example shows that agreement with a reference can differ from matching the stated output requirement.

Reference specification

  • BEq remains inconclusive for addition: substituting the implementation output into the reference’s existential equality yields the candidate condition, but no successful proof is recorded.Exact match is zero, logical-atom F1 is 0.538, and GTED is 0.200; behavioral fields are unavailable for this run.Source: Reference specification · p. 14

A.4 Triangle area: reference agreement is a separate question

  • CLEVER row 44 is a triangle-area task asking for area from a side length and height.The natural-language excerpt uses the phrase “high return area.”Source: §A.4 · p. 15

Reference specification

The triangle-area example separates a generated contract’s output constraint from the reference’s guarded obligation. Supporting audits qualify compilation, projection, and feature-based measurements.

Reference specification

  • For base 2 and height 3, output 999 satisfies the reference’s local obligation but violates the candidate’s required output of 3.The reference implication guards the whole conjunction with a = 0, whereas the candidate leaves behavior outside its nonnegative-input guard unspecified.Source: Reference specification · p. 15
  • Both declarations typecheck, yet logical-atom F1 of 0.688 misses the moved guard; GTED is 0.200 and behavioral measurements are unavailable.These metrics do not diagnose the guard issue in this example.Source: Reference specification · p. 15

B Audits supporting measurement validity

  • All 350 upstream contracts compile in pinned native environments, while common-projection failures involve compatibility, missing context, and representation differences.The four CLEVER export failures use List.indexOf instead of upstream List.idxOf; 16 CLEVER projection failures involve imports or source-local helpers. Table 1 distinguishes native/export source-environment checks from a Mathlib 4.20 common projection using a different artifact.Source: B Audits supporting measurement validity · p. 16, Table 1 · p. 16
  • The 62 VERINA and 20 CLEVER textual differences are not adjudicated semantic-defect counts, and native compilation does not certify agreement with natural-language requirements.A retained counterexample recheck timed out importing Mathlib, so it is not used as successful independent certification of reference witnesses.Source: B Audits supporting measurement validity · p. 16
  • Empty signature features on both sides yield Signature F1 of one by convention, while numeric literals and some Unicode comparisons are omitted from logical-atom extraction.Historical scores are retained within these limits; generation-failure logical-atom zeros differ from unavailable GTED measurements, which are excluded from GTED means.Source: B Audits supporting measurement validity · p. 16

B.1 Structural-score distributions and projection checks

GTED distributions expose differences hidden by conditional means, but high recorded scores can reflect incomplete normalizations rather than complete contract comparisons. Behavioral evidence checks distinguish observed finite passes from unresolved outcomes, while coverage and replay limits constrain cross-configuration interpretation.

B.1 Structural-score distributions and projection checks

  • VERINA’s GTED mean was 0.335 versus median 0.200, with 14/115 available scores at one; Figure 5 shows the underlying distributions.On CLEVER, the CLEVER and LeanAide configurations both had median GTED 0.200, despite means of 0.321 and 0.233.Source: §B.1 · p. 16, Figure 5 · p. 17
  • Some perfect GTED scores compare incomplete normalized fragments, so they do not establish that complete contracts were compared.The inspected examples include GTED 1 alongside low logical-atom F1; the authors retain historical scores and do not generalize the defect to all fourteen perfect-score records.Source: §B.1 · p. 16
  • Across measured groups, logical-atom F1 and GTED correlations ranged from −0.238 to 0.219, but projection failures and discrete scores preclude interpreting this as independence.Historical behavioral scores can also coexist with execution errors, so numerical metric availability alone does not establish valid evidence.Source: §B.1 · p. 16

B.2 Behavioral evidence and cohort checks

  • The retrospective classification separates reported finite passes from unresolved nonpasses, unsupported cases, generation failures, and harness errors across 756 VERINA attempts.A reported finite pass requires both recorded test-class scores to equal one without an inspected evaluator-error flag.Source: §B.2 · p. 17, Table 2 · p. 17
  • The revised behavioral path records indexed Boolean outcomes and withholds scores for compilation failure, missing decidability, or incomplete output; the five-task replay produced no completed results.The replay’s Lean-session timeouts do not revalidate the historical cohort or justify replacing its scores.Source: §B.2 · p. 17
  • After excluding two demonstrations, pass/harness-error/unresolved/unsupported/no-output counts were 0/163/0/24/0 for VERINA, 94/10/59/24/0 for CLEVER, 29/125/9/24/0 for prompted, and 61/52/44/22/8 for LeanAide.The checks support traceability and interpretation, not a budget-matched, held-out semantic leaderboard.Source: §B.2 · pp. 17–18

B.3 Complete metric comparison and benchmark dashboard

The metric comparison and dashboard make metric availability visible, while authored controls separate postcondition behavior from required-input coverage. These controls show that strong output-test scores can coexist with excluded required inputs.

B.3 Complete metric comparison and benchmark dashboard

  • The comparison reports scalar signals with bracketed measurement counts, and the dashboard exposes metric availability, agent distributions, summary values, and comparisons.The dashboard covers 756 VERINA task–agent records.Source: §B.3 · p. 18, Figure 6 · p. 19

B.4 Authored calibration controls

  • The constant-true control had unavailable postcondition measurements, so the retained run does not establish successful calibration of every authored control.A dash in Table 4 denotes unavailable evidence.Source: §B.4 · p. 19, Table 4 · p. 20
  • With y ≥ x, positive-test recall was 1 and negative-test rejection 1/2; restricting the postcondition to y = x + 1 reversed these scores.Figure 7 visualizes six distinct measured patterns for the requirement to return an integer y > x.Source: Figure 7 · p. 19, §B.4 · p. 20
  • Keeping y > x while setting the precondition to x > 0 or False preserved both postcondition scores at 1, while required-input recall fell to 1/3 or 0.The false precondition excludes every required input while leaving the independently tested postcondition unchanged.Source: §B.4 · pp. 19–20
Loading 2610.10604v1…