What is neurosymbolic AI?

Neurosymbolic AI is the convergence of Neural Networks (deep learning, LLMs) and Symbolic Reasoning (logic, mathematics, formal methods).

The two paradigms

1. Neural (subsymbolic)

Examples: GPT-4, Claude, Llama
Strength: Pattern recognition, language understanding, creativity
Weakness: Cannot prove correctness, prone to hallucinations
Output: Probabilistic (unverified correctness)

2. Symbolic

Examples: Z3 (SAT Solver), SymPy (Computer Algebra), Prolog (Logic Programming)
Strength: Deterministic reasoning, mathematical proof
Weakness: Cannot understand natural language
Output: Deterministic (proven correct)

The neurosymbolic synthesis

QWED bridges both worlds:

Natural Language Query
         ↓
    LLM (Neural)
    "Translates to formal logic"
         ↓
   Symbolic Solver
   "Proves correctness"
         ↓
   Verified Result

Example: User Query: “What is the derivative of x²?” Neural Step (GPT-4):

LLM translates to SymPy code:
>>> from sympy import symbols, diff
>>> x = symbols('x')
>>> diff(x**2, x)

Symbolic Step (SymPy):

Result: 2*x  # Mathematically proven

QWED verifies: ✅ LLM said “2x”, SymPy proves “2x” → Verified!

Why neurosymbolic wins

Problem: LLM-only systems

Scenario: Healthcare AI diagnoses patient

GPT-4: "Give aspirin (contraindicated with warfarin)"
      ↓
 NO VERIFICATION
      ↓
  ☠️ Patient harm

Solution: QWED (neurosymbolic)

GPT-4: "Give aspirin"
      ↓
Medical Logic Engine: Checks drug interaction database
      ↓
Z3 Solver: Proves "aspirin + warfarin = contraindicated"
      ↓
🛑 BLOCKED + Alert doctor

Research background

Neurosymbolic AI is backed by leading research:

Google DeepMind: AlphaProof (math theorem proving)
MIT CSAIL: Neurosymbolic programming
IBM Research: Neuro-symbolic learning

QWED is the first open-source implementation focused on LLM verification.

QWED’s neurosymbolic architecture

Neural components (untrusted translators)

OpenAI GPT-4
Anthropic Claude
Google Gemini
Ollama (Local LLMs)

Symbolic components (trusted verifiers)

SymPy → Math verification
Z3 → Logic verification
Python AST → Code security verification

The contract

Component	Role	Trust Level
LLM	Translate natural language → formal logic	⚠️ Untrusted
Symbolic Solver	Execute logic, prove result	✅ Trusted

Comparison: symbolic vs neural vs neurosymbolic

Approach	Understands Language?	Proves Correctness?	QWED Uses
Symbolic Only	❌ No	✅ Yes	Verification engines
Neural Only	✅ Yes	❌ No	Translation step
Neurosymbolic	✅ Yes	✅ Yes	✅ Both combined!

Real-world impact

Finance example

Old Way (LLM-only):

GPT: "Investment return = 12.5%"
→ Trust blindly
→ $12,889 error (from benchmark)

QWED Way (Neurosymbolic):

GPT: "Investment return = 12.5%"
→ SymPy calculates: 11.8%
→ 🛑 Mismatch detected!
→ ✅ Corrected before loss

Code security example

Old Way:

GPT: "Here's the code"
```python
eval(user_input)  # Dangerous!

→ No check → 🔓 Security breach


**QWED Way:**

GPT: “Here’s the code” → AST analyzer detects ‘eval’ → 🛑 UNSAFE CODE → ✅ Blocked before execution

---

## Why "neurosymbolic" matters for QWED

- The term has an established academic definition: neural plus symbolic.
- QWED meets that definition: LLMs (neural) plus SymPy and Z3 (symbolic).
- The architecture aligns with active research directions in AI verification.

---

## Further reading

- [Neurosymbolic AI - MIT](https://arxiv.org/abs/2305.00813)
- [DeepMind AlphaProof](https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/)
- [IBM Neurosymbolic AI](https://research.ibm.com/topics/neurosymbolic-ai)

---

**QWED: Where Neural Networks meet Mathematical Proof.** 🧠🔬

Architecture

Concepts

Specifications

Integration Patterns

Contributing

The two paradigms

1. Neural (subsymbolic)

2. Symbolic

The neurosymbolic synthesis

Why neurosymbolic wins

Problem: LLM-only systems

Solution: QWED (neurosymbolic)

Research background

QWED’s neurosymbolic architecture

Neural components (untrusted translators)

Symbolic components (trusted verifiers)

The contract

Comparison: symbolic vs neural vs neurosymbolic

Real-world impact

Finance example

Code security example

​The two paradigms

​1. Neural (subsymbolic)

​2. Symbolic

​The neurosymbolic synthesis

​Why neurosymbolic wins

​Problem: LLM-only systems

​Solution: QWED (neurosymbolic)

​Research background

​QWED’s neurosymbolic architecture

​Neural components (untrusted translators)

​Symbolic components (trusted verifiers)

​The contract

​Comparison: symbolic vs neural vs neurosymbolic

​Real-world impact

​Finance example

​Code security example

The two paradigms

1. Neural (subsymbolic)

2. Symbolic

The neurosymbolic synthesis

Why neurosymbolic wins

Problem: LLM-only systems

Solution: QWED (neurosymbolic)

Research background

QWED’s neurosymbolic architecture

Neural components (untrusted translators)

Symbolic components (trusted verifiers)

The contract

Comparison: symbolic vs neural vs neurosymbolic

Real-world impact

Finance example

Code security example