[2026年7月30日提交]

查看PDF HTML（实验性）

摘要：使用LLM代理实现程序验证的自动化，需要生成规约、注解、辅助引理和工具调用，所有这些都依赖于可复用的技能。一个自然的解决方案是技能自进化：从轨迹中提炼技能，并通过反馈进行精炼。然而，现有的进化方法在处理程序验证任务时遇到困难，因为它们无法可靠地识别特定技能的失败，也无法从不透明的验证器反馈中提取可操作的信号。在本文中，我们提出VeriSkill，一个专为程序验证构建的自进化框架。它将验证失败归因于技能缺陷，将诊断特征提炼为可复用的经验教训，并迭代地精炼候选技能，仅接受那些既能提升验证性能又能保持程序语义的修改。实验表明，VeriSkill在多个验证工具、代理框架和LLM后端上持续优于所有基线。

提交历史

来自：Changguo Jia [查看邮箱]
[v1] 2026年7月30日 星期四 06:15:29 UTC (395 KB)