Improving Dynamic Specification Inference with LLM-Generated Counterexamples

• URL: http://arxiv.org/abs/2604.10761v1
• Date: Sun, 12 Apr 2026 18:09:53 GMT
• Title: Improving Dynamic Specification Inference with LLM-Generated Counterexamples
• Abstract summary: This paper explores the use of large language models (LLMs) to automatically generate tests that attempt to invalidate generated assertions.<n>Our results show that state-of-the-art LLMs can generate effective counterexamples that help to discard up to 11.68% of invalid assertions inferred by SpecFuzzer.
• Score: 3.555888578860533
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Contract assertions, such as preconditions, postconditions, and invariants, play a crucial role in software development, enabling applications such as program verification, test generation, and debugging. Despite their benefits, the adoption of contract assertions is limited, due to the difficulty of manually producing such assertions. Dynamic analysis-based approaches, such as Daikon, can aid in this task by inferring expressive assertions from execution traces. However, a fundamental weakness of these methods is their reliance on the thoroughness of the test suites used for dynamic analysis. When these test suites do not contain sufficiently diverse tests, the inferred assertions are often not generalizable, leading to a high rate of invalid candidates (false positives) that must be manually filtered out. In this paper, we explore the use of large language models (LLMs) to automatically generate tests that attempt to invalidate generated assertions. Our results show that state-of-the-art LLMs can generate effective counterexamples that help to discard up to 11.68\% of invalid assertions inferred by SpecFuzzer. Moreover, when incorporating these LLM-generated counterexamples into the dynamic analysis process, we observe an improvement of up to 7\% in precision of the inferred specifications, with respect to the ground-truths gathered from the evaluation benchmarks, without affecting recall.

Related papers

• Evaluating and Mitigating the Misguidance Effect of Buggy Code in LLM-Generated Unit Tests [6.228248513679207]
  This paper presents a new metric to measure the "misguidance effect," a phenomenon where buggy code steers LLMs toward generating tests that validate its erroneous behavior rather than expose it.<n>We introduce and validate a specification-based unit test generation paradigm that replaces the code under test in the prompt with an LLM-generated specification docstring.<n>Our results show that this paradigm effectively reduces misguided tests while substantially increasing effective tests, improves multi-round, feedback-driven test generation pipelines, and remains applicable to both buggy and bug-free code.
  arXiv  Detail & Related papers  (2026-07-24T19:47:41Z)
• Neuroforger: certified violation witnesses for smart contracts verification via LLMs [0.0]
  Recent large language models (LLMs) incorporate reasoning capabilities that allow them to perform well in predicting whether a smart contract respects a certain property.<n>We introduce a new formal specification language that extends Solidity with abstract types.<n>We design a workflow that combines LLMs with type checking and concrete execution to generate and validate violation witnesses.
  arXiv  Detail & Related papers  (2026-05-29T14:54:51Z)
• 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)
• RESTestBench: A Benchmark for Evaluating the Effectiveness of LLM-Generated REST API Test Cases from NL Requirements [0.13681174239726607]
  RESTestBench is a benchmark comprising three REST services paired with manually verified NL requirements.<n>We evaluate two approaches across multiple state-of-the-art LLMs: (i) non-refinement-based generation, and (ii) refinement-based generation guided by interaction with the running SUT.
  arXiv  Detail & Related papers  (2026-04-28T16:59:08Z)
• On the Soundness and Consistency of LLM Agents for Executing Test Cases Written in Natural Language [4.290931412096985]
  The use of natural language (NL) test cases for validating graphical user interface (GUI) applications is emerging as a promising direction.<n>Recent advances in large language models (LLMs) have opened the possibility of the direct execution of NL test cases by LLM agents.<n>This paper investigates the impact on NL test case unsoundness and on test case execution consistency.
  arXiv  Detail & Related papers  (2025-09-23T15:20:40Z)
• 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)
• Toward Automated Validation of Language Model Synthesized Test Cases using Semantic Entropy [0.5057850174013127]
  Modern Large Language Model (LLM)-based programming agents often rely on test execution feedback to refine their generated code.<n>This paper introduces VALTEST, a novel framework that leverages semantic entropy to automatically validate test cases generated by LLMs.<n>Experiments show that VALTEST boosts test validity by up to 29% and improves code generation performance, as evidenced by significant increases in pass@1 scores.
  arXiv  Detail & Related papers  (2024-11-13T00:07:32Z)
• 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)
• Prompt Optimization with EASE? Efficient Ordering-aware Automated Selection of Exemplars [66.823588073584]
  Large language models (LLMs) have shown impressive capabilities in real-world applications. The quality of these exemplars in the prompt greatly impacts performance. Existing methods fail to adequately account for the impact of exemplar ordering on the performance.
  arXiv  Detail & Related papers  (2024-05-25T08:23:05Z)
• 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)
• ReEval: Automatic Hallucination Evaluation for Retrieval-Augmented Large Language Models via Transferable Adversarial Attacks [91.55895047448249]
  This paper presents ReEval, an LLM-based framework using prompt chaining to perturb the original evidence for generating new test cases. We implement ReEval using ChatGPT and evaluate the resulting variants of two popular open-domain QA datasets. Our generated data is human-readable and useful to trigger hallucination in large language models.
  arXiv  Detail & Related papers  (2023-10-19T06:37:32Z)
• LLMs as Factual Reasoners: Insights from Existing Benchmarks and Beyond [135.8013388183257]
  We propose a new protocol for inconsistency detection benchmark creation and implement it in a 10-domain benchmark called SummEdits. Most LLMs struggle on SummEdits, with performance close to random chance. The best-performing model, GPT-4, is still 8% below estimated human performance.
  arXiv  Detail & Related papers  (2023-05-23T21:50:06Z)

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.