HOLogicBench：评估 LLM 高阶逻辑推理能力的新基准

HOLogicBench 是一个包含 1,379 个实例的基准，用 Isabelle/HOL 形式化并验证答案，系统评估 LLM 的五类高阶推理操作。16 种模型配置平均准确率 53.86%，最佳配置达 65.99%。分析显示 LLM 生成的推理与有效推导对齐有限，易受最小反事实扰动影响，且不同高阶推理类型呈现不同失败模式。