DeFAb: A Verifiable Benchmark for Defeasible Abduction in AI

•DeFAb 將數十年來公共資助的知識庫（如 OpenCyc、YAGO、Wikidata 等分類層次結構，以及 ConceptNet、UMLS 等行為屬性圖）轉換為可廢止溯因推理的正式基礎實例，旨在透過推翻預設值同時保留不相關的預期來建構解釋異常的假設。
•該基準測試包含「渲染穩健性評估」，其中模型在不同表面渲染下進行測試時，其準確度顯著下降（例如，對於第二級別，準確度降至 7.8% 至 23.5%），這突顯了模型對呈現方式的敏感性。
•DeFAb 進一步發布了 DeFAb-Hard，這是一個包含 235 個第三級別難度實例的變體，其中最佳模型僅達到 53.3% 的準確度，而符號求解器則達到 100%；同時還引入了 CONJURE，這是一個經過核心驗證的變革性創造力變體，包含 560 個 Lean 4/Mathlib 實例。
•DeFAb 提供的驗證器可用作偏好優化（如直接偏好優化 DPO 和可驗證獎勵強化學習 RLVR/GRPO）的精確獎勵訊號，這對於大型語言模型 (LLM) 的對齊至關重要。

📊 競品分析▸ Show

基準測試名稱	評估重點	模態	關鍵發現/挑戰
DeFAb	可廢止溯因推理、形式邏輯嚴謹性、理論修正	文本/符號邏輯	頂尖模型在邏輯嚴謹性上表現不佳，渲染穩健性評估準確率最低僅 7.8%；符號求解器可達 100% 準確度。
αNLI (Abductive NLI)	溯因常識推理、選擇最合理解釋	文本	2020 年，人類準確度為 91.4%，最佳模型為 68.9%，存在 22.5% 的差距；LLM 在溯因和歸納推理上表現顯著不均。
BlackSwanSuite	視覺語言模型 (VLM) 在不可預測事件中的溯因與可廢止推理	影片/視覺與文本	評估 VLM 在異常事件中的推理能力，發現與人類表現存在高達 32% 的顯著差距。
InAbHyD	LLM 的歸納與溯因推理、奧卡姆剃刀原則	文本/符號邏輯	LLM 在簡單情境下表現良好，但在複雜世界模型和生成高品質假設方面表現不佳，即使使用推理增強技術也無顯著改善。
LogicSkills	形式符號化等核心邏輯技能	文本/符號邏輯	旨在分離和評估 LLM 掌握的核心邏輯技能。
FormalMATH	形式數學推理	文本/符號邏輯 (Lean4)	頂尖 LLM 在奧林匹亞級別和大學級別的數學問題上成功率僅為 16.46%，顯示出顯著的領域偏差。
DafnyBench	形式軟體驗證	程式碼/形式規範	LLM 在需要多步驟推理或實施中間引理的複雜證明中表現不佳。

DeFAb 的生成管道結合了分類層次結構（如 OpenCyc、YAGO、Wikidata）與行為屬性圖（如 ConceptNet、UMLS）。
該基準測試從 18 個來源生成了超過 372,648 個實例，包含 33.75 百萬條具體化規則。
實例分為三個難度級別，並具有多項式時間可驗證的黃金標準答案。
每個假設都必須通過多項式時間檢查，以確保其推導有效性、保守性和最小性。
一個基於規則的邏輯求解器能在 50 微秒內以 100% 的準確度解決每個實例。
DeFAb 還發布了 CONJURE，這是一個經過核心驗證的變革性創造力變體，包含 560 個 Lean 4/Mathlib 實例，其黃金答案是證明核心先前未包含的定義。

基礎模型需要根本性的架構變革以內化複雜邏輯推理。

現有模型在 DeFAb 基準測試中表現出顯著的性能差距和對呈現方式的敏感性，表明僅靠數據暴露不足以解決其邏輯推理的根本性挑戰。

DeFAb 等基準測試將加速更穩健和可驗證 AI 系統的開發。

透過提供精確、可驗證的獎勵訊號，DeFAb 能更有效地進行偏好優化和針對邏輯嚴謹性的訓練，從而推動 AI 能力的提升。

形式邏輯和符號方法與大型語言模型的整合將成為實現高級 AI 推理的關鍵。

符號求解器在 DeFAb 實例上達到 100% 的準確度，這突顯了與 LLM 之間的持續差距，並暗示了神經符號方法在彌合這一差距方面的潛力。

1980年代初期

人工智慧領域出現非單調推理（與可廢止推理相關）的早期系統，如 Reiter 的預設邏輯。

1994

Donald Nute 在一篇開創性論文中引入了可廢止邏輯 (Defeasible Logic)。

2002

DeFAb 使用的知識庫之一 OpenCyc 首次發布。

2019-12

ART (Abductive Reasoning in Text) 數據集被引入，用於溯因常識推理，並揭示了大型語言模型在此類任務上的不足。

2024-12

BlackSwanSuite 基準測試被引入，用於評估視覺語言模型在不可預測影片事件中的溯因和可廢止推理能力。

2026-06-18

DeFAb：用於 AI 可廢止溯因推理的驗證基準被引入，旨在測試基礎模型在形式邏輯和理論推理方面的能力。

DeFAb：用於 AI 可廢止溯因推理的驗證基準