INDUCTION: Finite-Structure Concept Synthesis in First-Order Logic
Serafim Batzoglou
cs.AI
2026-02-22
INDUCTION: emit one FOL formula that explains a labeled concept across finite worlds. Grok 4 leads FullObs at 50.7%; bloated formulas fall from ~90% to ~20% held-out match.
Most logic benchmarks test deduction: the rules are given, and the system has to derive consequences. INDUCTION tests the inverse. A solver sees a handful of finite relational worlds plus object-level labels for an unknown unary concept, and must emit one first-order formula that accounts for those labels in every world.
Finite domains make the output checkable. Quantifiers are grounded, the formula becomes a Boolean circuit, and Z3 checks consistency. Natural-language interpretation is not in the loop. The hard part is uniqueness. Finite evidence usually admits many formulas. Some recover the planted concept. Others case-split on accidents of the input worlds. Scoring only validity mixes those two.
The signature is tiny and fixed: unary P, Q and binary R, S. Each world is a finite structure with a labeled positive set T. The output must have exactly one free variable x, written as a Lisp-style S-expression. The same formula is evaluated in every world. Per-world formulas are not allowed.
Three regimes share that interface:
The generator draws gold formulas from a pool of roughly 200 structural templates, then builds worlds against a frozen pool of about 1,500 distractors so that each new world kills at least one surviving shortcut. Instances solvable by an atomic formula, a proper subformula of the gold, or a quantifier-free combination are rejected. Scoring reports unbounded accuracy and Acc@gold+Δ, which also caps AST size relative to the planted gold. Bloat rate is the share of successful formulas more than 25 AST nodes above gold.
No prompted model wins all three tasks.
| Model | FullObs Acc / @+25 | CI Acc / @+25 | EC valid / @+25 |
| Grok4 | 50.7% / 46.7% | 78.0% / 75.5% | 53.0% / 53.0% |
| GPT-5.4 | 43.5% / 32.0% | 79.0% / 76.0% | 93.5% / 64.0% |
| GPT-5.2 | 43.7% / 19.5% | 82.5% / 73.0% | 78.0% / 59.5% |
| Gemini 3.5 Flash | 34.4% / 33.9% | 78.5% / 78.0% | 51.5% / 51.0% |
Grok4 leads FullObs, but coverage is only 89.3%. GPT-5.2 hits 100% on the simple band and 89.0% on easy, then falls to 29.0% / 21.0% / 0% on medium / hard / extreme. GPT-5.4 scores 39.0% / 25.0% / 8.0% on those three; Grok4 scores 43.0% / 39.0% / 16.0%. GPT-4o is 0% on FullObs.
Symbolic baselines do not collapse the suite either. The unified SMT search (z3-prenex + rescue) reaches 48.8% FullObs, 82.0% CI, and 100% EC. A FullObs-specific Z3 portfolio, z3-ad-mix, reaches 65.9%. A restricted ILP/ASP fragment, ilasp-frag, is at 15.7% FullObs.
Bloat is the sharper split. GPT-5.2's unbounded FullObs accuracy is 43.7%, but Acc@gold+25 is only 19.5%, with 24.3% bloat. GPT-5.4 is almost identical unbounded (43.5%), yet 32.0% budgeted, with bloat down to 11.5%. Gemini 3.5 Flash's bloat is 0.5%.
On five held-out worlds drawn from the same generator, near-gold formulas (AST at most gold+1) match 77.3%–97.6% of the time; formulas above gold drop to 6.7%–73.3%. GPT-5.4 falls from 92.6% to 24.8%, GPT-5.2 from 88.7% to 15.9%. On the same problem, compact formulas hold at 87.1% held-out match versus 11.8% for bloated ones, and the compact side wins on 92% of those problems.
A recurring structural error is collapsing "every R-successor satisfies a property" into "there exists a neighbor." In EC, purely existential gold formulas are far easier than mixed existential/universal ones: GPT-5.2's Acc@gold+25 drops from 93.2% to 25.3%.
For people who build reasoning evals, this is a mechanically checkable induction test that separates fitting the given worlds from recovering a stable concept. Compactness is not an aesthetic preference here. Held-out exact match moves by tens of points.
For agent and neuro-symbolic work, the suite is a usable regression set. Universal relational generalization, lift-hard patterns (a relation on the free variable x sitting inside a universal quantifier), and case-splitting bloat are the failure modes that keep recurring. Code and the v1 data are public.
This is not a general first-order reasoning scoreboard. The signature is small, domains are tiny, and gold formulas come from a template library. It measures concept synthesis under those controls.
The authors bound the scope themselves: no functions, constants, arithmetic, types, or background theories, and domains of a few to a dozen elements. The planted gold is not a claim of global syntactic minimality. Many inequivalent formulas can agree on the finite input worlds. EC's existential-completion semantics is permissive; large disjunctions can sometimes exploit the unknown atoms. Symbolic rows are 30-minute bounded searches, not upper bounds. Prompts were not tuned per model, and there is no systematic compactness-prompt ablation.
Raw CI accuracy runs higher than FullObs, in part because the generator leaves YES worlds easier to satisfy with simple formulas and then uses NO worlds to kill shortcuts. An 80% CI score is not evidence that the intended concept was recovered: even among instance-correct near-gold formulas, held-out YES exact match sits around 7%–17%.