为什么重要
FOLIO 是少有的将形式逻辑（一阶逻辑）与自然语言推理严格对齐的基准。每个样本都有对应的 FOL 公式和自然语言版本，可以用定理证明器验证正确性。这使其成为精确评测 LLM 逻辑推理能力（而非模式匹配）的金标准。
构建方式
专家手工编写自然语言前提和结论，同时写出对应的一阶逻辑公式。使用 Prover9 定理证明器验证标注的正确性。三分类标签：True / False / Unknown。
任务示例
- 前提：“All birds can fly. Penguins are birds. Penguins cannot fly.”
- 结论：“There exists something that is a bird and cannot fly.”
- FOL: ∀x(Bird(x)→Fly(x)), Bird(penguin), ¬Fly(penguin) ⊢ ∃x(Bird(x)∧¬Fly(x))
- 标签：True（但前提集矛盾）
关键发现
- 即使是 GPT-4 在该基准上也远低于定理证明器，说明 LLM 的”推理”仍有本质局限
- Unknown 类别最难判断——模型倾向于过度推断
- 形式化验证可以精确定位推理失败点
关联基准
LogiQA（逻辑选择题）、ProofWriter（规则推理）、CLUTRR（组合推理）
不足与展望
规模较小，覆盖的逻辑模式有限。FOL 表达能力不足以捕捉所有自然语言推理现象。