# Veriequivbench Eval

> 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. Use when the user wants to benchmark on VeriEquivBench, or asks about evaluating this task. Reports equivalence_score.

- Skill: `qhjqhj00/veriequivbench-eval` (Agent Skill)
- Install (CLI): `npx skillmds add qhjqhj00/veriequivbench-eval`
- Raw SKILL.md: https://api.skillmd.com/api/skills/qhjqhj00/veriequivbench-eval/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: AI & ML
- Author: qhjqhj00 (https://skillmd.com/u/qhjqhj00)
- Updated: 2026-09-08
- Page: https://skillmd.com/skills/qhjqhj00/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

```python
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

```bibtex
@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