深度分析
AxDafny：結合 AI 程式生成與 Dafny 形式驗證的迭代框架
本報導介紹 AxDafny，一個以 Dafny 為平台、透過驗證回饋迭代修正的程式與證明自動生成框架。研究同時發布 LCB‑Pro‑Dafny 基準，涵蓋 250 題競賽式問題，測試模型在程式合成與證明合成上的表現。
深度分析
本報導介紹 AxDafny，一個以 Dafny 為平台、透過驗證回饋迭代修正的程式與證明自動生成框架。研究同時發布 LCB‑Pro‑Dafny 基準，涵蓋 250 題競賽式問題，測試模型在程式合成與證明合成上的表現。
Dafny
本研究聚焦於以Dafny形式驗證Minimax系列搜尋演算法，涵蓋Alpha‑Beta剪枝與轉置表等優化手法。研究者為深度受限的兩種變體設計見證式正確性條件，並完成全部驗證與Python參考實作。此成果為遊戲人工智慧提供可驗證的基礎，減少實作錯誤與效能不確定性。