VerifyThisBench: Generating Code, Specifications, and Proofs All at Once

• URL: http://arxiv.org/abs/2505.19271v2
• Date: Tue, 07 Oct 2025 00:41:01 GMT
• Title: VerifyThisBench: Generating Code, Specifications, and Proofs All at Once
• Authors: Xun Deng, Sicheng Zhong, Barış Bayazıt, Andreas Veneris, Fan Long, Xujie Si,
• Abstract summary: We introduce a new benchmark that evaluates end-to-end program verification from natural language descriptions.<n>Our evaluation reveals that even state-of-the-art (SOTA) models, such as o3-mini, achieve a pass rate of less than 4%.
• Score: 9.383313869205628
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large language models (LLMs) have demonstrated remarkable progress in code generation, but many existing benchmarks are approaching saturation and offer little guarantee on the trustworthiness of the generated programs. To improve visibility into model reasoning on formal correctness, we introduce VerifyThisBench, a new benchmark that evaluates end-to-end program verification from natural language descriptions: models must (i) extract formal specifications, (ii) implement in a verification-aware language, and (iii) construct machine checkable proofs. Our evaluation reveals that even state-of-the-art (SOTA) models, such as o3-mini, achieve a pass rate of less than 4%, with many outputs failing to compile. To isolate sources of difficulty, we further propose VerifyThisBenchXS, a relaxed variant in which partial implementations or proofs are provided. Across nine models and seven verification tools on both benchmarks, we observe consistent gains with feedback-driven refinement, but overall pass rates remain low, underscoring substantial gaps in formal reasoning. We release the benchmark and the unified evaluation environment to catalyze the verification capabilities for future models.

Related papers

• IF-RewardBench: Benchmarking Judge Models for Instruction-Following Evaluation [85.56193980646981]
  We propose IF-RewardBench, a comprehensive meta-evaluation benchmark for instruction-following.<n>For each instruction, we construct a preference graph containing all pairwise preferences among multiple responses.<n>Experiments on IF-RewardBench reveal significant deficiencies in current judge models.
  arXiv  Detail & Related papers  (2026-03-05T02:21:17Z)
• Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
  Large Language Models (LLMs) show remarkable capabilities, yet their next-token prediction creates logical inconsistencies and reward hacking.<n>We introduce a formal logic verification-guided framework that dynamically interleaves formal symbolic verification with the natural language generation process.<n>We operationalize this framework via a novel two-stage training pipeline that synergizes formal logic verification-guided supervised fine-tuning and policy optimization.
  arXiv  Detail & Related papers  (2026-01-30T07:01:25Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code [25.916111156888235]
  We introduce a new benchmark for formal verification of Large Language Models (LLMs)<n>Our framework replaces ground-truth matching with a formally grounded metric, the equivalence score, and rigorously verifies the quality of generated specifications and code.<n>Our results show that generating formally verifiable code remains a profound challenge for state-of-the-art LLMs.
  arXiv  Detail & Related papers  (2025-10-07T13:19:05Z)
• STEPWISE-CODEX-Bench: Evaluating Complex Multi-Function Comprehension and Fine-Grained Execution Reasoning [6.282781900938977]
  We present STEPWISE-CODEX-Bench (SX-Bench), a novel benchmark for complex multi-function understanding and fine-grained execution reasoning.<n>SX-Bench is highly discriminative, even the state-of-the-art OpenAI-O3 achieves only 78.37 percent accuracy on Hard-Reasoning tasks.
  arXiv  Detail & Related papers  (2025-08-07T09:28:43Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  We develop CompassVerifier, an accurate and robust lightweight verifier model for evaluation and outcome reward.<n>It demonstrates multi-domain competency spanning math, knowledge, and diverse reasoning tasks, with the capability to process various answer types.<n>We introduce VerifierBench benchmark comprising model outputs collected from multiple data sources, augmented through manual analysis of metaerror patterns to enhance CompassVerifier.
  arXiv  Detail & Related papers  (2025-08-05T17:55:24Z)
• AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction [32.14733357890831]
  We propose AssertCoder, a novel unified framework that automatically generates high-quality SVAs.<n>AssertCoder employs a modality-sensitive preprocessing to parse heterogeneous specification formats.<n>The framework incorporates a mutation-based evaluation approach to assess assertion quality.
  arXiv  Detail & Related papers  (2025-07-14T14:43:14Z)
• Supporting Software Formal Verification with Large Language Models: An Experimental Study [9.688989142858954]
  SpecVerify integrates large language models with formal verification tools.<n>This framework combines Claude 3.5 Sonnet with the ESBMC verifier to form an automated workflow.<n> Evaluated on nine cyber-physical systems from Lockheed Martin, SpecVerify achieves 46.5% verification accuracy, comparable to NASA's CoCoSim.
  arXiv  Detail & Related papers  (2025-07-07T10:30:05Z)
• VERINA: Benchmarking Verifiable Code Generation [47.9771074559674]
  Large language models (LLMs) are increasingly integrated in software development.<n>Verifiable code generation offers a promising path to address this limitation.<n>Current benchmarks often lack support for end-to-end verifiable code generation.
  arXiv  Detail & Related papers  (2025-05-29T06:12:52Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• Scoring Verifiers: Evaluating Synthetic Verification for Code and Reasoning [59.25951947621526]
  We propose an approach which can transform existing coding benchmarks into scoring and ranking datasets to evaluate the effectiveness of synthetic verifiers.<n>We release four new benchmarks (HE-R, HE-R+, MBPP-R, and MBPP-R+), and analyzed synthetic verification methods with standard, reasoning-based, and reward-based LLMs.<n>Our experiments show that reasoning can significantly improve test case generation and that scaling the number of test cases enhances the verification accuracy.
  arXiv  Detail & Related papers  (2025-02-19T15:32:11Z)
• Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation [24.081573908824353]
  First-order logic (FOL) reasoning is pivotal for intelligent systems.<n>Existing benchmarks often rely on extensive human annotation or handcrafted templates.<n>We propose a novel framework called ProverGen that synergizes the generative strengths of Large Language Models with the rigor and precision of symbolic provers.
  arXiv  Detail & Related papers  (2025-02-10T15:31:54Z)
• FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware [4.480157114854711]
  We present FVEval, the first comprehensive benchmark for characterizing large language models (LLMs) performance in tasks pertaining to formal verification (FV) The benchmark consists of three sub-tasks that measure LLM capabilities at different levels. We present both collections of expert-written verification collateral and methodologies to scalably generate synthetic examples aligned with FV.
  arXiv  Detail & Related papers  (2024-10-15T21:48:57Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  Large language models (LLMs) struggle with consistent and accurate reasoning. LLMs are trained primarily on correct solutions, reducing their ability to detect and learn from errors. We propose a novel collaborative method integrating Chain-of-Thought (CoT) and Program-of-Thought (PoT) solutions for verification.
  arXiv  Detail & Related papers  (2024-10-05T05:21:48Z)
• AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation [6.3585378855805725]
  We present a novel benchmark to evaluate Large-Language Models' effectiveness for assertion generation.<n>AssertioBench contains 100 curated Verilog hardware designs from OpenCores and formally verified assertions for each design generated from GoldMine and HARM.
  arXiv  Detail & Related papers  (2024-06-26T14:47:28Z)
• Benchmarking Uncertainty Quantification Methods for Large Language Models with LM-Polygraph [83.90988015005934]
  Uncertainty quantification is a key element of machine learning applications.<n>We introduce a novel benchmark that implements a collection of state-of-the-art UQ baselines.<n>We conduct a large-scale empirical investigation of UQ and normalization techniques across eleven tasks, identifying the most effective approaches.
  arXiv  Detail & Related papers  (2024-06-21T20:06:31Z)
• SORRY-Bench: Systematically Evaluating Large Language Model Safety Refusal [64.9938658716425]
  SORRY-Bench is a proposed benchmark for evaluating large language models' (LLMs) ability to recognize and reject unsafe user requests.<n>First, existing methods often use coarse-grained taxonomy of unsafe topics, and are over-representing some fine-grained topics.<n>Second, linguistic characteristics and formatting of prompts are often overlooked, like different languages, dialects, and more -- which are only implicitly considered in many evaluations.
  arXiv  Detail & Related papers  (2024-06-20T17:56:07Z)
• Model Reprogramming Outperforms Fine-tuning on Out-of-distribution Data in Text-Image Encoders [56.47577824219207]
  In this paper, we unveil the hidden costs associated with intrusive fine-tuning techniques. We introduce a new model reprogramming approach for fine-tuning, which we name Reprogrammer. Our empirical evidence reveals that Reprogrammer is less intrusive and yields superior downstream models.
  arXiv  Detail & Related papers  (2024-03-16T04:19:48Z)
• Self-Evaluation Improves Selective Generation in Large Language Models [54.003992911447696]
  We reformulate open-ended generation tasks into token-level prediction tasks. We instruct an LLM to self-evaluate its answers. We benchmark a range of scoring methods based on self-evaluation.
  arXiv  Detail & Related papers  (2023-12-14T19:09:22Z)
• On the Reliability and Explainability of Language Models for Program Generation [15.569926313298337]
  We study the capabilities and limitations of automated program generation approaches. We employ advanced explainable AI approaches to highlight the tokens that significantly contribute to the code transformation. Our analysis reveals that, in various experimental scenarios, language models can recognize code grammar and structural information, but they exhibit limited robustness to changes in input sequences.
  arXiv  Detail & Related papers  (2023-02-19T14:59:52Z)
• On the Limits of Evaluating Embodied Agent Model Generalization Using Validation Sets [101.28658250723804]
  This paper experiments with augmenting a transformer model with modules that effectively utilize a wider field of view and learn to choose whether the next step requires a navigation or manipulation action. We observe that the proposed modules resulted in improved, and in fact state-of-the-art performance on an unseen validation set of a popular benchmark dataset, ALFRED. We highlight this result as we believe it may be a wider phenomenon in machine learning tasks but primarily noticeable only in benchmarks that limit evaluations on test splits.
  arXiv  Detail & Related papers  (2022-05-18T23:52:21Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.