Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs

• URL: http://arxiv.org/abs/2603.15510v1
• Date: Mon, 16 Mar 2026 16:37:38 GMT
• Title: Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs
• Abstract summary: Wonda is a pipeline that refines noisy data via AST-based normalization, followed by semantic rewriting and augmentation with provable quality guarantees.<n>We demonstrate that fine-tuning Small Language Models (SLMs) on this curated dataset result in consistent and significant performance gain.
• Score: 6.863007247776099
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The synthesis of inductive loop invariants is a critical bottleneck in automated program verification. While Large Language Models (LLMs) show promise in mitigating this issue, they often fail on hard instances, generating invariants that are invalid or computationally ineffective. While fine-tuning is a natural route to mitigate this limitation, obtaining high-quality training data for invariant generation remains an open challenge. We present a rigorous data curation pipeline designed to extract high-quality training signals from raw verifier-generated invariants. First, we formalize the properties required for a high-quality training invariant. Second, we propose Wonda, a pipeline that refines noisy data via AST-based normalization, followed by LLM-driven semantic rewriting and augmentation with provable quality guarantees. We demonstrate that fine-tuning Small Language Models (SLMs) on this curated dataset result in consistent and significant performance gain. In particular, a fine-tuned 4B parameter model matches the utility of a GPT-OSS-120B baseline and approaches the state-of-the-art GPT-5.2, without incurring reasoning-time overhead. On challenging instances from the recent InvBench evaluation suite, our approach doubles the invariant correctness and speedup rates of base models; and improves their Virtual Best Performance (VBP) rates on the verification task by up to 14.2%.

Related papers

• 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)
• 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)
• Training LLMs for Multi-Step Tool Orchestration with Constrained Data Synthesis and Graduated Rewards [76.49428173793386]
  LLMs must invoke multiple dependent APIs in the correct order while propagating intermediate outputs.<n>Training models to handle such faces two obstacles: existing environments focus on simple per-turn function calls with simulated data, and binary rewards.<n>We present a framework addressing both challenges. First, we construct a reinforcement learning environment backed by a large-scale cache of real API responses, enabling a data synthesis pipeline that samples valid multi-step orchestration traces.<n>Second, we propose a graduated reward design that decomposes correctness into atomic validity and orchestration.
  arXiv  Detail & Related papers  (2026-03-25T18:31:39Z)
• Benchmarking Few-shot Transferability of Pre-trained Models with Improved Evaluation Protocols [123.73663884421272]
  Few-shot transfer has been revolutionized by stronger pre-trained models and improved adaptation algorithms.<n>We establish FEWTRANS, a comprehensive benchmark containing 10 diverse datasets.<n>By releasing FEWTRANS, we aim to provide a rigorous "ruler" to streamline reproducible advances in few-shot transfer learning research.
  arXiv  Detail & Related papers  (2026-02-28T05:41:57Z)
• InstructDiff: Domain-Adaptive Data Selection via Differential Entropy for Efficient LLM Fine-Tuning [35.89674702985539]
  InstructDiff is a unified framework that operationalizes differential entropy as a domain-adaptive selection criterion.<n>We show that InstructDiff achieves 17% relative improvement over full data training on mathematical reasoning and 52% for general instruction-following.
  arXiv  Detail & Related papers  (2026-01-30T14:15:44Z)
• Winning the Pruning Gamble: A Unified Approach to Joint Sample and Token Pruning for Efficient Supervised Fine-Tuning [71.30276778807068]
  We propose a unified framework that strategically coordinates sample pruning and token pruning.<n>Q-Tuning achieves a +38% average improvement over the full-data SFT baseline using only 12.5% of the original training data.
  arXiv  Detail & Related papers  (2025-09-28T13:27:38Z)
• Uncertainty Aware Learning for Language Model Alignment [97.36361196793929]
  We propose uncertainty-aware learning (UAL) to improve the model alignment of different task scenarios. We implement UAL in a simple fashion -- adaptively setting the label smoothing value of training according to the uncertainty of individual samples. Experiments on widely used benchmarks demonstrate that our UAL significantly and consistently outperforms standard supervised fine-tuning.
  arXiv  Detail & Related papers  (2024-06-07T11:37:45Z)
• Adversarial Fine-Tuning of Language Models: An Iterative Optimisation Approach for the Generation and Detection of Problematic Content [0.0]
  We tackle the emerging challenge of unintended harmful content generation in Large Language Models (LLMs) Our two-pronged approach employs an adversarial model, fine-tuned to generate potentially harmful prompts, and a judge model, iteratively optimised to discern these prompts. We show that a rudimentary model textttada can achieve 13% higher accuracy on the hold-out test set than GPT-4 after only a few rounds of this process.
  arXiv  Detail & Related papers  (2023-08-26T05:20:58Z)
• Constraining Generative Models for Engineering Design with Negative Data [11.432911164773488]
  We introduce a novel training method to guide a generative model toward constraint-satisfying outputs.<n>Our negative-data generative model (NDGM) formulation easily outperforms classic models.
  arXiv  Detail & Related papers  (2023-06-27T02:47:59Z)
• PTP: Boosting Stability and Performance of Prompt Tuning with Perturbation-Based Regularizer [94.23904400441957]
  We introduce perturbation-based regularizers, which can smooth the loss landscape, into prompt tuning. We design two kinds of perturbation-based regularizers, including random-noise-based and adversarial-based. Our new algorithms improve the state-of-the-art prompt tuning methods by 1.94% and 2.34% on SuperGLUE and FewGLUE benchmarks, respectively.
  arXiv  Detail & Related papers  (2023-05-03T20:30:51Z)
• Conditional Denoising Diffusion for Sequential Recommendation [62.127862728308045]
  Two prominent generative models, Generative Adversarial Networks (GANs) and Variational AutoEncoders (VAEs) GANs suffer from unstable optimization, while VAEs are prone to posterior collapse and over-smoothed generations. We present a conditional denoising diffusion model, which includes a sequence encoder, a cross-attentive denoising decoder, and a step-wise diffuser.
  arXiv  Detail & Related papers  (2023-04-22T15:32:59Z)
• Training Discrete Deep Generative Models via Gapped Straight-Through Estimator [72.71398034617607]
  We propose a Gapped Straight-Through ( GST) estimator to reduce the variance without incurring resampling overhead. This estimator is inspired by the essential properties of Straight-Through Gumbel-Softmax. Experiments demonstrate that the proposed GST estimator enjoys better performance compared to strong baselines on two discrete deep generative modeling tasks.
  arXiv  Detail & Related papers  (2022-06-15T01:46:05Z)

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.