研究者らは、基盤モデルにおける可敗北的アブダクション（defeasible abduction）の能力を評価するための検証可能なベンチマーク「DeFAb（Defeasible Abduction Benchmark）」を発表しました。可敗北的アブダクションとは、デフォルトルールを上書きしながら無関係な期待を保持することで、異常を説明する仮説を構築する高度な推論プロセスです。DeFAbは、40年にわたる公的資金による知識ベースを形式化されたインスタンスに変換し、各仮説が多項式時間で検証可能な導出、保守性、最小性のチェックを通過することを要求します。これにより、論理的厳密性が創造性と理論的推論を測定するための道具となり、流暢だが理論を破壊する散文ではなく、規律ある理論修正の構築を評価します。
DeFAbの生成パイプラインは、分類階層（OpenCyc、YAGO、Wikidata）と行動特性グラフ（ConceptNet、UMLS）を組み合わせ、18のソースから3375万の具体化ルールを生成し、3つの難易度レベルにわたる372,648以上のインスタンスを生産します。各インスタンスには多項式時間で検証可能なゴールドスタンダードが付属し、評価の信頼性を確保します。
実験結果は、ルールベースの論理ソルバーが50マイクロ秒未満で100%の精度で全インスタンスを解決できる一方、最良のフロンティア言語モデルは標準評価で65%に達するものの、ロバストレンダリング評価（4種類の表面レンダリングの最悪ケース）では23.5%に低下することを示しています。4つのフロンティアモデルは可敗北的推論を確実に内部化できず、ロバスト評価におけるレベル2の精度は7.8%から23.5%の範囲にとどまりました。チェーン・オブ・ソートのばらつき（約36パーセントポイント）はモデル間の差を上回り、マッチングによる汚染制御ではレベル3で19.4パーセントポイントの隔たりが確認されました。
研究チームはさらに、235インスタンスからなるレベル3の難易度バリアント「DeFAb-Hard」と、Lean 4/Mathlibに基づくカーネル検証型創造的推論バリアント「CONJURE」も公開しました。CONJUREは560インスタンスから成り、ゴールドアンサーは証明カーネルが以前に含んでいなかった定義であり、判定者不要の検証器を使用します。パイロット実験では新規概念は発見されませんでした。
この検証器は、優先最適化（DPO、RLVR/GRPO）のための正確な報酬としても機能します。DeFAbはMITライセンスの下で公開され、Hugging Faceから入手可能であり、AI研究コミュニティにモデルの推論能力を評価・改善するための貴重なリソースを提供します。