Article · Neuro-symbolic AI

System 2 for machines

Language models are System 1 — fast, fluent, intuitive, and unable to check themselves. The next level of AI is a System 2 that reasons in logic. MLambda builds that engine.

System 2 for machines — a fast intuitive language model paired with a slow logical verifier.

Daniel Kahneman gave us the most useful map of the mind that a business audience has ever adopted: System 1, fast, automatic, associative, effortless — and System 2, slow, deliberate, logical, effortful. System 1 recognises a face, finishes a sentence, senses that something is off. System 2 checks the arithmetic, follows a proof, notices that two beliefs contradict each other. Neither is optional. A mind with only System 1 is fluent and confidently wrong; a mind with only System 2 never gets anything done.

A large language model is a System 1. That is not an insult — it is the most precise thing one can say about it, and it is the key to what it can and cannot do, and therefore to what it is worth. This article is about the missing half, why the field is now building it, and what MLambda has built.

What a language model actually is

A language model predicts the next token given the tokens before it, over a distribution learned from an enormous corpus. Everything it does — answering, coding, summarising — is that one act, repeated. The consequences are structural, not bugs to be patched:

  • It cannot verify. Verification means holding an answer against a standard independent of how the answer was produced. A model checking its own output is running the same process again; a second sample is not a second opinion. The research community has said this plainly: Kambhampati and colleagues' ICML position paper concludes that autoregressive language models cannot, by themselves, plan or self-verify — and that self-verification is, after all, a form of reasoning.
  • It cannot plan. Planning requires maintaining a state, applying rules, and rejecting branches that violate constraints. Models produce plausible-looking plans and lose track of the state that makes them valid; follow-up work found they can plan reliably only when an external system tells them what is legal at each step.
  • It does not know what it knows. Ask a model how confident it is and you receive a number produced the way every other token is produced. It has no epistemic state — no distinction between what it was told, what it inferred, and what it made up. That is the mechanism of hallucination: not a failure of the objective but a property of it. The most probable continuation is often false, and nothing in the process can tell.
  • It cannot be consistent. Two answers to two phrasings of one question can contradict each other, and the model has no representation in which the contradiction exists. Consistency is a relation between statements; a token predictor has no statements, only strings.
  • It cannot decide the undecidable, and does not know where the line is. Recent work characterising how models reason about program termination — the halting problem in miniature — finds them confidently answering questions no procedure can settle. System 1 has no sense of its own boundary.

Every one of these is a System 2 faculty. None of them arrives by scaling System 1.

Why the direction is already set

The clearest signal is what the frontier laboratories did when they wanted results that had to be right. DeepMind's AlphaGeometry pairs a language model with a symbolic deduction engine; AlphaProof pairs a model with the Lean proof assistant and a search that proves or disproves each candidate formally. Together they reached silver-medal level on the 2024 International Mathematical Olympiad — the model proposing, a formal system deciding. Reported follow-ups in 2025 pushed formal provers to gold-medal Olympiad performance and to solving every problem on the Putnam competition. None of this was achieved by a larger model alone. It was achieved by giving System 1 a System 2 that cannot be fooled.

The academic literature has converged on the same shape. Surveys of neuro-symbolic AI describe a field "gaining renewed attention as a way to overcome the limitations of large language models in complex reasoning"; the LLM-Modulo framework formalises the arrangement — the model generates, external verifiers and critics decide, and the loop continues until the verifiers are satisfied. Work on enterprise agents reports large gains from grounding a model in an ontology — typed knowledge with rules — over plain retrieval. And Gary Marcus, the field's most persistent critic of scale-alone, points to AlphaProof as the demonstration that the future is hybrid.

For an investor this is the important paragraph. The question is no longer whether AI needs a symbolic System 2. The question is who builds one that is general enough to sit under a business, not just a maths competition — and that is a systems-engineering problem, not a model-training problem.

What a System 2 for machines has to be

Stated without jargon, a System 2 must be able to do four things to what System 1 proposes:

  1. Type it — decide what kind of thing a claim is about, and reject claims that mix kinds: a duty owed by a number, a person who is also a company. This is sortal logic.
  2. Qualify it — distinguish what is known from what is believed, and by whom; what must be from what merely is; what is obligatory from what is permitted; what holds now from what must eventually hold. These are the epistemic, alethic, deontic and temporal modal logics, and they are exactly the distinctions a business runs on.
  3. Check it — for consistency with everything already admitted, and against invariants that must never be violated, exhaustively rather than by sampling.
  4. Explain it — return the proof behind a yes, the counterexample behind a no, and an honest "I don't know" when neither exists.

The engine MLambda built

This is what Thinker — the reasoning layer inside Turing — is, and what makes it a System 2 rather than another prompt. Knowledge is held as an ontology with a written formal semantics: an ontological network of kinds and duties, a semantic network of things, a statement language stratified into facts, a sortal layer, and a modal layer. Rules and facts are expressed in Shin, a rule language whose engine carries four families of modal logic — epistemic (S5), deontic (KD), temporal (LTL), alethic — plus forward and backward chaining, truth maintenance, abduction and explanation. Nothing a model proposes enters the knowledge base until it passes an admission gate: well-formed, correctly sorted, consistent with what is already there.

The visible result is that every answer carries a verdict a System 1 cannot produce: Known (provable from confirmed axioms), Believed with a confidence equal to its weakest link, Unknown, or Contradicted — with a proof or citations attached, and with provenance: who believes this, and why. The system knows what it knows, how well, and from whom, because that knowledge is a data structure rather than a feeling. Underneath, for the questions that are about software itself, sits a native TLA+ model checker that enumerates every reachable state of a specification and returns a certified counterexample when one exists.

The division of labour is the one the research points to, made operational: the language model gathers; the proofs decide. System 1 is used everywhere and trusted nowhere. That is not a limitation on the model. It is the arrangement that makes the model usable for anything that has to be right.

What this is worth, and to whom

A System 2 is worth money exactly where a wrong answer costs money. Regulated industries, where an auditor asks for evidence rather than confidence. Financial systems, where a plausible trade is not the same as a valid one. Logistics, where a contract that drifts costs real vehicles real hours. And software engineering itself — the domain where the standard of correctness is already formal, and where MLambda's Turing applies this engine to turn requirements into verified systems, with the model helping define the requirement and never writing the code.

The commercial claim is modest and checkable: MLambda does not sell a smarter model. It sells the faculty that makes any model's output admissible — the typing, qualifying, checking and explaining that turn a fluent guess into a claim with a status. Every model on the market is a System 1. The System 2 is the scarce part, and it is engineered, not trained.

The scientific spirit, kept

Two honesties, so that the argument does not overreach. First, "neuro-symbolic" is a direction with open problems: how much of the symbolic layer can be learned rather than written, how to keep formalisation from becoming a bottleneck, and how far ontological grounding generalises beyond the domains it was built for — MLambda's own research line, Hilbert, exists because those questions are unsettled. Second, a System 2 is only as good as the knowledge admitted into it; the gate can refuse the ill-formed and the contradictory, but a consistent falsehood that no axiom contradicts will pass. That is why provenance and human-grounded axioms are part of the design rather than decoration. Kahneman's point was never that System 2 is infallible. It was that without it, System 1 does not know when it is wrong — and neither, today, does a language model on its own.

Sources

Thinker and the expert society are part of Turing; Shin and the TLA+ checker are Genesis packages. Related: The LLM never answers · Context that has been proved · The intelligence LLMs are missing. Request a demonstration.