Reinforcement Learning with Negative Tests as Completeness Signal for Formal Specification Synthesis

• URL: http://arxiv.org/abs/2604.05820v1
• Date: Tue, 07 Apr 2026 12:53:42 GMT
• Title: Reinforcement Learning with Negative Tests as Completeness Signal for Formal Specification Synthesis
• Abstract summary: We present SpecRL, a reinforcement learning framework for specification in Dafny.<n>We use the fraction of negative tests rejected by a candidate specification as a signal of specification completeness.<n>Experiments show that SpecRL improves both specification strength and verification success over SFT and RL.
• Score: 7.936959383169967
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The specification synthesis task aims to automatically generate specifications, together with any necessary auxiliary verification annotations, for existing programs. This task is important because such specifications serve as behavioral contracts that support modular reasoning and reusable verification across a codebase. At the same time, it remains challenging because verifier-only feedback is fundamentally incomplete: passing verification establishes soundness, but cannot distinguish weak specifications from strong ones. What is missing is a fine-grained signal for specification completeness. We present SpecRL, a reinforcement learning framework for specification synthesis in Dafny. SpecRL introduces a self-contained pipeline that generates negative tests, i.e., input-output pairs that can never be produced by the program. We use the fraction of these negative tests rejected by a candidate specification as a signal of specification completeness, which is integrated into the reward for RL training. Experiments across four model sizes show that SpecRL improves both specification strength and verification success over SFT and RL with a binary specification-strength reward, generalizes to an out-of-distribution benchmark, and remains competitive on that unseen benchmark compared to much larger general-purpose LLMs.

Related papers

• ProofPulse: Interactive Proof Coverage Analysis for Dafny [47.23158426199152]
  Deductive verification ensures that an implementation satisfies its specification, but successful verification does not guarantee the quality of the specification.<n>We present proofpulse, a tool for Dafny that diagnoses specification quality using a three-valued proof coverage model.
  arXiv  Detail & Related papers  (2026-08-31T14:00:31Z)
• How Powerful are LLMs in Generating Formal Program Specifications? [20.791968710071973]
  Coins is an evaluation framework that assesses specification quality by instantiating specifications under evaluation on trusted test cases and generating concrete proof obligations.<n>We conduct a large scale study on HumanEval with a curated set of human written Rocq specifications.<n>Our results show that specification generation remains a formidable challenge, and that verification complexity can obscure genuine differences in specification quality.
  arXiv  Detail & Related papers  (2026-08-13T10:45:18Z)
• 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)
• Self-Improving In-Context Learning [3.9202238580555417]
  We propose to improve in-context learning by optimizing the embeddings of a few prompt test at time.<n>We formalize this signal as a bounded, self-supervised calibration procedure.<n>Across a comprehensive suite of ICL tasks, the proposed calibration improves or matches upon the base model and consistently outperforms classification-specific baselines on most tasks.
  arXiv  Detail & Related papers  (2026-05-22T03:01:34Z)
• Certified Program Synthesis with a Multi-Modal Verifier [5.998029529040967]
  LeetProof is an agentic pipeline built on Velvet, a multi-modal verifier embedded in Lean.<n>It combines dynamic validation, automated proofs, and interactive proof scripting in one foundational framework.<n>We evaluate LeetProof on benchmarks derived from prior work on certified synthesis.
  arXiv  Detail & Related papers  (2026-04-17T14:56:45Z)
• VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications [0.3240750198587795]
  We compare classical and prompt-based approaches for automated JML specification synthesis.<n>We investigate whether prompt optimization can push synthesis quality further by evolving prompts through structured verification feedback.<n>We propose VeriAct, a verification-guided agentic framework that iteratively synthesizes and repairs specifications.
  arXiv  Detail & Related papers  (2026-03-31T22:12:15Z)
• Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications [12.783777562919383]
  Formal verification of memory-manipulating programs critically depends on precise function specifications that capture memory states written by experts.<n>We propose a neuro-symbolic framework for automatically generating memory-aware formal function specifications for C programs.<n>We introduce LeetCode-C-Spec, a new benchmark of 200 C programming problems for generating memory-aware formal function specifications.
  arXiv  Detail & Related papers  (2026-03-12T15:02:26Z)
• CVeDRL: An Efficient Code Verifier via Difficulty-aware Reinforcement Learning [57.24524263804788]
  Code verifiers play a critical role in post-verification for LLM-based code generation.<n>Existing supervised fine-tuning methods suffer from data scarcity, high failure rates, and poor inference efficiency.<n>We show that naive RL with only functionality rewards fails to generate effective unit tests for difficult branches and samples.
  arXiv  Detail & Related papers  (2026-01-30T10:33:29Z)
• CoT-Saliency: Unified Chain-of-Thought Reasoning for Heterogeneous Saliency Tasks [96.64597365827046]
  We present the first unified framework that jointly handles three operationally heterogeneous saliency tasks.<n>We introduce a Chain-of-Thought (CoT) reasoning process in a Vision-Language Model (VLM) to bridge task heterogeneity.<n>We show our model matches or outperforms specialized SOTA methods and strong closed-source VLMs across all tasks.
  arXiv  Detail & Related papers  (2025-11-01T04:37:01Z)
• EvoSyn: Generalizable Evolutionary Data Synthesis for Verifiable Learning [63.03672166010434]
  We introduce an evolutionary, task-agnostic, strategy-guided, executably-checkable data synthesis framework.<n>It jointly synthesizes problems, diverse candidate solutions, and verification artifacts.<n>It iteratively discovers strategies via a consistency-based evaluator that enforces agreement between human-annotated and strategy-induced checks.
  arXiv  Detail & Related papers  (2025-10-20T11:56:35Z)
• You only need 4 extra tokens: Synergistic Test-time Adaptation for LLMs [50.54173262572369]
  Large language models (LLMs) are increasingly deployed in specialized domains such as finance, medicine, and agriculture.<n>We study label-free test-time adaptation for language models and present SyTTA, an inference-time framework that adapts models on-the-fly without additional supervision.
  arXiv  Detail & Related papers  (2025-10-11T14:00:39Z)
• Hybrid Reinforcement: When Reward Is Sparse, It's Better to Be Dense [36.71358559780692]
  HERO is a reinforcement learning framework that integrates verifier signals with reward-model scores in a structured way.<n> HERO consistently outperforms RM-only and verifier-only baselines, with strong gains on both verifiable and hard-to-verify tasks.
  arXiv  Detail & Related papers  (2025-10-08T17:09:41Z)
• 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)
• VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
  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%.
  arXiv  Detail & Related papers  (2025-05-25T19:00:52Z)
• Foreseeing the Benefits of Incidental Supervision [83.08441990812636]
  This paper studies whether we can, in a single framework, quantify the benefits of various types of incidental signals for a given target task without going through experiments. We propose a unified PAC-Bayesian motivated informativeness measure, PABI, that characterizes the uncertainty reduction provided by incidental supervision signals.
  arXiv  Detail & Related papers  (2020-06-09T20:59:42Z)

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.