Phase 14 — Neurosymbolic Reasoning: LLM Proposes, Symbolic Verifies

The phase that fixes the one thing a language model fundamentally cannot do: be sure. A transformer is a magnificent pattern-matcher and a hopeless logician — it will tell you, with total fluency and total confidence, that 17 × 23 = 371, that a flight connects two cities it doesn't, that a plan is safe when it isn't. The senior move is not "prompt it harder." It is to bolt a sound symbolic verifier onto the side of the neural model so that nothing leaves the system until something that cannot hallucinate has checked it. That pattern — LLM proposes, symbolic verifies — is how AlphaGeometry hit IMO-medal level, how LLM+Lean proves theorems, and how production agents avoid shipping a confident lie.

Why this phase exists

Every phase before this one made the neural part better — bigger, faster, cheaper, aligned, retrieval-grounded, tool-using. None of it bought you a guarantee. A 405B model and a 1.5B model are both equally capable of asserting a false arithmetic fact with a straight face, because next-token prediction has no notion of proof. Meanwhile, the symbolic AI of the 1980s had nothing but guarantees — a Prolog program never lies about whether a goal follows from its rules — and it died commercially because it could neither perceive the world nor read a sentence.

Neurosymbolic AI is the synthesis a senior engineer reaches for when correctness is non-negotiable: keep the LLM's flexibility (perception, natural language, fuzzy generation) and add the symbolic engine's soundness (logic, constraints, types, proofs). The integration that actually ships is asymmetric and simple — the network generates, the symbolic core checks — and this phase builds that core from scratch: a forward/backward-chaining inference engine, a backtracking constraint solver, a schema/type verifier, and the loop that ties them to an injected "LLM" proposer.

The deeper reason this works is the oldest one in computer science: finding a correct answer is hard, but checking a proposed one is easy and sound. Generating a valid schedule, a closed proof, or a satisfying assignment is real search; verifying a candidate is cheap and gives a guarantee. So you spend your expensive, flexible budget (the LLM) on the guess and your cheap, sound budget (the solver, the type checker, the proof kernel) on the gate. That asymmetry is why this phase's pattern — not a fancier hybrid architecture — is what correctness-critical AI actually ships.

Concept map

                ┌───────────────────────────────────────────────┐
                │   Neural is fluent but unsound.                │
                │   Symbolic is sound but blind.                 │
                │   Neurosymbolic = use each for what it's good at│
                └───────────────────────────────────────────────┘
                         │                          │
            ┌────────────┘                          └────────────┐
            ▼                                                     ▼
     NEURAL  (the proposer)                          SYMBOLIC  (the verifier)
     LLM / pattern-matching                          sound, deterministic, explainable
     perception, NL, generation                      logic · constraints · types · proofs
            │                                                     │
            │  candidate answer                                   │
            └──────────────────────►  VERIFY  ◄──────────────────┘
                                        │
              ┌─────────────────────────┼──────────────────────────┐
              ▼                          ▼                          ▼
       KNOWLEDGE + INFERENCE       CONSTRAINTS (CSP/SAT)      TYPES / SCHEMA
       facts, Horn rules           backtracking + prune       JSON-schema-ish
       forward chain → fixpoint    graph-colour, scheduling   structured-output check
       backward chain → proof      satisfiable? assignment    accept / reject + reason
              │                          │                          │
              └──────────────┬───────────┴──────────────┬───────────┘
                             ▼                           ▼
                   accept → return answer       reject → feed reason back
                                       │              (retry up to N)
                                       ▼
                          THE NEUROSYMBOLIC LOOP
                  propose_and_verify(proposer, verifier, max_attempts)
            "flexibility from the network, guarantees from the symbols"

The lab

The lab is a runnable, test-verified miniature — see the lab standard. The "LLM" is an injected deterministic proposer stub, so the whole pipeline is offline and reproducible. Run it red (pytest test_lab.py), make it green, then read solution.py.

Integrated scenario ideas

• Make an LLM do reliable arithmetic. Wire a calculator (a trivial symbolic verifier) into propose_and_verify: the model proposes an answer, the calculator checks it, wrong answers get the real value fed back. Show the failure rate drop to zero — the verifier is the guarantee, not the prompt.
• Constrain a generated schedule. Have the proposer emit a class timetable; verify it with a CSP (no room double-booked, no teacher in two places). Show the verifier catching a plausible but infeasible draft the model was confident about.
• Validate structured output. Point TypeChecker at an LLM's JSON; reject malformed records with a reason, retry, and compare to "just ask nicely for valid JSON." Tie to constrained decoding (Phase 08) — that is the same idea moved inside the sampler.
• Prove a plan is safe before executing it. Encode safety rules as Horn clauses; before an agent acts, backward_chain the goal "this plan violates no constraint" and refuse to run an unproven plan (forward-ref to Phase 15's verified plans).

What "done" looks like in your head

By the end you should be able to walk into a design review where someone says "the model is unreliable, let's fine-tune it more" and counter with a mechanism: what is the verifier, what does it return on rejection, and how does the feedback close the loop? You should be able to hand-trace forward chaining to a fixpoint, read a backward-chaining proof tree, and explain why a CSP's None is a sound impossibility proof an LLM can never give. The lab makes each of those a function you wrote and a test you can point to — and the soul test, where the verifier catches a wrong LLM proposal and the loop recovers, is the artifact you demo to prove you understand the thesis.

Deliverables checklist

• lab.py passes pytest test_lab.py -v (and LAB_MODULE=solution does too).
• You can explain why a pure LLM has no guarantee and a pure symbolic system has no perception, and why the proposer/verifier split exploits both.
• You can hand-trace forward_chain to a fixpoint and explain how "no new facts" terminates it.
• You can read a backward_chain proof tree and say which steps are base facts vs rule firings.
• You can explain why a backtracking CSP returns None for an unsatisfiable instance.
• You can name three production verifiers (code execution, type/schema check, theorem prover) and place constrained decoding as a degenerate verifier inside the decoder.

Key takeaways

• The network proposes; the symbol checks. This asymmetry is the whole phase. The hard, brittle, knowledge-acquisition-heavy symbolic part stays small (a checker), and the flexible part (generation) stays neural. You verify a candidate far more cheaply than you'd synthesise a correct one symbolically.
• A verifier converts confidence into correctness. An LLM's 0.99 token probability is not a guarantee; a passing type-check, a satisfied constraint set, or a closed proof is. Soundness comes from the symbolic side or it does not exist.
• Feedback closes the loop. Rejection is not the end — the symbolic error is structured signal the proposer can use. "Wrong: variable ?y violates all_different" is a far better next-step prompt than silence. This is exactly how AlphaGeometry and LLM+Lean iterate to a solution.
• Constrained decoding is this pattern collapsed into the sampler. A grammar/regex mask is a verifier applied at every token instead of every answer — Phase 08's mechanism is a special case of Phase 14's thesis.

Next: Phase 15 — Embodied AI & Robotics.