INDUCTION: Finite-Structure Concept Synthesis in First-Order Logic
This work addresses the problem of concept synthesis in formal logic for AI researchers, though it appears incremental as it focuses on benchmarking rather than novel methods.
The authors introduced INDUCTION, a benchmark for synthesizing first-order logic formulas from finite relational worlds with labeled predicates, and found that low-bloat formulas generalize better on held-out worlds while revealing sharp difficulty gradients and persistent hard structural families.
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.