AxDafny

深度分析

AxDafny：結合 AI 程式生成與 Dafny 形式驗證的迭代框架

本報導介紹 AxDafny，一個以 Dafny 為平台、透過驗證回饋迭代修正的程式與證明自動生成框架。研究同時發布 LCB‑Pro‑Dafny 基準，涵蓋 250 題競賽式問題，測試模型在程式合成與證明合成上的表現。