让AI自动改进代码验证技能，提升可靠性。
VeriSkill: A Self-Evolution Framework for Program Verification Skills
- 通过诊断失败原因提炼可复用的验证经验
- 迭代优化技能，确保验证成功率提升且代码语义不变
- 适用于各类验证工具和大模型，通用性强
利用大语言模型代理自动化程序验证，需生成规范、注释、辅助引理和工具调用，这些均依赖可复用的技能。自然解决方案是技能自演化：从执行轨迹中提炼技能，并通过反馈进行优化。然而，现有演化方法在程序验证任务中表现不佳，因无法准确识别技能相关失败，也无法从模糊的验证器反馈中提取有效信号。本文提出VeriSkill，一个专为程序验证设计的自演化框架。该框架将验证失败归因于技能不足，将诊断特征提炼为可复用的经验，并迭代优化候选技能，仅保留能提升验证性能且不改变程序语义的修订。实验表明，VeriSkill在多个验证工具、代理框架和大模型后端上均持续优于所有基线。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。