INDUCTION: Finite-Structure Concept Synthesis in First-Order Logic

TL;DR

INDUCTION is a benchmark for evaluating the synthesis of finite-structure concepts in first-order logic, highlighting challenges in formula generalization and the impact of formula bloat across different regimes.

Contribution

This paper introduces INDUCTION, a novel benchmark for finite-structure concept synthesis in first-order logic, with diverse regimes and analysis of model behaviors.

Findings

Low bloat formulas generalize better.

Sharp difficulty gradients observed across tasks.

Different models exhibit distinct generalization strategies.

Abstract

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.