Neuro-symbolic reasoning and knowledge representation

Understand knowledge representation, symbolic reasoning, and neuro-symbolic integration (neural proposes, symbolic checks); planning as a bridge between them; and why a deterministic symbolic layer is the natural place to put the checks the neural layer cannot be trusted to make.

Track

Research

Module

9 · Agent cognition & reasoning

Prerequisites

Reasoning and test-time compute

A system that acts on the world needs to know what it believes, why it believes it, since when it is true, and what it should stop believing when new information arrives. A language model stores knowledge in its weights with none of those four properties: no explicit justification, no provenance, no time, and no coherent mechanism to revise one fact without disturbing others. Reported knowledge-editing experiments make this concrete — editing a single fact in the weights is remembered in isolation but fails on multi-hop questions that depend on it (change a country's head of government and the model still names the old spouse), because weight editing adds a fact without propagating its consequences.

Symbolic knowledge representation and symbolic reasoning supply exactly those properties, at a price in expressiveness and cost. The payoff for an agent is a layer whose guarantees are precise: it derives only what follows, it can return the proof, and its conclusions can be inspected, revised, and time-stamped. The design question this lesson answers is how to combine that layer with a neural model that generalises broadly but errs silently.

Explicit knowledge representation separates declarative knowledge from the inference procedure, so that behaviour improves by adding statements rather than by reprogramming. Four capabilities define it, and each has a mature formalism.

Ontologies and description logic

Classes, roles and axioms with a formal semantics, splitting terminology (the TBox) from assertions about individuals (the ABox). Expressiveness trades against tractability: full ontology reasoning is intractable, so standard profiles restrict the language to recover polynomial reasoning.

Knowledge graphs (RDF)

Facts as (subject, relation, object) triples, with named graphs grouping triples by source or version — the standard mechanism for provenance. A graph is a knowledge base only when it has a schema, provenance and time; without them it is just an index.

Time (bitemporal)

Valid time (when a fact holds in the world) separated from transaction time (when the system believed it). Together they answer "what was true at tv according to what we knew at tt", distinguishing a change in the world from the correction of an error — the basis for auditing a past decision.

Belief revision and truth maintenance

The AGM theory specifies what rational change of beliefs must satisfy (expansion, contraction, revision); a truth-maintenance system records why each belief is held and retracts it when its support falls, with dependency-directed backtracking to the assumptions responsible for a contradiction.

One distinction matters for agents and is easy to get wrong: revising is not updating. Revision incorporates new information about a world that has not changed (an observation); update incorporates a change in the world (the effect of an action). The two obey different postulates and give different answers to the same input, and confusing them produces inferences with no basis — concluding something about a state that was never observed. A real system also needs non-prioritised revision: the right to not accept an input, which is indispensable when the source can be wrong or hostile. In the recommended architecture the model proposes facts and translates queries, but does not write directly into the base; its proposals pass through a revision policy that weighs source reliability against the entrenchment of what they contradict.

Symbolic reasoning manipulates formulas by rules whose correctness can be proven: if the premises are true, the conclusion is too, and the procedure can return the proof. Four modes of inference matter, and only one preserves truth. Deduction goes from premises to necessary consequences. Induction generalises from cases to a rule — it extends knowledge at the cost of being able to be wrong. Abduction goes from an observation to a hypothesis that would explain it. Non-monotonic reasoning cuts across all three: a conclusion reached by default ("the service is healthy unless there is an alert") is retracted when information is added, unlike classical logic where adding premises never removes consequences.

The engines that mechanise deduction scale through a few ideas: resolution with unification in first-order logic; SAT solvers (DPLL, and its successor CDCL, which learns a new clause from each conflict and backtracks non-chronologically); and satisfiability modulo theories (SMT), which decides boolean formulas whose atoms belong to a theory with its own decision procedure (arithmetic, arrays, bit-vectors). These come with teeth: SAT is NP-complete, first-order validity is only semi-decidable (a search for a refutation that does not exist may never terminate), and there are small, obviously unsatisfiable formulas that no solver refutes in reasonable time.

The property that matters most for neuro-symbolic design is an asymmetry. Checking a proposed solution is cheap — evaluating a formula on a candidate model is linear time — while finding one, or proving none exists, is hard. Modern solvers exploit this: they can emit a certificate (a model to substitute and check, or an unsatisfiability proof a small independent verifier reviews). So an unreliable component can propose, as long as a reliable and cheap component checks. That asymmetry is the hinge of the next sections.

The reported evidence on what language models do when asked to reason deductively sharpens the division of labour. They take individually correct deduction steps but do not search systematically when several valid steps are possible — they fail at planning the proof — and on compositional tasks their accuracy decays quickly with complexity. In induction they are good at proposing candidate rules and poor at applying them, and pairing a proposer with a symbolic interpreter that filters the rules works well. The systematic search — choosing among steps, backtracking, proving no solution exists — is exactly what DPLL and CDCL do.

Planning sits between knowledge representation and reasoning: it builds, before acting, a sequence or policy that reaches a goal under an explicit model of the domain. A classical planning problem is states as sets of atoms, actions with preconditions and add/delete effects, an initial state and a goal; planning is searching a path in an implicit state graph. A* is the reference algorithm, expanding states in order of estimated total cost, and a heuristic obtained by solving a relaxed problem is admissible — it never overestimates — which is what guarantees an optimal plan.

The bridge is a difference of contract, and it is the whole reason planning appears in this lesson. A plan returned by a correct planner is valid with respect to the model: every precondition holds, the goal is reached. A plan generated by a language model carries no such guarantee. That difference is precisely what lets a system put the decision outside the model — the LLM may propose a plan, but a planner or a validator built on an explicit model is what certifies it respects the constraints. Deciding under genuine probabilistic uncertainty (belief states, expected utility) is a further step, treated in the uncertainty lesson; here the point is simply that a correct planner gives a guarantee a generator cannot.

A neuro-symbolic system combines a learned component that perceives, translates or proposes with a symbolic component that deduces, solves or checks with guarantees. Done well it keeps the best of each; done badly it inherits the brittleness of the specification and the ungroundedness of the model at once. The patterns differ by where the neural component sits relative to the guarantee.

• ▸Formalize-and-solve: the model translates the statement to a formal specification (first-order logic, SMT, a constraint problem) and a solver processes it. The guarantee is that the solution satisfies the TRANSLATED formula, not the true one — the model wrote the specification, so its error passes through the solver and comes out looking proven.
• ▸Generate-and-check: the model proposes complete candidates and an external verifier accepts or rejects them against a formal model it did NOT write. Precision is one by construction; the cost is paid in calls when the per-sample success probability is low. This is the strongest pattern, and it needs a trustworthy external model of the domain.
• ▸Logic in learning: a constraint enters the loss (semantic loss, fuzzy logics) or the architecture (differentiable provers). This improves the model on average but imposes nothing at inference time unless a layer enforces it.

Formalising qualitatively — which guarantee survives — gives one blunt consequence: in formalize-and-solve, retrying a weak filter does not improve precision. If a translation is uniquely but wrongly solvable with some probability and uniquely-correct with another, precision is fixed by the ratio of those two classes that the filter accepts; retries only convert abstentions into answers in the same proportion of right and wrong. Redundancy (two independent translations that must agree) helps against independent errors but not against a systematic misreading that recurs identically. Reported results fit the pattern: the large gains appear when the symbolic side verifies or reasons over a reliable specification (formal geometry, a program evaluator, expert-written constraints) or when the translation is nearly mechanical; the limits appear exactly where open language or perception must be mapped to symbols.

synthetic — a neuro-symbolic check loop (generate-and-check against an external model)
def solve(problem, spec_checker, max_tries=16):
    """Neural proposes; a deterministic checker verifies. The guarantee
    is the checker's, over a specification the MODEL did not write."""
    for i in range(1, max_tries + 1):
        candidate = neural_propose(problem)        # unreliable, broad
        verdict   = spec_checker.verify(candidate) # exact w.r.t. the model
        if verdict.ok:
            return Answer(candidate, tries=i, proof=verdict.certificate)
    # no accepted candidate: ABSTAIN, do not emit the last guess
    return Answer(None, tries=max_tries, proof=None)

# Precision is set by the checker, not by how many times we retry.
# A passing check certifies the FORMULA, never the world or the action.

The neural layer cannot be trusted to make its own safety-relevant checks: it errs silently, it is sensitive to irrelevant format changes, and its confidence is not its correctness. A deterministic symbolic layer is the natural place to put those checks for three concrete reasons — it is auditable (a model is checked by substitution, unsatisfiability by a proof), it is composable (adding a constraint does not change the core), and its contract is explicit (it guarantees exactly the specification, so what is unspecified is visibly unchecked).

1. 1Look first for a formal model of the domain that does not depend on the LLM — a schema, a validator, a simulator, business rules already encoded.
2. 2If one exists, use the model to generate and the symbolic layer to verify (generate-and-check), so the neural error becomes cost, not incorrectness.
3. 3If you must autoformalize, measure translation quality separately from final accuracy on a labelled set, and report the silent-error rate (answers emitted and wrong), not just accuracy.
4. 4Add consistency checks that use information independent of the statement (promised uniqueness, known cardinalities), and remember that retrying against them does not raise precision.
5. 5Constrain decoding to the formal language's grammar, bound the solver's time, and define the behaviour on timeout: abstain, escalate, or relax constraints.

The honest caveat is that autoformalization is the measured bottleneck. The dominant and most dangerous failure mode is an infaithful translation: a formula that is syntactically valid and semantically different from the statement, so the solver returns, with full correctness, the answer to another problem. And the most frequent failure of symbolic systems in deployment is not in the reasoner but in the specification — an omitted constraint, a flipped sign, a wrong predicate — which the reasoner cannot detect, because its contract is with the formula. The symbolic layer removes the neural layer's silent errors only to the extent that the specification is right; it relocates the risk to whoever writes the spec, which is why that spec deserves tests, independent review, or expert authorship.

Seen from reasoning, the lab's transversal thesis is this: the model proposes and interprets, and any decision with effects must pass through checks whose specification does not depend on the same model. A symbolic check that a plan respects its constraints is evidence for a decision, not the decision — and crucially, it is not an authorization to execute. Reasoning is not authorizing: whether an action is permitted is a question of policy and authority, separate from whether a formula is satisfiable.

• ▸A proof certifies the formula, not the world: the specification is the usual point of failure, and the reasoner cannot detect a wrong specification.
• ▸Formalize-and-solve relocates risk to translation; generate-and-check needs a trustworthy external model; logic-in-learning imposes nothing at inference time.
• ▸Retrying a weak filter does not improve precision; redundancy protects against independent errors, not systematic ones.
• ▸If the model writes the verifier's specification, the verifier inherits the model's errors — the guarantee becomes circular.
• ▸A satisfiable plan, a passing check, a derived proof — none of them authorize an action. Authority lives outside the reasoner, and what is unverified stays UNKNOWN, never SAFE.

Expected direction: The guarantee is the SMT checker's, and it is exactly the written invariants over an external formal model (the configuration semantics) that the model did not write — this is generate-and-check, the strong pattern, so the model's error becomes cost (a rejected candidate) rather than an incorrect approval. It does NOT hold for anything unspecified: what is not written as an invariant is not checked, so an omitted invariant is a silent gap. If the team let the model draft the invariants, it would collapse into autoformalization and the checker would inherit the model's errors, so the invariants should be written/reviewed by people and reused. Finally, "the checker passed" certifies the formula, not authorization: reasoning is not authorizing, so applying the change must still pass through an external authorization control. Until authority is established, the change is UNKNOWN-risk, not SAFE.

Why does weight editing fail to propagate consequences, and what does knowledge representation add?

Editing a fact in the weights adds it locally without closure, so dependent multi-hop facts are not updated (reported as catastrophic failure on multi-hop questions). Explicit knowledge representation adds justification, provenance, time, and coherent revision — a truth-maintenance system retracts a belief's consequences when its support falls.

State the find-versus-check asymmetry and why it matters for neuro-symbolic systems.

Checking a candidate is cheap (linear-time evaluation, or verifying a certificate) while finding a solution or proving none exists is hard (NP-complete / semi-decidable). It matters because an unreliable component can propose as long as a reliable, cheap component checks — the basis of generate-and-check.

Why is a plan from a correct planner different in kind from a plan from an LLM?

A correct planner returns a plan valid with respect to the explicit model — every precondition holds and the goal is reached — while an LLM plan carries no such guarantee. That difference of contract is what lets the system put the decision on an external, model-based validator.

Why does retrying a weak filter not improve precision in formalize-and-solve?

Precision is fixed by the ratio of uniquely-correct to uniquely-wrong translations that the filter accepts; retries only convert abstentions into answers in the same proportion of right and wrong. To raise precision you must harden the filter, not retry, and systematic errors defeat redundancy entirely.