POSTCONDBENCH: Benchmarking Correctness and Completeness in Formal Postcondition Inference

• URL: http://arxiv.org/abs/2605.03356v1
• Date: Tue, 05 May 2026 04:29:38 GMT
• Title: POSTCONDBENCH: Benchmarking Correctness and Completeness in Formal Postcondition Inference
• Abstract summary: We introduce POSTCONDBENCH, a benchmark for evaluating method-level postcondition generation from real-world software.<n>To enable automatic evaluation, POSTCONDBENCH provides a runnable execution environment and operationalizes completeness via defect discrimination.<n>Our results reveal a substantial gap between correctness and completeness, and show that repository-level dependencies and method complexity exacerbate this gap.
• Score: 10.01438318022033
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal postconditions precisely characterize program behavior and support debugging, testing, and verification, but writing them requires substantial expertise and effort. This has motivated recent work on automatically generating postconditions from code and natural-language artifacts using large language models (LLMs). However, evaluation remains a key bottleneck. Existing benchmarks primarily emphasize correctness under limited evaluation settings, often relying on surface-form matching or manual assessment on small or synthetic datasets. We introduce POSTCONDBENCH, a multilingual benchmark for evaluating method-level postcondition generation from real-world software. POSTCONDBENCH comprises 420 Python and Java tasks drawn from 121 open-source projects, each paired with a high-quality ground-truth postcondition set constructed with expert involvement. To enable automatic evaluation, POSTCONDBENCH provides a runnable execution environment and operationalizes completeness via defect discrimination: a postcondition set is more complete if it is violated by more defective implementations while remaining satisfied on correct executions. Using POSTCONDBENCH, we formulate three generation settings and evaluate five SOTA LLMs. Our results reveal a substantial gap between correctness and completeness, and show that repository-level dependencies and method complexity exacerbate this gap.

Related papers

• Teaching Code LLMs to Reason with Intermediate Formal Specifications [9.552020178028576]
  SpecCoder is a training framework that learns from validated reference programs, behavior-changing mutants, and multi-turn specification-refinement traces.<n> SpecCoder selects specifications that hold on correct executions while rejecting faulty executions, turning specifications from passive annotations into executable evidence.
  arXiv  Detail & Related papers  (2026-07-05T11:09:30Z)
• ClarifyCodeBench: Evaluating LLMs on Clarifying Ambiguous Requirements for Code Generation [54.788849448970154]
  We introduce ClarifyCodeBench, a novel interactive benchmark for evaluating Large Language Models' capability in resolving requirement ambiguity.<n>We conduct a systematic evaluation of six state-of-the-art LLMs using ClarifyCodeBench.<n>Our empirical results yield three critical insights: 1) Capability Decoupling: Strong code generation performance does not inherently translate to effective requirement clarification; 2) The Reasoning Paradox: While increased computational thinking enhances code correctness, it yields marginal gains in identifying ambiguities.
  arXiv  Detail & Related papers  (2026-07-01T09:58:59Z)
• CDR-Bench: Evaluating Faithful Execution of Compositional, Order-Sensitive Data Refinement Recipes [52.734097662607375]
  CDR-Bench is a comprehensive benchmark featuring 3,462 high-quality tasks spanning four real-world data refinement domains.<n>Our benchmark evaluates models across atomic, order-agnostic, and order-sensitive settings.<n>Experiments on 10+ state-of-the-art LLMs reveal consistent failure patterns.
  arXiv  Detail & Related papers  (2026-06-30T10:08:45Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• You Don't Need Public Tests to Generate Correct Code [0.9668407688201359]
  We show that large language models possess the capability to autonomously construct valid inputs and simulate execution flows for self-correction.<n>We introduce DryRUN, a framework that removes the necessity for ground-truth data by enabling the LLM to iteratively plan, synthesize its own test inputs, and run simulated executions.
  arXiv  Detail & Related papers  (2026-04-23T12:21:03Z)
• SpecMind: Cognitively Inspired, Interactive Multi-Turn Framework for Postcondition Inference [7.324314351910779]
  SpecMind is a novel framework for postcondition generation that treats LLMs as interactive and exploratory reasoners.<n>Our empirical evaluation shows that SpecMind significantly outperforms state-of-the-art approaches in both accuracy and completeness of generated postconditions.
  arXiv  Detail & Related papers  (2026-02-24T07:01:17Z)
• From Benchmark Data To Applicable Program Repair: An Experience Report [1.6913109767046948]
  This paper describes our approach to automated program repair.<n>We combine various techniques from the literature to achieve this.<n>Experiments show that our approach performs better than other techniques on standard benchmarks.<n>On closer inspection, none of these techniques work on realistic defects that we see in industry.
  arXiv  Detail & Related papers  (2025-08-22T03:59:27Z)
• Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [79.74676890436174]
  We present an APR tool for Dafny that uses formal specifications as oracles for fault localization and repair.<n>We localize faults through a series of steps, which include using Hoare logic to determine the state of each statement within the program.<n>Our tool achieves 89.6% fault localization coverage and GPT-4o mini yields the highest repair success rate of 74.18%.
  arXiv  Detail & Related papers  (2025-07-04T15:36:12Z)
• A Controllable Examination for Long-Context Language Models [62.845852724511964]
  This study introduces $textbfLongBioBench, a benchmark for evaluating long-context language models.<n>We show that most models still exhibit deficiencies in semantic understanding and elementary reasoning over retrieved results.<n>Our further analysis indicates some design choices employed by existing synthetic benchmarks, such as contextual non-coherence.
  arXiv  Detail & Related papers  (2025-06-03T14:23:06Z)
• Fact-Consistency Evaluation of Text-to-SQL Generation for Business Intelligence Using Exaone 3.5 [0.0]
  Large Language Models (LLMs) have shown promise in enabling natural language interfaces for structured data querying through text-to-generation.<n>We propose a Fact-Consistency Evaluation Framework for assessing the semantic accuracy of LLM-generatedsql outputs using Exaone 3.5.<n>We construct a domain-specific benchmark comprising 219 natural language business questions, derived from actual sales data in LG Electronics' internal BigQuery environment.<n>We evaluate model performance using answer accuracy, execution success rate, semantic error rate, and non-response rate.
  arXiv  Detail & Related papers  (2025-04-30T14:42:18Z)
• Evaluating Generative Language Models in Information Extraction as Subjective Question Correction [49.729908337372436]
  We propose a new evaluation method, SQC-Score. Inspired by the principles in subjective question correction, we propose a new evaluation method, SQC-Score. Results on three information extraction tasks show that SQC-Score is more preferred by human annotators than the baseline metrics.
  arXiv  Detail & Related papers  (2024-04-04T15:36:53Z)

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.