Hypothesis Frontier: Verifier Guided LLM and Symbolic Search for First-Order Induction

Hypothesis Frontier: Verifier-Guided LLM–Symbolic Search for First-Order Induction

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. The paper introduces 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.

The problem setting involves FullObs instances from the INDUCTION benchmark, containing finite relational worlds over the shared signature P, Q, R, S, =, with unary predicates P, Q and binary predicates R, S. Each world provides a finite domain, complete predicate interpretations, and a target extension. The task is to return one first-order formula with exactly one free variable, evaluated in every world. A formula is train-valid iff it matches every label in every training world. Because domains are finite, this condition can be evaluated exactly on every labeled object, yielding concrete false positives and false negatives.

The method works as follows. Each LLM proposal is parsed and evaluated on every training object. Unparseable outputs count as failures; parseable invalid formulas enter repair, train-valid formulas enter simplification, and every symbolic descendant is re-evaluated before retention. A deterministic train-only ranking selects the cumulative frontier. The recurrent pipeline is LLM proposal → exact verification → repair or simplification → frontier selection → next proposal; the next prompt contains the selected frontier and any remaining errors.

Repair combines three complementary candidate generators. A structural beam applies Boolean normalization and factoring, subtree deletion, quantifier-body pruning, constraint relaxation, and guards around formulas or existential witnesses. A selector generator scores compact conditions and their negations on every training object, producing restrictors and expansions that yield forms such as ϕ ∧ r, ϕ ∨ e, (ϕ ∧ r) ∨ e, and (ϕ ∨ e) ∧ r. A multi-term generator combines selectors into conjunctive or disjunctive patches. Every candidate is executed on all training objects; a descendant is retained only if it reaches train validity, lowers mismatch, or, at equal mismatch, is simpler.

Verified simplification applies only to train-valid formulas. From a train-valid formula, it generates parent-derived AST edits including Boolean deletion and factoring, quantifier pruning and merging, equality simplification, and reuse of existing subformulas. A candidate may replace the incumbent only if it produces exactly the same truth-value vector on every training pair and is smaller under a lexicographic complexity measure (AST size, then quantifier depth, then equality count). After the final frontier is chosen, a final exact pass shortens train-valid formulas while preserving their predictions on the training worlds.

Frontier selection ranks all direct proposals and parent-derived descendants seen through each round lexicographically, preferring evaluable, then parseable, then train-valid candidates, then minimizing mismatch count, AST size, quantifier depth, and equality count. Source and round do not affect the ranking. The winner becomes the cumulative frontier, preserving verified progress across calls. Later prompts repeat the full problem, retain the Round 1 formula as an anchor, and supply the current frontier with its validity, residual counts, AST size, quantifier depth, and misclassified objects. Trajectories contain at most six LLM calls.

The evaluation uses Benchmark300 (300 tasks) and Challenge64 (64 deliberately difficult tasks). Across matched model, task set, and LLM-round limits, Hypothesis Frontier outperforms repeated original-prompt generation in 9 of 9 comparisons by +6.2–+25.0 percentage points; 7 paired bootstrap intervals exclude zero. On Benchmark300, mean validity rises from 4.7% to 29.0% across configurations with complete trajectories; on Challenge64, from 29.9% to 59.4%. Repeated generation improves beyond Round 1 in 9 runs, yet Hypothesis Frontier uses fewer LLM calls in 9 comparisons.

The additional solutions do not come only from cases already close to a direct answer. Problems solved only by Hypothesis Frontier have larger Round 1 mismatch and a lower cross-fitted probability that repeated generation will succeed. On Benchmark300, the median Round 1 error is 32.1% among task–model cases solved only by Hypothesis Frontier, compared with 6.1% when both methods solve the task; the corresponding Challenge64 medians are 32.1% and 0.0%.

Within Hypothesis Frontier, both direct LLM generation and parent-derived repair produce first exact solutions. Later direct proposals are the largest direct source on Benchmark300, whereas Round 1 and later direct proposals account for most first solutions on Challenge64. Repair often advances the frontier before it solves a problem: across seven configurations with complete lineage records, it lowers mismatch on 83.1–98.4% of paired invalid proposals but reaches exact validity immediately on only 1.2–7.8%. Among 58 selected final train-valid formulas produced by repair, 40 (69%) had train-invalid parents.

The final exact simplifier finds a smaller formula in 461 of 1330 cases (34.7%) on Benchmark300, and 173 of 379 cases (45.6%) on Challenge64. Mean AST falls from 40.9 to 32.5 and from 128.3 to 98.4, respectively, while H-exact rises from 30.4% to 33.6% on Benchmark300 and from 18.9% to 20.0% on Challenge64. Paired world exactness usually remains unchanged. Every evaluated formula no larger than its planted reference is holdout-exact in both benchmark views, whereas the rate is at most 1.7% for formulas more than 25 nodes larger. Shorter formulas have a world-exactness advantage of +19.9 percentage points on Benchmark300 and +7.3 on Challenge64; when both formulas remain larger than the reference, the estimates are-1.5 points [-4.3, +1.5] and-3.3 points [-7.1, +1.6], neither excluding zero.

The paper also evaluates two LLM-free Z3 systems: z3-prenex + rescue (generic bounded prenex grammar) and z3-ad-mix (FullObs-specific schemas). Neither symbolic synthesis nor Hypothesis Frontier subsumes the other. In a symbolic-first workflow, running Z3 first and then applying Hypothesis Frontier only to unsolved problems raises final validity by 2.2–11.5 percentage points and reduces LLM calls by 8.3–46.6% relative to running Hypothesis Frontier on every problem. On the same remaining problems, Hypothesis Frontier exceeds repeated generation by 13.3–20.7 percentage points.

The paper makes three contributions: verifier-guided search over LLM formulas (evaluating each formula exactly, repairing its errors, keeping the strongest verified formula across calls, and using remaining errors to guide the next call); controlled comparisons and a symbolic-first workflow (Hypothesis Frontier outperforms repeated generation in every comparison, and running Z3 first solves additional problems and reduces LLM calls); and exact simplification and concept recovery (an exact simplifier shortens many train-valid formulas while preserving every training prediction and modestly improving overall holdout validity).

The results reveal three roles for symbolic reasoning: independent synthesis can solve problems before any LLM call, repair can develop an LLM-generated hypothesis during search, and exact simplification can shorten the final valid formula. Exact fit and shorter syntax, however, do not ensure concept recovery; most simplified formulas behave similarly on holdout worlds. The broader lesson is that an LLM formula need not already be correct to be useful: with exact feedback, it can become a hypothesis that symbolic methods test, repair, retain, and simplify.

Improvements to AI Systems:

1. Verifier-Guided Iterative Refinement Loop: Integrate an external exact verifier into the LLM generation loop. After each LLM proposal, evaluate it on all training data, retain the best-scoring hypothesis, and feed residual errors (false positives/negatives) back into the next prompt. This turns a single-shot generator into a closed-loop search that converges to correct solutions without requiring the LLM to be initially correct.

2. Symbolic Repair Module for Invalid Outputs: Add a post-processing layer that automatically repairs syntactically valid but semantically incorrect LLM outputs. Use structural transformations (e.g., Boolean normalization, quantifier pruning, constraint relaxation, guard insertion) and data-driven selector generators to create candidate patches. Retain only descendants that reduce mismatch or improve simplicity, enabling the system to salvage partially correct hypotheses.

3. Exact Simplification for Verified Formulas: After a formula is verified as train-valid, apply a deterministic simplifier that performs AST-level edits (deletion, factoring, quantifier merging, equality simplification) while preserving the exact truth-value vector on all training objects. This reduces formula size and improves holdout generalization, as shorter formulas are more likely to match the true concept.

4. Cumulative Frontier Memory Across Calls: Maintain a persistent, ranked frontier of the best hypothesis seen so far (by validity, mismatch count, AST size, quantifier depth). Use this frontier as an anchor in subsequent prompts, ensuring that progress is never lost and that later LLM calls build on verified improvements rather than starting from scratch.

5. Symbolic-First Workflow Integration: Before invoking the LLM, run a fast symbolic synthesizer (e.g., Z3 with bounded grammars). If it solves the problem, skip the LLM entirely. If not, apply the verifier-guided LLM loop only to unsolved instances. This reduces LLM calls by 8–46% and increases overall validity by 2–11 percentage points, combining the strengths of exhaustive search and generative flexibility.

6. Error-Guided Prompt Construction: Construct prompts that explicitly list the current frontier formula, its validity status, residual mismatch counts, AST size, quantifier depth, and the specific misclassified objects. This provides the LLM with concrete, actionable feedback, steering it toward fixing known errors rather than exploring blindly.

7. Multi-Source Hypothesis Generation: Combine direct LLM proposals with symbolic repair descendants and independent symbolic synthesis. Track which source first achieves exact validity, and use this lineage to prioritize future generation strategies—e.g., if repair is advancing the frontier but not solving, allocate more compute to direct generation or vice versa.

8. Complexity-Aware Ranking and Selection: Rank all candidate formulas (LLM, repaired, simplified) using a deterministic lexicographic order: evaluable > parseable > train-valid > lower mismatch > smaller AST > lower quantifier depth > fewer equality symbols. This ensures the system always retains the simplest verified hypothesis, improving interpretability and reducing overfitting.

9. Holdout-Aware Simplification: After final selection, apply a final exact pass that shortens train-valid formulas while preserving training predictions. Monitor holdout exactness to confirm that simplification does not degrade generalization—shorter formulas are more likely to be correct on unseen worlds, as shown by the paper’s results.

10. Bounded Trajectory Control: Limit the number of LLM calls (e.g., six) and use the verifier to decide when to stop (e.g., when a train-valid formula is found or no improvement occurs). This reduces computational cost while maintaining high success rates, as demonstrated by the paper’s efficiency gains over repeated generation.

What the Improved AI System Can Do:

• Solve first-order concept synthesis tasks with significantly higher accuracy (e.g., from 4.7% to 29.0% validity on Benchmark300) by combining LLM generation with exact verification and symbolic repair.

• Recover correct formulas from partially correct LLM outputs, even when the initial hypothesis has high error rates (median 32.1% mismatch), by iteratively repairing and retaining the best verified candidate.

• Produce shorter, more generalizable formulas that are more likely to match the true concept on holdout worlds, improving world-exactness by up to 20 percentage points.

• Reduce reliance on LLM calls by first attempting symbolic synthesis, and by using a cumulative frontier to avoid redundant generation—achieving higher validity with fewer calls.

• Handle invalid or unparseable LLM outputs gracefully through symbolic repair and simplification, rather than discarding them as failures.

• Provide interpretable, verifiable hypotheses at every step, with exact guarantees on training data and measurable complexity metrics (AST size, quantifier depth), enabling trust in the system’s outputs.

• Scale to diverse relational structures (unary and binary predicates, equality) and adapt to both standard and deliberately difficult benchmarks, outperforming both pure LLM generation and pure symbolic search in most cases.

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.