[Submitted on 30 Jul 2026]

View PDF HTML (experimental)

Abstract:利用大型語言模型代理進行程式驗證自動化，需要生成規格、註解、輔助引理以及工具呼叫，而這些都仰賴可重複使用的技能。自然而然的解決方案是技能自演化：從軌跡中萃取技能，並透過回饋進行精煉。然而，現有的演化方法在程式驗證任務上遇到困難，因為它們無法可靠地辨識特定技能的失敗，也無法從不透明的驗證器回饋中萃取可行的訊號。在本文中，我們提出 VeriSkill，一個專為程式驗證打造的自演化框架。它將驗證失敗歸因於技能缺陷、將診斷特徵提煉成可重複使用的經驗，並迭代地精煉候選技能，僅接受那些能提升驗證效能且同時保留程式語意的修正。實驗結果顯示，VeriSkill 在多種驗證工具、代理框架以及大型語言模型後端上， consistently 優於所有基線方法。

Submission history

From: Changguo Jia [view email]
[v1] Thu, 30 Jul 2026 06:15:29 UTC (395 KB)