Neurosymbolic AI

Definition. Neurosymbolic (neuro-symbolic, NeSy) AI combines neural networks (learning from data, perception, language) with symbolic methods (logic, rules, knowledge graphs, planners, theorem provers) so a system can learn and also reason with explicit, checkable structure. d’Avila Garcez and Lamb framed it as the “3rd wave” of AI, aiming at robust learning plus reasoning and explainability (arXiv 2012.05876, December 2020).

Common integration patterns

• Neural perception, symbolic reasoning: a vision or language model produces structured facts that a rule engine or planner consumes.
• Neural-guided search: a model proposes steps (proofs, programs, plans) and a symbolic engine searches or verifies them.
• Symbolic constraints on learning: logic-based losses or rules supervise a network (differentiable logic, e.g. Logic Tensor Networks, DeepProbLog).
• Generate and verify: an LLM drafts, a formal checker (type checker, SMT solver, proof assistant, unit tests) accepts or rejects. In the author’s view this is the pattern that has scaled most visibly in 2025-2026.

2025-2026 examples (dated, sourced)

• AlphaProof (Google DeepMind): an AlphaZero-style reinforcement-learning agent that finds formal proofs in the Lean prover, trained on about 80 million auto-formalised problems; it solved three of five problems at IMO 2024 (silver level, per search results). The method paper “Olympiad-level formal mathematical reasoning with reinforcement learning” appeared in Nature in November 2025 (doi 10.1038/s41586-025-09833-y; publication month per search results, the page itself was not readable).
• Aristotle (Harmonic): combines Lean proof search, an informal lemma-based reasoning pipeline and a geometry solver; the Harmonic team reports gold-medal-equivalent performance on IMO 2025 with solutions verified in Lean 4 (arXiv 2510.01346, 2025-10-01).
• The wider pattern is “LLM plus formal verifier” in maths and verified code. Agentic coding loops that run tests and linters before accepting changes are a lightweight form of it (loop-engineering, graph-engineering). Knowledge-graph grounding of LLMs relates to ontology, resource-description-framework and owl.

Why it matters, and limits

• Explanations and verifiable outputs: a proof or rule trace can be checked, a neural score cannot.
• Hallucination control: symbolic checks reject invalid outputs.
• Costs: formalising a domain is labour-intensive, symbolic search scales poorly on large knowledge bases, and translating between embeddings and symbols is lossy. Reported gains are domain-specific (maths, code, planning); the author is not aware of a general NeSy system that has displaced plain LLMs for open-ended tasks (opinion, not surveyed).

Related: neural-networks, machine-learning, large-language-model, future-trends-in-ai.

Open items

• DeepProbLog and Logic Tensor Networks are named from general knowledge; their papers were not re-opened. Industry neurosymbolic products were not surveyed.

Sources (fetched 2026-10-05)

• https://arxiv.org/abs/2012.05876
• https://arxiv.org/abs/2510.01346
• https://www.nature.com/articles/s41586-025-09833-y (blocked by redirect; details via search results 2026-10-05)