Neurosymbolic AI

Combining neural networks (pattern recognition, language understanding, probabilistic reasoning) with symbolic systems (logic solvers, constraint satisfaction, graph traversal, formal verification). The neural side handles ambiguity and natural language; the symbolic side handles exhaustive computation and provable correctness.

Why combine them

Neural models are good at understanding intent, handling noisy input, and generating plausible answers. They're bad at exhaustive search, guaranteed correctness, and multi-step formal reasoning — they hallucinate paths that don't exist and miss paths that do.

Symbolic systems are the opposite. A Prolog solver will find every valid path through a call graph, but it can't parse a natural language question or decide which query to run. Putting them together lets each system do what it's good at.

The pattern in practice

The typical architecture: the neural model acts as a front-end that interprets the user's question and translates it into a formal query, then a symbolic solver executes the query and returns a guaranteed-correct result. The LLM never touches the computation — it's a translator and presenter.

chiasmus is a clean example. The LLM decides "the user wants to know if user input can reach this SQL query," formulates a reachability query, and calls the MCP tool. Tree-sitter parses the code into an AST, Prolog facts encode the call graph, and Prolog's backtracking finds all paths (or proves none exist). The answer comes from the solver, not the model.

Where it shows up

• Code analysis — chiasmus uses tree-sitter + Prolog for reachability, dead code, impact analysis
• Math reasoning — LLMs translating word problems into symbolic math, then calling a CAS (Wolfram, SymPy) to solve
• Planning — LLMs generating PDDL domain descriptions, then classical planners finding optimal action sequences
• Database queries — text-to-SQL where the LLM generates the query and the database engine guarantees correct execution
• Formal verification — LLMs generating proof sketches, proof assistants (Lean, Coq) verifying them
• Constraint puzzles — sudoku encoded as a graph 9-coloring or as a polynomial ideal, then handed to a backtracking or Gröbner-basis solver (chalkdust-sudoku-secrets)

Token economics

Beyond correctness, there's a practical cost argument. Symbolic solvers run locally and consume zero tokens. An LLM doing five rounds of grep-and-reason to trace a call chain costs ~2,500 tokens and might miss paths. A single tool call to a symbolic solver costs ~200 tokens and is exhaustive. The more computation you can offload to deterministic local tools, the cheaper and more reliable the system becomes.

Tension with end-to-end learning

The deep learning community has historically favored end-to-end approaches — train one big model to do everything, no hand-crafted components. Neurosymbolic AI pushes back: some problems have known-correct algorithms, and running them is cheaper and more reliable than training a model to approximate them. The question is where to draw the boundary between the neural and symbolic parts.