提出首个一阶逻辑概念合成基准,评估模型在有限结构中统一解释目标谓词的能力。
INDUCTION: Finite-Structure Concept Synthesis in First-Order Logic
- 设计三类观测场景,通过精确模型检验验证逻辑公式的正确性
- 发现低复杂度公式在未见世界上的泛化能力显著更强
- 揭示先进模型在不同任务中存在截然不同的概念泛化策略
我们提出INDUCTION,一个面向一阶逻辑中有限结构概念合成的基准。给定带有扩展性标签的目标谓词的小型关系世界,模型需输出一个单一的一阶逻辑公式,在所有世界中统一解释目标,且通过精确模型检查验证正确性。该基准包含三种情形:FullObs(全观测)、CI(对比)和EC(存在完成),并惩罚公式冗余。实验发现显著的难度梯度、持续困难的结构性类别,且低冗余公式在未见世界上的泛化表现远超高冗余公式。顶尖近期模型在不同任务和指标上表现出质的不同行为,暗示其概念泛化策略存在差异。
原文摘要 · Abstract (English)
We introduce INDUCTION, a benchmark for finite structure concept synthesis in first order logic. Given small finite relational worlds with extensionally labeled target predicates, models must output a single first order logical formula that explains the target uniformly across worlds, with correctness verified via exact model checking. The benchmark includes three regimes, FullObs, CI (contrastive), and EC (existential completion), nd penalizes formula bloat. We find sharp difficulty gradients, persistent hard structural families, and observe that low bloat formulas generalize far better on held out worlds. Elite recent models show qualitatively different behaviors across tasks and performance metrics, hinting to their different strategies of concept generalization.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。