Warmup Guide — Neurosymbolic Reasoning: LLM Proposes, Symbolic Verifies

Zero-to-senior primer for Phase 14. We start from the uncomfortable fact that a transformer cannot know anything is true — it can only predict that a true-sounding token comes next — and we end with the one architecture that buys back the guarantee: a sound symbolic verifier bolted onto a neural proposer. Along the way we build, from first principles, the symbolic machinery every senior should be able to write on a whiteboard: facts and Horn clauses, unification, forward chaining to a fixpoint, backward chaining with a proof, backtracking constraint solving, and schema/type verification — then the loop, propose_and_verify, that is the phase's entire thesis.

Table of Contents

Chapter 1: Why Pure Neural Reasoning Is Unreliable

From zero. A large language model computes one thing: P(next token | previous tokens). It is trained to make plausible continuations, and it is breathtakingly good at it. But "plausible" is not "true," and there is no internal mechanism that distinguishes the two. When you ask for 17 × 23, the model does not run a multiplication; it emits the token sequence that looked like the answer in similar contexts. Sometimes that is 391; sometimes it is 371 delivered with identical confidence. The model has no assert.

Why this happens, mechanically. Three structural reasons, not bugs:

  1. No grounding. The training signal is text co-occurrence, not correspondence to a world or a proof system. A fact and a confident falsehood produce the same kind of gradient if both appeared fluently in the corpus.
  2. Soft, not discrete. Reasoning is implemented in continuous attention weights and residual activations. There is no place in the forward pass where a step is checked and the computation refuses to proceed. Every step is a smooth interpolation; errors compound silently.
  3. Brittle composition. Multi-step logic and arithmetic require carrying exact intermediate state. Transformers approximate this with limited depth and finite precision; the longer the chain, the more the approximation drifts. This is why a model that can add two 3-digit numbers fails on two 12-digit numbers — there was never an algorithm, only a learned shortcut.

The senior's framing. Treat an LLM's output as a hypothesis, never a conclusion. Its token probability is a prior over candidates, which is genuinely useful — but a prior is not a guarantee, and you cannot ship "probably correct" into a payments system, a medical workflow, or a robot's motion plan.

Common misconception. "Chain-of-thought makes it reason, so it's reliable now." CoT raises the probability of a correct path by spending more tokens on intermediate steps, and it helps a lot — but it is still next-token prediction. A confidently wrong chain of thought is a more persuasive wrong answer, not a checked one. "Faithful CoT" research exists precisely because the stated reasoning often does not match the actual computation.

Chapter 2: Why Pure Symbolic AI Is Brittle

From zero. Symbolic AI — Prolog, expert systems, planners, theorem provers — represents knowledge as explicit symbols and rules and manipulates them with sound inference. If a Prolog program says mortal(socrates) follows from human(socrates) and human(X) ⇒ mortal(X), that is not a guess; it is a proof. For sixty years this was "AI." It gave us the guarantee the LLM lacks.

Why it lost commercially. Three brick walls, each the mirror image of the LLM's strengths:

  1. No perception. A symbolic system needs the world handed to it as clean symbols. It cannot look at a photo, parse a messy sentence, or extract parent(alice, bob) from a paragraph. The moment input is raw, unstructured, or noisy, it is helpless.
  2. The knowledge-acquisition bottleneck. Every rule must be written by a human expert. Real domains have millions of rules and endless exceptions ("birds fly — except penguins, ostriches, injured birds, dead birds…"). Hand-authoring and maintaining that is economically fatal; this killed the 1980s expert-systems industry.
  3. Brittleness at the edges. Symbolic systems are exact inside their model and catastrophic just outside it. An input the rules don't cover doesn't degrade gracefully — it fails or produces nonsense. There is no "fuzzy match to the nearest known case."

The senior's framing. Symbolic systems are sound but blind. They will never tell you a falsehood about their own rules, and they will never tell you anything about the actual world unless someone first translated it into their symbols.

Common misconception. "Symbolic AI is dead." The expert-system business model is dead. The technology — SAT/SMT solvers, type checkers, theorem provers, CSP engines — is everywhere and indispensable: your compiler, your build system, your verification tooling, every cloud provider's network-config checker. It just stopped trying to be the whole brain and became the verifier.

Chapter 3: The Neurosymbolic Thesis

The synthesis. Put the two side by side and the deal is obvious:

Neural (LLM)Symbolic
Perception / NL✅ excellent❌ none
Generation / fuzziness✅ excellent❌ brittle
Soundness / guarantee❌ none✅ total
Explainability❌ opaque✅ proof trace
Knowledge acquisition✅ learned from data❌ hand-authored

Each is strong exactly where the other is weak. Neurosymbolic AI combines learned pattern-matching with sound symbolic reasoning so the system is fluent and trustworthy.

The asymmetry that makes it practical. You might imagine a deep, bidirectional fusion. In practice the dominant, shippable pattern is lopsided and simple:

The LLM proposes; the symbolic engine verifies.

Why this direction and not the reverse? Because verifying a candidate is far cheaper and far more reliable than synthesising a correct one symbolically. Generating a valid Sudoku solution by search is real work; checking a proposed grid is trivial and sound. Writing a theorem prover that finds proofs is decades of research; checking a proposed proof in Lean is a finished, trusted kernel. So you let the flexible neural model do the creative leap and let the cheap, sound symbolic checker be the gate. This is the P ≠ NP intuition applied to engineering: finding is hard, checking is easy — so spend your "hard" budget on a model that's good at guessing and your "easy, sound" budget on a verifier that's good at refusing.

   ┌─────────┐  candidate   ┌──────────────┐
   │ PROPOSER │ ───────────► │   VERIFIER   │
   │  (LLM)   │              │ (sound, det) │
   └─────────┘  ◄─────────── └──────────────┘
                  feedback           │ accept
                  (the reason        ▼
                   it was wrong)   return guaranteed-correct answer

Common misconception. "Neurosymbolic means a fancy hybrid neural net with a logic layer baked in." Sometimes (Chapter 10's differentiable approaches). But the version that earns its keep today is the loop, not a special architecture: an ordinary LLM, an ordinary solver, and a controller that retries with feedback. The lab builds exactly that.

Chapter 4: Knowledge Representation — Facts, Horn Clauses, Ontologies

What a fact is. The atom of symbolic knowledge is a ground fact: a predicate applied to constant arguments, like parent(alice, bob). "Ground" means no variables — every slot is a specific value. A knowledge base (KB) is a set of such facts. We model it as a Python set of frozen Fact objects, which gives deduplication and a clean fixpoint test for free.

What a rule is. A Horn clause is an implication with a conjunction of conditions (the body) and exactly one conclusion (the head):

$$ b_1 \wedge b_2 \wedge \dots \wedge b_n ;\Rightarrow; h. $$

The "exactly one positive conclusion" restriction is what makes Horn logic efficient and decidable for our purposes — it is the logical core of Prolog and Datalog. Bodies and heads use patterns: atoms whose arguments may be variables (we mark them with a leading ?, e.g. ?x). The classic example is the transitive closure of ancestor:

parent(?x, ?y)                       ⇒ ancestor(?x, ?y)
ancestor(?x, ?y) ∧ parent(?y, ?z)    ⇒ ancestor(?x, ?z)

The safety condition (do not skip this). Every variable in the head must appear in the body. A rule like parent(?x, ?y) ⇒ ancestor(?x, ?z) has a free ?z in the head and would "derive" ancestor(alice, <anything>) — infinitely many ungrounded facts. The lab's Rule constructor raises on an unsafe rule, because catching it at construction is the difference between a fixpoint and an infinite loop. This is the symbolic analogue of input validation.

Ontologies and knowledge graphs (the scaled-up version). A KB of facts with a typed schema of predicates and a class hierarchy (Dog ⊑ Mammal ⊑ Animal) is an ontology; stored as (subject, predicate, object) triples it is a knowledge graph (RDF/OWL, Wikidata, Neo4j). The reasoning we build here — forward/backward chaining — is exactly what an RDF reasoner runs over those triples to materialise entailed facts. The toy parent/ancestor KB is the same mechanism at lab scale.

Common misconception. "A knowledge graph is just a database." A database stores what you put in it; a KB with rules derives what follows. ancestor(alice, dan) is never stored — it is entailed, and the inference engine is what makes it appear.

Chapter 5: Unification — The Primitive Under Everything

The question. To fire a rule you must match its variable-bearing pattern against the ground facts you have. "Can parent(?x, bob) match parent(alice, bob), and if so, what is ?x?" Answering that — finding a substitution of variables to terms that makes two expressions equal — is unification, and both chaining directions and the proof search stand on it.

The algorithm (one-directional, sufficient here). Because our facts are always ground, we only ever bind variables on the pattern side. Walk the pattern's terms against the fact's args in lockstep:

  • predicate and arity must match, else fail;
  • if the pattern term is a variable: bind it to the fact's value — unless it is already bound to a different value (then fail; a variable must be consistent everywhere it appears);
  • if the pattern term is a constant: it must equal the fact's value, else fail.

The output is a substitution dict like {"?x": "alice"}, or None for no match.

unify( parent(?x, bob),  parent(alice, bob) )  →  {?x: alice}
unify( parent(?x, bob),  parent(alice, carol))  →  None        (constant bob ≠ carol)
unify( same(?x, ?x),     same(a, a)           )  →  {?x: a}
unify( same(?x, ?x),     same(a, b)           )  →  None        (?x can't be a and b)

That repeated-variable case (same(?x, ?x)) is the whole subtlety: a variable carries one binding across all its occurrences. Get that right and unification is twenty lines.

Common misconception. "Unification is just pattern matching." Pattern matching is one-way (bind the pattern to fixed data); full unification binds variables on both sides and includes the occurs check (a variable can't be bound to a term containing itself). We use the one-way restriction because ground facts make it sufficient — and saying exactly that in an interview shows you know what you simplified and why.

Chapter 6: Forward Chaining & the Fixpoint

What it is. Forward chaining is data-driven, bottom-up inference: start from the facts you have, fire every rule whose body is satisfied, add the new conclusions, and repeat. It computes the deductive closure — every fact entailed by the base facts and rules.

The mechanism, step by step. Each iteration (a full pass):

  1. Take a deterministic snapshot of the current facts (sorted, so the run is reproducible).
  2. For each rule, find every substitution that satisfies all its premises — a conjunctive join, implemented as recursive backtracking over the premise list (each premise unified against the snapshot, recursing on the rest with the extended substitution).
  3. Ground each rule's conclusion under each satisfying substitution; collect the ones not already present.
  4. If this pass produced no new facts, stop — you have reached the fixpoint. Otherwise add them and run another pass.

The fixpoint, formally. Let ( T ) be the "fire all rules once" operator on a fact set ( S ). Forward chaining computes the least fixpoint

$$ S^* = T(S^*) , \qquad \text{i.e. the smallest } S \text{ with } T(S) \subseteq S. $$

Because each pass only adds facts and the set of derivable ground facts (the Herbrand base) is finite, the sequence ( S, T(S), T^2(S), \dots ) is monotonically increasing and bounded, so it must stabilise. "No new facts this pass" is the computational witness that you have arrived.

iter 0: parent(a,b) parent(b,c) parent(c,d)
iter 1: + ancestor(a,b) ancestor(b,c) ancestor(c,d)         (rule 1)
iter 2: + ancestor(a,c) ancestor(b,d)                       (rule 2)
iter 3: + ancestor(a,d)                                     (rule 2 again)
iter 4: (nothing new)  →  FIXPOINT, stop

Why determinism and termination matter. A max_iters guard turns "did the rules have a bug" into a RuntimeError instead of a hung process; the sorted snapshot makes the derived set byte-for-byte reproducible (a test contract). Symmetric or cyclic rules (sib(?x,?y) ⇒ sib(?y,?x)) still terminate because once both directions are present, a pass adds nothing.

Common misconception. "Forward chaining is wasteful — it derives everything." Yes, and that is the point when you will query repeatedly: materialise the closure once, then every membership test is O(1). The trade-off vs backward chaining (Chapter 7) is exactly derive-everything-once vs prove-on-demand — Datalog's "bottom-up" vs Prolog's "top-down."

Chapter 7: Backward Chaining & the Proof Trace

What it is. Backward chaining is goal-driven, top-down inference: start from the goal you want to prove and work backwards, asking "what would make this true?" It is how Prolog answers a query, and unlike forward chaining it does only the work the goal demands.

The mechanism. To prove(g):

  1. Base case — if g is already a known fact, it is proven; the proof leaf is [fact].
  2. Rule case — find a rule whose head unifies with g. Bind the head's variables to g's constants, then recursively prove each premise under those bindings. If all premises prove, g is proven via that rule, and the subproofs become children in the proof tree.
  3. If neither works (within a depth bound), the goal is not proven → None.

The depth bound is not a detail — it is what makes a false goal (or a cyclic rule set) fail fast instead of recursing forever. A senior always asks "what stops this loop?"

The proof trace — soundness you can read. The output is not a bare boolean; it is a proof tree that an auditor can check by hand. This is the symbolic side's superpower over the LLM: the answer comes with its justification.

ancestor(alice, dan)        [ancestor]      ← proven by the transitivity rule
  ancestor(alice, carol)    [ancestor]      ← itself proven by a rule
    ancestor(alice, bob)    [ancestor]
      parent(alice, bob)    [fact]          ← grounds out in a base fact
    parent(bob, carol)      [fact]
  parent(carol, dan)        [fact]

A subtlety the lab makes you confront. Proving ancestor(alice, dan) via the rule ancestor(?x,?y) ∧ parent(?y,?z) ⇒ ancestor(?x,?z) requires binding ?y to carol — but ancestor(alice, carol) is not a base fact, it is itself derivable. So the premise enumeration must consider derivable groundings, not just stored ones. The clean solution: enumerate candidate bindings against the forward-chain closure, then prove each grounding top-down so the trace still shows the rules used. That interplay — backward search guided by forward closure — is a real technique (magic-sets / semi-naïve evaluation in disguise).

Forward vs backward — the senior's rule of thumb. Few facts, many possible queries, you'll ask once → backward (don't derive what you won't need). Stable KB, queried constantly → forward (materialise once, query free). Most production systems do both.

Common misconception. "Backward chaining is just recursion." It is recursion plus unification plus backtracking over rule choices plus a termination bound. Drop any of those and it either gives wrong answers or hangs.

Chapter 8: Constraint Satisfaction, SAT & SMT

The problem class. A constraint satisfaction problem (CSP) is: variables, each with a domain of allowed values, and constraints restricting which combinations are legal. Find an assignment of a value to every variable that satisfies all constraints — or prove none exists. Graph-colouring, Sudoku, timetabling, register allocation, and resource scheduling are all CSPs.

Backtracking — the core algorithm. Depth-first search with early pruning:

  1. Pick the next unassigned variable (in the lab, in declaration order — deterministic).
  2. Try each value in its domain, in order.
  3. After each tentative assignment, check every constraint on the partial assignment. If any is violated, prune this branch immediately and try the next value (this early check is the "propagation" that makes the exponential search tractable).
  4. Recurse. On a dead end, undo the assignment and backtrack.
  5. Return a complete assignment on success, or None if the whole tree is exhausted — which is a proof of unsatisfiability, not a failure to try hard enough.
solve 3-colour a triangle (A–B–C all adjacent), domain {R,G,B}:
  A=R → B=R? ✗ (A≠B) → B=G → C=R? ✗ (A≠C) → C=G? ✗ (B≠C) → C=B ✓  → {A:R, B:G, C:B}

same triangle, domain {R,G} only:
  every branch hits a violated A≠B / B≠C / A≠C → tree exhausted → None
  (K3 is not 2-colourable; the solver *proves* it)

That None is the whole lesson. A backtracking solver that exhausts the search space returns a sound "unsatisfiable." This is the guarantee an LLM cannot give: ask a model "can this graph be 2-coloured?" and it may confidently say yes. The solver knows.

SAT and SMT — the industrial version. A SAT solver decides satisfiability of Boolean formulas; modern CDCL (conflict-driven clause learning) SAT solvers handle millions of variables and are the workhorse behind verification, planning, and config-checking. SMT (satisfiability modulo theories — e.g. Z3) extends SAT with arithmetic, arrays, and bit-vectors, so you can ask "is there an integer x such that …" directly. Our backtracking solver is the conceptual ancestor; real systems add clause learning, unit propagation, and smart variable ordering — but the "search + propagate + prove-unsat-by-exhaustion" skeleton is the same, and it is what you bolt onto an LLM when the candidate must satisfy hard constraints.

Common misconception. "Just ask the LLM to respect the constraints in the prompt." It will usually comply and occasionally not, with no way to tell which. A solver either returns a satisfying assignment or proves there is none. Use the model to propose (it's a great heuristic for which branch to try first); use the solver to guarantee.

Chapter 9: Verification — Types, Schemas, Proofs, Execution

The unifying idea. A verifier is a sound, deterministic function candidate → (ok, reason). It never produces a false "ok," and on rejection it returns why. The four production verifiers a senior should know:

  1. Type / schema checking. Does the LLM's JSON match the contract? The lab builds a JSON-schema-ish validate_against_schema: primitives with enum/min/max, arrays with item schemas and length bounds, objects with required keys and "no extra keys." Crucial design decision baked into the lab: a bad value returns False (a verification outcome the loop can act on); a malformed schema raises (SchemaError, a programmer bug). Conflating those two is a classic API-design mistake — "is this a verdict or a crash?" must be unambiguous. One more honest subtlety: in Python bool is a subclass of int, so True would sneak past an int check — the verifier explicitly rejects it. Edge cases like that are why you write the checker instead of trusting isinstance.
  2. Constraint / CSP checking (Chapter 8) — does the candidate satisfy hard constraints?
  3. Proof checking — does a proposed proof close in a trusted kernel (Lean, Isabelle, Coq)? The kernel is tiny and audited, so a checked proof is certain; this is how LLM theorem-proving gets its guarantee.
  4. Execution checking — run the LLM's code against tests / a reference. The interpreter is the verifier; passing tests is the (probabilistic but strong) signal.

Why "return the reason" is the load-bearing part. A verifier that says only False ends the conversation. A verifier that says "value -5 violates age.min = 0" hands the proposer structured signal for its next attempt. The reason string is the bandwidth of the feedback loop in Chapter 10.

Common misconception. "A verifier just needs to be correct." It needs to be correct and informative and fast. You will call it on every attempt; a slow or silent verifier guts the loop. Soundness is the floor, not the ceiling.

Chapter 10: The Integration Patterns (and Why One Wins)

There are three families of neurosymbolic integration. Know all three; reach for the first.

(1) LLM-as-proposer + symbolic-verifier (the dominant, shippable one). The loop the lab builds: the network generates a candidate, the symbolic engine verifies it, and on rejection the reason is fed back for a retry, up to a budget. The answer that leaves the system is guaranteed by the verifier, not by the model's confidence.

$$ \text{result} = \begin{cases} c_i & \text{first } c_i = \text{proposer}(i, r_{i-1}) \text{ with } \text{verify}(c_i)=\text{ok} \ \text{fail} & \text{if no } c_i \text{ verifies within } N \text{ attempts.} \end{cases} $$

This subsumes: code-execution checks, type/schema validation, calculator/tool use, CSP/SAT gating, and theorem-prover checking. It is exactly the lab's propose_and_verify.

(2) Symbolic-in-the-loop (tools the LLM calls mid-generation). Rather than verify a finished answer, the model invokes symbolic engines as it reasons — a calculator, a SQL engine, a CAS (computer algebra system), an SMT solver — and conditions on the (sound) results. This is the tool-use of Phase 12 with symbolic tools, and it is the same proposer/verifier idea interleaved step-by-step instead of at the end.

(3) Differentiable / learned-relaxation (deep fusion). Make the symbolic operation differentiable so it can be trained end-to-end: soft/fuzzy logic (Logic Tensor Networks), neural theorem provers, DeepProbLog (probabilistic logic with neural predicates), differentiable SAT layers. Elegant and the subject of much research, but harder to engineer, harder to guarantee, and rarely the production answer today. Know it exists; don't lead with it.

Constrained decoding as a degenerate verifier (tie to Phase 08). A grammar/regex mask applied during sampling is a verifier moved inside the decoder: at every token it rejects continuations that would violate the structure. That is pattern (1) collapsed from "verify the whole answer" to "verify each token" — the cheapest possible verifier, run continuously. The lab's schema check is the same guarantee applied once, at the end; constrained decoding is it applied at every step. Same thesis, different granularity.

Common misconception. "The fancier (differentiable) integration must be better." For a senior shipping a correctness-critical feature, the simple loop wins: it reuses your existing model and an off-the-shelf solver, the guarantee is obvious and auditable, and you can explain it to a reviewer in one sentence. Complexity is a cost, not a credential.

Chapter 11: Real Systems & the Road to Robotics

AlphaGeometry (DeepMind, 2024). Solved olympiad geometry at near-gold-medal level by pairing a language model (proposes auxiliary constructions — the creative leap) with a symbolic deduction engine (derives consequences soundly). Pure neurosymbolic proposer/verifier: the LM guesses where to add a point; the symbolic engine grinds out what follows. Neither half could do it alone.

LLM + Lean / Isabelle (DeepSeek-Prover, and the broader autoformalisation line). The model proposes a formal proof; the proof assistant's kernel checks it. Because the kernel is small and trusted, a checked proof is certain — the model can hallucinate freely and nothing wrong gets through. This is the cleanest possible instance of the thesis: an absolutely sound verifier.

LLM + CAS / SMT. Wire a computer-algebra system (SymPy, Mathematica) or an SMT solver (Z3) as the symbolic backend: the model sets up the problem in natural language, the solver returns the sound result. This is how you make an LLM trustworthy at math — not by training it harder, but by giving it a calculator it cannot argue with.

Constrained decoding in production (Phase 08). Every "guaranteed valid JSON" feature (structured outputs, function-calling schemas) is a constrained-decoding verifier in the sampler. You have already met this mechanism; now you can name it as a special case of neurosymbolic verification.

Where this goes next — robotics and agents (forward-ref Phase 15). When an LLM plans a robot's actions, "probably safe" is not acceptable. The neurosymbolic move: encode safety and feasibility as symbolic constraints, and verify the plan before executing it — backward_chain the goal "this plan violates no constraint," or run the plan through a CSP/temporal-logic checker, and refuse to actuate an unproven plan. The proposer dreams up the plan; the verifier is the thing that keeps the robot from driving through a wall. Phase 15 builds on exactly this.

Common misconception. "These are research curiosities." AlphaGeometry, Lean-checked proofs, and constrained decoding are all deployed or competition-winning. The proposer/verifier pattern is the single most reliable way known to get a guarantee out of a generative model, and it is becoming table stakes for correctness-critical AI.

Lab Walkthrough Guidance

The lab (lab-01-neurosymbolic-verifier) turns these chapters into code. Suggested order (matches the file top-to-bottom):

  1. Knowledge representation (Fact, Pattern, Rule) — Chapter 4. The only real logic is the Rule safety check: every head variable must appear in the body, else ValueError.
  2. Unification (unify) — Chapter 5. Twenty lines; the subtlety is the consistent-binding case (same(?x, ?x)). Get test_unify_* green before moving on — everything depends on it.
  3. Forward chaining (_match_premises, forward_chain) — Chapter 6. The conjunctive join is recursive backtracking; the loop stops when a pass adds nothing (the fixpoint). Use the sorted snapshot for determinism and the max_iters guard for safety.
  4. Backward chaining (backward_chain, Proof) — Chapter 7. The trick is enumerating derivable (not just base) premise bindings — reuse the forward_chain closure, then prove each grounding top-down so the trace records the rules. The depth bound makes a false goal return None.
  5. CSP (all_different, not_equal, solve_constraints) — Chapter 8. Order-deterministic backtracking with a constraint check on each partial assignment. None for an unsatisfiable instance is the point.
  6. Schema/type check (validate_against_schema, TypeChecker) — Chapter 9. Remember: bad value → False, malformed schema → SchemaError; and bool is not a valid int.
  7. The neurosymbolic loop (propose_and_verify, VerifyResult) — Chapter 10. Propose → verify → on reject feed the reason back → retry to the budget. test_propose_and_verify_accepts_ later_valid_proposal is the soul of the lab: the first proposal is wrong, the verifier catches it, the second is returned.

Run red → green: pytest test_lab.py -v, then LAB_MODULE=solution pytest test_lab.py -v, then python solution.py for the worked run.

Success Criteria

  • All tests pass against your lab.py and against LAB_MODULE=solution.
  • You can state, without notes, why pure neural reasoning has no guarantee and pure symbolic has no perception — and why "LLM proposes, symbolic verifies" exploits both.
  • You can hand-trace forward_chain on the parent/ancestor KB to its fixpoint and explain that "a pass adds nothing" is the termination witness.
  • You can read a backward_chain proof tree and identify base-fact leaves vs rule firings, and say why the depth bound makes a false goal terminate.
  • You can explain why a backtracking CSP's None is a sound unsatisfiability proof, and why an LLM cannot give you that.
  • You can articulate the bad-value-vs-bad-schema design split, and why returning a reason (not just False) is what makes the retry loop work.
  • You can place constrained decoding (Phase 08) as a per-token degenerate case of the verifier pattern, and name AlphaGeometry / LLM+Lean as the canonical systems.

Interview Q&A

  • "Why can't you just trust an LLM's reasoning?" — Next-token prediction optimises plausibility, not truth; no grounding, no discrete check, brittle multi-step composition. Treat output as a hypothesis; get the guarantee from a verifier, not from the prompt.
  • "What killed symbolic AI, and what survived?" — The expert-system business model (no perception, hand-authored rules, edge-brittleness). The technology — SAT/SMT, type checkers, theorem provers, CSP — is everywhere; it became the verifier instead of the brain.
  • "State the neurosymbolic thesis in one sentence." — The LLM proposes (flexible, fluent), a sound symbolic engine verifies (guaranteed, explainable), and rejection feedback drives a retry — because checking a candidate is far cheaper and more reliable than synthesising one.
  • "Forward vs backward chaining — when each?" — Forward = data-driven, materialise the whole closure once (great for repeated queries on a stable KB; Datalog). Backward = goal-driven, prove on demand and only do the needed work, returns a proof tree (Prolog).
  • "How does forward chaining terminate?" — Each pass only adds facts; the Herbrand base is finite; so the increasing, bounded sequence reaches a least fixpoint — operationally, "a pass derives nothing new." A max_iters guard turns a buggy rule set into an error, not a hang.
  • "What is unification and where's the subtlety?" — Find a substitution making a pattern equal a fact; the subtlety is consistent bindings for repeated variables (and the occurs-check in the full bidirectional version, which we can skip because facts are ground).
  • "Your CSP returns None — what does that mean?" — A backtracking solver that exhausts the search space has proven unsatisfiability; it's a sound result, not "didn't find one." That guarantee is exactly what the LLM lacks.
  • "Bad LLM JSON — False or raise?" — Bad value → False (a verification outcome the loop feeds back); malformed schema → raise (a programmer bug). And reject bool as int, since Python makes bool an int subclass.
  • "How does AlphaGeometry use this pattern?" — A language model proposes auxiliary constructions; a symbolic deduction engine derives consequences soundly. Proposer/verifier; neither half solves olympiad geometry alone.
  • "How is constrained decoding related?" — It's the verifier collapsed into the sampler: a grammar/regex mask rejects invalid tokens at every step instead of validating the whole answer once. Same thesis, finer granularity (Phase 08).
  • "Why feed the error back instead of just resampling?" — The rejection reason is structured signal ("?y violates all_different") that conditions the next proposal toward the valid region — exactly how LLM+Lean and AlphaGeometry iterate. Blind resampling wastes the information the verifier already computed.
  • "Where does this matter for robotics/agents?" — Verify a plan before executing it: encode safety/feasibility as constraints or Horn rules and refuse to actuate an unproven plan. "Probably safe" is not safe (Phase 15).

References

  • Trinh, Wu, Le, He, Luong, Solving Olympiad Geometry without Human Demonstrations ("AlphaGeometry", Nature, 2024) — the canonical LLM-proposes / symbolic-verifies system.
  • Garcez & Lamb, Neurosymbolic AI: The 3rd Wave (2020/2023) — the survey of integration patterns.
  • Kautz, The Third AI Summer (AAAI Robert S. Engelmore Lecture, 2022) — a taxonomy of neural+symbolic architectures from a founder of the field.
  • Ellis et al., DreamCoder: Growing generalizable, interpretable knowledge with wake-sleep Bayesian program learning (2021) — learning symbolic programs with a neural search policy.
  • DeepSeek-AI, DeepSeek-Prover (2024) and the broader LLM + Lean/Isabelle autoformalisation line — proof generation gated by a trusted kernel.
  • Lyu et al., Faithful Chain-of-Thought Reasoning (2023) — why stated CoT ≠ actual computation, and translating NL reasoning into checkable symbolic form.
  • de Moura & Bjørner, Z3: An Efficient SMT Solver (2008) — the SMT solver behind LLM+SMT systems.
  • Russell & Norvig, Artificial Intelligence: A Modern Approach — chapters on logical agents, inference (forward/backward chaining, unification), and constraint satisfaction (the textbook treatment the lab miniaturises).
  • Datalog / Prolog references and the RDF/OWL reasoning literature for forward chaining at scale.