Veriequivbench Eval

veriequivbench-eval

VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code — Lingfei Zeng et al. (2025) (arXiv:2510.06296, 2025)

What this evaluates

Evaluates an LLM's ability to generate formally verifiable code that aligns with natural language problem descriptions and passes unit tests. It probes complex algorithmic reasoning and code-specification alignment without requiring manual ground-truth specifications.

Datasets

• VeriEquivBench — total 2389; splits: (unstated); repo https://github.com/PunyGood/VeriEquivBench

Metrics

• equivalence_score (primary) — range: [0, 1]
  • Computed via a two-step protocol: (1) an LLM rewrites the natural language description to mirror the formal specification, and a second LLM judges the alignment yielding a score; (2) the formal specification is translated to Python and executed against ground-truth unit tests to compute the passing rate.

Input / output format

Input: Natural language problem description, formal Dafny specification, reference Python solution, and unit tests.

Output: Annotated Dafny code implementation.

Scoring recipe

def compute_equivalence_score(predictions, gold):
    total_score = 0
    for pred, g in zip(predictions, gold):
        eq_score = llm_evaluate_alignment(g['nl_query'], g['spec'])
        py_spec = translate_dafny_to_python(g['spec'])
        test_pass = run_unit_tests(py_spec, g['unit_tests'])
        total_score += (eq_score + test_pass) / 2
    return total_score / len(predictions)

Common pitfalls

• Assuming the generated Dafny code is directly executable; the protocol requires translating the formal specification to Python for unit test validation.
• Relying on manual specification evaluation instead of the automated equivalence score, which is designed to be ground-truth-free.
• Evaluating on the original LeetCode test set without filtering for the TagComp subset, risking contamination on novel tag-composed problems.

Evidence (verbatim from paper)

Equivalence to NL The equivalence check follows the protocol proposed by Clover (2024) and contains two steps: (1) A model (we use Grok4 here) rewrites the description so that it cleanly mirrors the specification, then another model (Claude-4) judges the equivalence between the original description and the rewritten one, yielding a score; (2) The specification alone is translated into Python and executed against the ground-truth LeetCode unit tests. The unit test passing rate is reported in Appendix D.1.

Citation

@misc{zeng2025veriequivbench,
  title={VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code},
  author={Lingfei Zeng et al. (2025)},
  year={2025},
  note={arXiv:2510.06296}
}

• arXiv: 2510.06296