为什么重要
ProofWriter 要求模型不仅给出正确答案，还必须生成完整的推理证明。通过控制推理深度（1-5 步）和开放世界假设（CWA vs OWA），可以精确诊断模型在不同推理复杂度下的失败模式。
构建方式
使用逻辑引擎自动生成事实集 + 规则集 + 推理问题 + 证明。深度从 0-hop 到 5-hop 递增。引入 “Unknown” 标签处理开放世界假设下不可证明的命题。
任务示例
- 事实：“Anne is blue. Anne is nice.”
- 规则：“If something is blue and nice, then it is smart.”
- 问题：“Is Anne smart?” → 答案：True
- 证明：Anne is blue [fact] + Anne is nice [fact] → Anne is smart [rule 1]
关键发现
- 推理深度 >3 步后准确率急剧下降
- 证明生成比答案判断难得多——模型可能猜对答案但证明错误
- 否定推理和开放世界假设是最大挑战
关联基准
FOLIO（一阶逻辑）、bAbI（基础推理）、EntailmentBank（解释推理）
不足与展望
合成数据的语言极度简化。规则推理与自然语言推理之间存在较大鸿沟。