FVSpec：真實世界屬性測試作為 Lean 4 驗證挑戰
為何重要
這將為 AI 輔助正式軟體驗證提供具體的驗證標尺，有助於解決當代軟體日益複雜的合約式驗證需求。
FVSpec 是一個新推出的評估基準，旨在將 2,772 個真實 Python 倉庫中的屬性測試（PBTs）轉寫為 9,415 個包含 sorry 放置符的 Lean 4 規範。該研究建立了一個三智慧體 LLM 管線來處理依賴型程式設計與 Python 語義轉換之間的挑戰，並全面公開了相關程式碼與資料。
這將為 AI 輔助正式軟體驗證提供具體的驗證標尺，有助於解決當代軟體日益複雜的合約式驗證需求。
FVSpec 是一個新推出的評估基準，旨在將 2,772 個真實 Python 倉庫中的屬性測試（PBTs）轉寫為 9,415 個包含 sorry 放置符的 Lean 4 規範。該研究建立了一個三智慧體 LLM 管線來處理依賴型程式設計與 Python 語義轉換之間的挑戰，並全面公開了相關程式碼與資料。