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

First-order concept synthesis asks a system to infer one formula that classifies labeled objects consistently across several finite relational structures. Every candidate can be evaluated exactly, but quantified first-order formulas form a vast search space, and LLM outputs are often semantically promising without being fully correct. We introduce Hypothesis Frontier, a verifier-guided neurosymbolic framework that evaluates each LLM formula on every training object, retains the strongest verified hypothesis across rounds, and uses its remaining errors to guide subsequent generation. Symbolic processing repairs invalid formulas while remaining anchored to the LLM-generated hypothesis, and simplifies train-valid formulas without changing any training prediction. Under matched models, problem sets, and LLM-round budgets, Hypothesis Frontier solves substantially more problems than repeated original-prompt generation. After the final formulas are selected, exact simplification shortens many train-valid formulas while preserving every training prediction. Exact symbolic reasoning therefore helps both to solve more induction problems and to compress many of the resulting formulas.

Logical rule induction seeks interpretable rules that transfer across propositional schemas. This requires respecting symmetries: atom naming, example order, polarity flips, and label swap. Enforcing exact symmetry by construction lets one trained inducer scale beyond its training schemas. Our central contribution is a canonical export that decodes a discrete rule from literal scores. It needs no retraining and is exactly equivariant whenever those scores respect the symmetries. We instantiate it on the Neural Rule Inducer, a disjunctive-normal-form (DNF) foundation model that natively respects only example order. We restore the remaining symmetries through architecture, inference, and training. On synthetic stress tests, accuracy on the support labels stays stable at much larger schemas, and rule fidelity on fresh inputs remains above the unmodified model. On real data, accuracy improves most on larger schemas. The exported rule is exact on synthetic full-group tests and on schema-valid real-data tests. This is a mathematical property of the export rather than of a specific model, and we validate it empirically only on the NRI. Enforcing symmetry by construction turns this small-data pretrained model into a reusable, interpretable inducer that transfers to larger schemas.

We introduce ABD, a benchmark for default-exception abduction over finite first-order worlds. Given a background theory with an abnormality predicate and a set of relational structures, a model must output a first-order formula that defines exceptions, restoring satisfiability while keeping exceptions sparse. We formalize three observation regimes (closed-world, existential completion, universal completion) with exact SMT verification. Evaluating ten frontier LLMs on 600 instances, the best models achieve high validity but parsimony gaps remain, and holdout evaluation reveals distinct generalization failure modes across regimes.