Lab 01 — Neurosymbolic Verifier: "LLM Proposes, Symbolic Verifies"

Phase: 14 — Neurosymbolic Reasoning Difficulty: ⭐⭐⭐☆☆ (the logic is moderate; the judgment is ⭐⭐⭐⭐⭐) Time: 4–5 hours

A language model is a fluent guesser with no assert; a symbolic engine is a perfect logician that can't perceive. This lab builds the bridge: a symbolic reasoning core — a Horn-clause inference engine (forward chaining to a fixpoint, backward chaining with a proof trace), a backtracking constraint solver, and a JSON-schema-ish type checker — coupled to an injected, deterministic "LLM" via propose_and_verify. The thesis of the phase, in one function: the model proposes a candidate, the sound symbolic verifier accepts or rejects it (handing back the reason on rejection), and we retry up to a budget — so nothing leaves the system until something that cannot hallucinate has signed off.

What you build

• Fact / Pattern / Rule — the knowledge representation: ground facts in a set-backed KB, variable-bearing patterns, and Horn clauses (body ⇒ head) with an enforced safety check (every head variable must appear in the body, else a runaway derivation).
• unify — the primitive under everything: match a pattern against a ground fact, returning a consistent substitution {var: const} or None.
• forward_chain — data-driven, bottom-up inference that fires rules until a pass adds nothing (the least fixpoint = the deductive closure), deterministic and termination-guarded.
• backward_chain + Proof — goal-driven, top-down proving that returns a readable proof tree for a true goal and None for a false one (depth-bounded so it can't loop).
• solve_constraints + all_different / not_equal — a deterministic backtracking CSP solver: a satisfying assignment for a solvable instance, None (a sound unsatisfiability proof) for an impossible one. Enough for graph-colouring / Latin-square / scheduling.
• validate_against_schema + TypeChecker — a JSON-schema-ish verifier for an LLM's structured output: bad value → False (a verdict the loop can act on), malformed schema → SchemaError (a programmer bug), and bool is rejected as int.
• propose_and_verify + VerifyResult — the neurosymbolic loop: propose → verify → feed the rejection reason back → retry to max_attempts; return the first verified answer or a failure.

Key concepts

Files

Run

pip install -r requirements.txt
pytest test_lab.py -v                       # against your lab.py
LAB_MODULE=solution pytest test_lab.py -v   # against the reference
python solution.py                          # the worked example

Success criteria

• All tests pass against your implementation (and LAB_MODULE=solution).
• You can explain why forward_chain derives all and only the entailed facts and how the fixpoint (a pass with no new fact) terminates it without an infinite loop.
• You can read the backward_chain proof tree for ancestor(alice, dan) and point to base-fact leaves vs rule firings — and explain why a false goal returns None.
• You can explain why test_csp_unsatisfiable_returns_none (a triangle, two colours) proves K3 is not 2-colourable rather than merely failing to find a colouring.
• You can explain why validate_against_schema returns False for a bad value but raises for a malformed schema, and why it rejects True as an int.
• You can explain why test_propose_and_verify_accepts_later_valid_proposal is the soul of the lab: the first LLM proposal is wrong, the verifier catches it, and the second is returned.
• Given any "make this LLM output trustworthy" prompt you can name the verifier, what it returns on rejection, and how the feedback closes the loop.

How this maps to the real stack

Limits of the miniature (be honest in the interview): our unify is one-directional (facts are ground) and skips the occurs-check; forward chaining is naïve (no semi-naïve/magic-sets optimisation), so it re-derives across passes; the CSP solver is plain backtracking (no arc consistency, MRV heuristic, or clause learning — real solvers add all three and scale by orders of magnitude); the schema checker covers a useful subset of JSON Schema, not the spec; and the "proposer" is a deterministic stub — a real LLM is non-deterministic, so production loops add sampling, caching, and a cost/latency budget on top of max_attempts.

Extensions (build these on real hardware / real models)

• Swap the stub proposer for a real LLM call and keep the verifier identical; measure how many attempts a schema/CSP gate needs, and how feeding the reason back changes that number.
• Replace solve_constraints with z3 and solve a real timetable; show it proving an over-constrained instance unsatisfiable (the thing an LLM can't do).
• Add arc consistency (AC-3) and the minimum-remaining-values heuristic to the CSP solver and benchmark the node count on a harder instance.
• Wire a code-execution verifier: the proposer emits Python, the verifier runs it against unit tests, and failures (stack traces) become the feedback. This is the strongest practical verifier.
• Tie to Phase 08: implement a token-level grammar mask as a degenerate verifier and show it is propose_and_verify collapsed into the decoder.
• Tie to Phase 15: encode a robot plan's safety/feasibility as Horn rules and backward_chain the goal "this plan violates no constraint" before allowing execution.

Interview / resume

• Talking points: "Why can't you trust an LLM's reasoning, and what do you bolt on instead?" "Forward vs backward chaining — when each, and how does forward chaining terminate?" "Your CSP returns None — what does that mean?" "Walk me through AlphaGeometry as a proposer/verifier system." "How is constrained decoding the same idea inside the sampler?"
• Resume bullet: Built a neurosymbolic verification core — a Horn-clause forward/backward chaining inference engine, a backtracking constraint (CSP) solver, and a JSON-schema type checker — and the "LLM proposes, symbolic verifies" loop that gates an LLM's output behind a sound, explainable verifier with feedback-driven retry.