VeriSkill：程序验证技能的自进化框架

用LLM智能体实现程序验证自动化，需要生成规范、标注、辅助引理和工具调用，而这一切都依赖可复用的技能。一个自然的对策是技能自进化：从轨迹中蒸馏技能并通过反馈加以改进。然而，现有进化方法在程序验证任务上表现不佳，因为它们无法可靠地识别技能特定的失败，也难以从晦涩的验证器反馈中提取可操作的信号。本文提出VeriSkill，一个专为程序验证构建的自进化框架。它将验证失败归因于技能缺陷，把诊断特征蒸馏为可复用的经验教训，并迭代改进候选技能，只接受那些在保持程序语义的同时提升验证性能的修订。实验表明，VeriSkill在多种验证工具、智能体框架与LLM后端上一致优于所有基线。