# VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code

arXiv: https://arxiv.org/abs/2510.06296 · HTML: https://mlsanity.com/paper/2510.06296/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Builds on 30 of its 44 references that are in the map.
- First posted on arXiv 7 Oct 2025.

## Builds on (most cited first, 30 of 30)

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code](https://mlsanity.com/paper/2403.07974/) (2024)
- [Competition-Level Code Generation with AlphaCode](https://mlsanity.com/paper/2203.07814/) (2022)
- [ReTool: Reinforcement Learning for Strategic Tool Use in LLMs](https://mlsanity.com/paper/2504.11536/) (2025)
- [Absolute Zero: Reinforced Self-play Reasoning with Zero Data](https://mlsanity.com/paper/2505.03335/) (2025)
- [The Illusion of Thinking: Understanding the Strengths and Limitations of Reasoning Models via the Lens of Problem Complexity](https://mlsanity.com/paper/2506.06941/) (2025)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [ARC-AGI-2: A New Challenge for Frontier AI Reasoning Systems](https://mlsanity.com/paper/2505.11831/) (2025)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Physics of Language Models: Part 2.1, Grade-School Math and the Hidden Reasoning Process](https://mlsanity.com/paper/2407.20311/) (2024)
- [Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems](https://mlsanity.com/paper/2405.06624/) (2024)
- [LeetCodeDataset: A Temporal Dataset for Robust Evaluation and Efficient Training of Code LLMs](https://mlsanity.com/paper/2504.14655/) (2025)
- [Quantifying Contamination in Evaluating Code Generation Capabilities of Language Models](https://mlsanity.com/paper/2403.04811/) (2024)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [LLMs for Mathematical Modeling: Towards Bridging the Gap between Natural and Mathematical Languages](https://mlsanity.com/paper/2405.13144/) (2024)
- [UTBoost: Rigorous Evaluation of Coding Agents on SWE-Bench](https://mlsanity.com/paper/2506.09289/) (2025)
- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [Vulnerabilities in AI Code Generators: Exploring Targeted Data Poisoning Attacks](https://mlsanity.com/paper/2308.04451/) (2023)
- [MCTS-Judge: Test-Time Scaling in LLM-as-a-Judge for Code Correctness Evaluation](https://mlsanity.com/paper/2502.12468/) (2025)
- [Towards Understanding the Characteristics of Code Generation Errors Made by Large Language Models](https://mlsanity.com/paper/2406.08731/) (2024)
- [CLEVER: A Curated Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2505.13938/) (2025)
- [Proving the Coding Interview: A Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2502.05714/) (2025)
- [miniCodeProps: a Minimal Benchmark for Proving Code Properties](https://mlsanity.com/paper/2406.11915/) (2024)
- [DICE: Detecting In-distribution Contamination in LLM's Fine-tuning Phase for Math Reasoning](https://mlsanity.com/paper/2406.04197/) (2024)
- [AetherCode: Evaluating LLMs' Ability to Win In Premier Programming Competitions](https://mlsanity.com/paper/2508.16402/) (2025)
- [Re:Form -- Reducing Human Annotations in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny](https://mlsanity.com/paper/2507.16331/) (2025)
- [Beyond Statistical Learning: Exact Learning Is Essential for General Intelligence](https://mlsanity.com/paper/2506.23908/) (2025)

## Built on by (most cited first, 7 of 7)

- [GGBench: A Geometric Generative Reasoning Benchmark for Unified Multimodal Models](https://mlsanity.com/paper/2511.11134/) (2025)
- [Evaluating Agentic Configuration Repair for Computer Networks](https://mlsanity.com/paper/2606.06212/) (2026)
- [Vero: Can AI Agents Build Formally Verified Software Repositories?](https://mlsanity.com/paper/2608.13522/) (2026)
- [AxDafny: Agentic Verified Code Generation in Dafny](https://mlsanity.com/paper/2606.32007/) (2026)
- [LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation](https://mlsanity.com/paper/2605.01394/) (2026)
- [FVSpec: Real-World Property-Based Tests as Lean Challenges](https://mlsanity.com/paper/2606.01008/) (2026)
- [Toward Interactive Understanding of Code APIs](https://mlsanity.com/paper/2609.32081/) (2026)

## Abstract (arXiv)

Formal verification is the next frontier for ensuring the correctness of code generated by Large Language Models (LLMs). While methods that co-generate code and formal specifications in formal languages, like Dafny, can, in principle, prove alignment with user intent, progress is bottlenecked by specification quality evaluation. Current benchmarks rely on matching against ground-truth specifications, a manual and expertise-intensive process that has limited existing datasets to a few hundred simple problems and also suffers from a reliability issue. To address this, we introduce VeriEquivBench, a new benchmark with 2,389 complex algorithmic problems that probe the limitations of current models in both code generation and formal reasoning. Our evaluation framework replaces ground-truth matching with a formally grounded metric, the equivalence score, and rigorously verifies the quality of generated specifications and code. Our results show that generating formally verifiable code remains a profound challenge for state-of-the-art LLMs. This underscores both the difficulty of the task and the need for benchmarks like VeriEquivBench to drive progress toward scalable and reliable coding agents.