VeriSkill: A Self-Evolution Framework for Program Verification Skills

• URL: http://arxiv.org/abs/2607.27733v1
• Date: Thu, 30 Jul 2026 06:15:29 GMT
• Title: VeriSkill: A Self-Evolution Framework for Program Verification Skills
• Abstract summary: We propose VeriSkill, a self-evolution framework for program verification.<n>It attributes verification failures to skill deficiencies, distills diagnostic signatures into reusable lessons, and iteratively refines candidate skills.
• Score: 19.114016708981023
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automating program verification with LLM agents requires generating specifications, annotations, auxiliary lemmas, and tool invocations, all of which depend on reusable skills. A natural remedy is skill self-evolution: distilling skills from trajectories and refining them through feedback. However, existing evolution methods struggle with program verification tasks because they cannot reliably identify skill-specific failures or extract actionable signals from opaque verifier feedback. In this paper, we propose VeriSkill, a self-evolution framework built for program verification. It attributes verification failures to skill deficiencies, distills diagnostic signatures into reusable lessons, and iteratively refines candidate skills, admitting only revisions that improve verification performance while preserving program semantics. Experiments show that VeriSkill consistently outperforms all baselines across multiple verification tools, agent frameworks, and LLM backends.

Related papers

• Evo-Harness: Context-to-Harness Skill Compilation for Self-Evolving Agents [67.97365535829098]
  Learning from experience is critical for developing capable, self-improving large language model (LLM) agents.<n>We propose Evo-Harness, which distills noisy, single-shot executions into reusable skill harnesses for cross-domain and topic-level adaptation.<n>Our analysis demonstrates the effectiveness of Evo-Harness and provides a principled understanding of how LLM agents can effectively learn on the fly.
  arXiv  Detail & Related papers  (2026-08-15T06:43:56Z)
• Skill Self-Play: Pushing the Frontier of LLM Capability with Co-Evolving Skills [53.15216425100295]
  We introduce Skill Self-Play (Skill-SP), a co-evolutionary framework comprising a proposer, a solver, and a skill controller.<n>The proposer generates challenging tasks conditioned on dynamically sampled skills; the solver explores candidate solutions to push its capability boundaries; and the skill controller collects execution feedback to update and expand the skill library.<n>This interactive co-evolution effectively bridges the gap between structured verification and open-ended exploration.
  arXiv  Detail & Related papers  (2026-07-24T17:59:22Z)
• AEVAL: From Anecdotal to Deterministic Testing for Agentic Skill Workflows [1.6785141970297952]
  AEVAL (Agentic Evaluation) is a CI-integrated framework that replaces this practice with a deterministic, reproducible test pipeline for agentic skills.<n>Every skill change triggers a test event: the skill runs against a developer declared evaluation contract inside an automated executor.<n>A key ingredient is a structural separation between executor and grader, preventing a subtle but pervasive failure mode.
  arXiv  Detail & Related papers  (2026-07-16T21:33:05Z)
• TTHE: Test-Time Harness Evolution [50.26245555541721]
  Existing approaches optimize such harnesses before deployment, searching training or development data for a fixed agent workflow that is then frozen at test time.<n>We ask whether the harness can instead be optimized during evaluation itself, using only the unlabeled execution traces the agent produces on the test inputs.<n>During evaluation, TTHE maintains a population of candidate harnesses and refines them through an agentic proposer that reasons over their execution traces.<n>A judge then commits an improved harness from execution-derived proxy signals, and the selected program persists to govern subsequent inputs.
  arXiv  Detail & Related papers  (2026-07-09T05:53:39Z)
• SkillCoach: Self-Evolving Rubrics for Evaluating and Enhancing Agentic Skill-Use [21.05387636058484]
  SkillCoach is a self-evolving framework for evaluating and enhancing agentic skill-use.<n>It derives skill-grounded process rubrics from real rollouts and evaluates trajectories along four dimensions.<n>It keeps the external verifier as a separate outcome signal, allowing process quality to be distinguished from accidental task success.
  arXiv  Detail & Related papers  (2026-07-02T08:28:51Z)
• SkillAudit: Ground-Truth-Free Skill Evolution via Paired Trajectory Auditing [81.51044612408793]
  SkillAudit is a framework for evolving agent skills without ground-truth feedback.<n>To turn behavioral differences into edit guidance, SkillAudit uses Process-Aligned Contrastive Evaluation.<n>It routes edits through two pipelines: Refine removes noisy or irrelevant guidance from broadly useful skills, while Repair replaces passages that conflict with the task.
  arXiv  Detail & Related papers  (2026-06-12T08:20:09Z)
• Socratic-SWE: Self-Evolving Coding Agents via Trace-Derived Agent Skills [12.442806027914097]
  We introduce Socratic-SWE, a closed-loop self-evolution framework that reuses the agent's historical solving traces as a source of training signal.<n>Rather than treating traces only as evidence for reward computation, Socratic-SWE distills them into structured agent skills that summarize recurring failures and effective repair patterns.
  arXiv  Detail & Related papers  (2026-06-05T16:00:17Z)
• VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
  We introduce VASO, a framework for verification-guided self-evolution of robot skill contracts.<n>VASO verifies logically inconsistent skill contracts, then verifies plans induced by the skill against global and local temporal specifications.<n>On Clearpath Jackal and PX4 quadcopter tasks, VASO reaches 97.2% formal-specification compliance using fewer than 100 optimization samples.
  arXiv  Detail & Related papers  (2026-06-03T20:02:35Z)
• SkillGrad: Optimizing Agent Skills Like Gradient Descent [30.781132643932338]
  Agent skills provide a lightweight way to adapt LLM agents to specialized domains by storing reusable procedural knowledge in structured files.<n>Existing skill-evolution methods often address these deficiencies through reflections without an explicit formulation.<n>We propose SkillGrad, a gradient-descent-inspired framework for optimizing agent skills.
  arXiv  Detail & Related papers  (2026-05-26T23:18:43Z)
• Trace2Skill: Verifier-Guided Skill Evolution for Long-Context EDA Agents [0.3733676450456031]
  We present Trace2Skill, a test-time scaling framework that improves a hardware agent without RTL-specialized model fine-tuning.<n>Rather than training a new model or only sampling more candidate solutions, Trace2Skill treats the agent's natural-language skill as an evolvable policy.<n>It mines repeated rollout traces for success and failure modes, converts them into dense diagnostics and oracle lessons, and uses an oracle, mutator, and selector loop to produce task-specific skills.
  arXiv  Detail & Related papers  (2026-05-20T23:10:49Z)
• ReVISE: Learning to Refine at Test-Time via Intrinsic Self-Verification [53.80183105328448]
  Refine via Intrinsic Self-Verification (ReVISE) is an efficient framework that enables LLMs to self-correct their outputs through self-verification.<n>Our experiments on various reasoning tasks demonstrate that ReVISE achieves efficient self-correction and significantly improves reasoning performance.
  arXiv  Detail & Related papers  (2025-02-20T13:50:02Z)

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.