Skip to content

CONCEPT Cited by 2 sources

Neurosymbolic AI

Definition

Neurosymbolic AI is the composition of neural methods (LLMs, transformers, RL) with symbolic methods (mechanical theorem provers, SAT/SMT solvers, formal reasoners). Done right, the two complement each other: symbolic tools bring mathematical rigor and provable correctness, neural tools bring dramatic ease-of-use, natural-language interfaces, and heuristic guidance through hard search spaces.

The only way to deliver that much-needed trust is through neurosymbolic AI, i.e. the combination of neural networks together with the symbolic procedures that provide the mathematical rigor that automated reasoning enjoys. — Byron Cook (Source: sources/2026-02-17-allthingsdistributed-byron-cook-automated-reasoning-trust-ai)

Why now

Cook names two mutually-reinforcing forces since 2022:

  1. LLMs are trained over theorem-prover outputs. This is the nontrivial part: modern LLMs are frequently trained on Lean/Isabelle/HOL-light proofs and their surrounding math corpora, so asking them to use provers is no longer friction-dominated.
  2. Production AI cannot be trusted without symbolic guarantees. Pure-generative outputs in high-stakes domains (agentic banking, regulatory zoning, safety-critical code) have no mathematical floor. Symbolic composition provides the floor.

Four named composition shapes

(From sources/2026-02-17-allthingsdistributed-byron-cook-automated-reasoning-trust-ai)

  1. RL-over-prover. Combine a theorem prover with reinforcement learning; the prover is the reward signal. DeepSeek is the public exemplar; the systems/lean prover is the target (Lean's founder Leo de Moura is at Amazon).
  2. Post-inference verification. LLM generates → symbolic reasoner checks the output against a specification → filter / regenerate / gate. systems/bedrock-guardrails-automated-reasoning-checks is the canonical AWS product. See patterns/post-inference-verification.
  3. Tool-cooperation inside agents. The prover is a first-class tool the agent calls mid-task, not a post-hoc filter. systems/kiro and Amazon Nova are named as surfaces.
  4. Envelope + composition reasoning. For multi-agent systems: specify each agent's envelope, mechanically restrict it with systems/bedrock-agentcore, then reason about the composition of those envelopes against global invariants. See patterns/envelope-and-verify.

Poetry vs banking: the stakes spectrum

Cook's design heuristic: "Every solution to a problem should be as simple as possible, but no simpler" (Einstein). Customer needs are multidimensional; neurosymbolic rigor is not free. The heuristic:

  • Writing poetry with generative AI — no trust required, pure generative is fine.
  • Agentic banking, healthcare, regulated industries — trust is non-negotiable; you must specify the envelope, restrict the agent to it, and reason about the composition.

Cost of reasoning scales with the required safety floor. Pick the floor.

Ecosystem: who is building it

AWS + Amazon (Cook's team across Kiro, Amazon Nova, Bedrock Guardrails, AgentCore) is one node. Cook calls out a broader set:

  • Large model builders pushing neurosymbolic: DeepSeek, DeepMind/Google.
  • Startups in the space (as of 2026-02): Atalanta, Axiom Math, Harmonic.fun, Leibnitz.
  • Public research: DARPA's expMath program, centered on autoformalization (natural-language → formal-spec translation, the current bottleneck).

Why this shape (and not just "more/better LLMs")

  • LLMs alone cannot prove. They can produce outputs that look correct; proof requires a mechanically-checked witness. Only symbolic tools produce that.
  • Symbolic tools alone are expert-gated. The last 50 years of theorem-prover research produced genuinely powerful tools that very few people could use. Neural front-ends dissolve that wall.
  • The combination is greater than either alone. LLMs drive proof search when algorithms get stuck. Provers catch LLM hallucinations before they reach production.

Corollary: specification becomes mainstream

A second-order effect of neurosymbolic tooling: as products like Kiro and Bedrock Guardrails land, customers start demanding specification languages from their tools. Cook predicts the customer-visible surface will expand to include:

  • Branching-time vs linear-time temporal logic
  • Past-time vs future-time operators
  • Logic of knowledge and belief (epistemic)
  • Causal reasoning

See concepts/specification-driven-development and concepts/temporal-logic-specification. The old regime (specs are an expert artifact produced once and discarded) is giving way to specs as live customer-visible inputs.

Seen in

Last updated · 200 distilled / 1,178 read