> For the complete documentation index, see [llms.txt](https://neurosymbolicai.gitbook.io/neuro-symbolic-ai-in-practice/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://neurosymbolicai.gitbook.io/neuro-symbolic-ai-in-practice/part-iii-core-approaches/chapter-4/4-3-hybrid-architectures/4-3-system1-system2.md). # 4.3.1 System 1 / System 2 — AlphaProof > *The neural component thinks fast; the symbolic component reasons carefully. Together, they produce answers that neither could verify alone.* *** **Definition:** A neural network provides fast, intuitive, parallel processing (System 1), while a symbolic reasoning engine provides slow, deliberate, serial reasoning (System 2). The two systems communicate through a structured interface.(Booch et al., 2021)(Marcus, 2020) This architecture is directly inspired by the dual-process theory of human cognition (Kahneman, 2011) — the observation that human thinking operates in two qualitatively different modes: * **System 1:** Fast, automatic, unconscious, pattern-based. Drives immediate perceptual responses, facial recognition, chess intuition. * **System 2:** Slow, deliberate, effortful, rule-following. Drives logical deduction, mathematical reasoning, careful planning. Human intelligence benefits enormously from both. Expert chess players use System 1 to rapidly narrow candidate moves to a handful, then System 2 to calculate consequences. Without System 1, the combinatorial explosion of possibilities is unmanageable. Without System 2, System 1's intuitions lead to systematic errors. The same complementarity applies in AI: | Property | Neural (System 1) | Symbolic (System 2) | | ------------ | ------------------------ | -------------------------- | | Speed | Milliseconds | Seconds to hours | | Input | Raw sensor data | Structured symbols | | Output | Continuous distributions | Discrete, verified results | | Knowledge | Implicit, distributed | Explicit, queryable | | Correctness | Statistical | Provable | | Failure mode | Hallucination | Brittleness | ### Architecture ``` ┌──────────────────────────────────────────────────────┐ │ Hybrid System │ │ │ │ Raw Inputs (images, text, sensor streams) │ │ │ │ │ ▼ │ │ ┌─────────────────────────────┐ │ │ │ Neural System 1 │ Fast perception │ │ │ (CNN / Transformer) │ Pattern matching │ │ └─────────────────────────────┘ │ │ │ Structured intermediate │ │ │ representation │ │ ▼ │ │ ┌─────────────────────────────┐ │ │ │ Symbolic System 2 │ Deliberate search │ │ │ (Planner / Theorem Prover) │ Formal reasoning │ │ └─────────────────────────────┘ │ │ │ Verified output │ │ │ + Feedback signal │ │ ▼ │ │ Neural system updated (fine-tuning / RLHF) │ └──────────────────────────────────────────────────────┘ ``` The neural-to-symbolic interface is the critical engineering challenge: transforming continuous neural representations into discrete symbolic structures that the reasoning engine can operate on. Scene graphs, PDDL problem files, Lean proof contexts, and knowledge graph triples are all examples of such structured interfaces. The symbolic-to-neural feedback enables the neural component to improve over time: successful symbolic solutions are used as supervision signals to fine-tune the neural component, enabling progressive improvement without ground-truth labels. ### Implementation Example: AlphaProof Deep Dive **AlphaProof** (AlphaProof Team et al., 2024) is the most complete realization of the System 1 / System 2 architecture for formal reasoning.(AlphaProof Team et al., 2024) **System 1 — The Policy and Value Networks:**\ A **fine-tuned Gemini language model** serves as the proof-step generator, trained on a large corpus of Lean 4 proofs from the mathlib library.(AlphaProof Team et al., 2024) Given a proof context (current hypotheses + goal), it predicts a probability distribution over Lean 4 tactics — the action space of formal proof. A separate value network estimates the probability that the current proof context is solvable within the remaining computation budget. **System 2 — Lean 4 + MCTS:**\ Lean 4 is a dependently typed proof assistant and programming language. Its type checker is sound and practically terminating — it either accepts a proof step as valid or rejects it with an error. (The Lean 4 kernel is engineered to always terminate on submitted proof terms via structural termination checking; the formal decidability of the full type theory, including its universe hierarchy and classical axioms, remains an active area of metatheory research.) This is the symbolic oracle. > **Note on formal guarantees:** *Sound* means every accepted proof is valid; *practically terminating* means the type checker is engineered to always terminate on submitted proof terms. Lean 4's type theory is not Gödel-complete — no sufficiently expressive formal system can prove all true mathematical statements (Gödel's incompleteness theorems). Soundness and practical termination are the relevant guarantees for a verified AI system. An **AlphaZero-inspired MCTS-based RL approach** — using PUCT selection (policy network prior P(s,a) weights exploration) rather than random rollouts — drives the proof search. The language model generates candidate tactic sequences, Lean 4 verifies each step, and successful proofs reinforce the model via RL. This self-improving loop, borrowed conceptually from AlphaZero's self-play but adapted to the single-player formal proof domain, is what enables AlphaProof to solve progressively harder problems.(AlphaProof Team et al., 2024) * **State:** A Lean 4 proof context (goal stack + hypotheses). * **Action:** A Lean 4 tactic (e.g., `ring`, `linarith`, `simp`, `apply lemma_name`). * **Transition:** Applying a tactic transforms the proof context, possibly splitting it into multiple sub-goals or closing the goal. * **Terminal state:** All goals closed (proof complete) or budget exhausted (failure). * **Reward:** +1 for complete proof, 0 otherwise. **The Self-Improvement Loop:**\ Training data begins from the **mathlib** library — the largest mathematical library in the Lean 4 ecosystem, containing thousands of verified proofs across algebra, topology, analysis, and combinatorics. The policy network is pre-trained on these proofs. Then, the AlphaZero RL loop begins: 1. For each problem statement, the language model generates candidate tactic sequences; Lean 4 verifies each step. 2. If a proof is found, Lean 4 verifies it completely. 3. Verified proofs are added to the training corpus as new data. 4. The model is fine-tuned on the augmented corpus. 5. Repeat — each iteration, the system can solve harder problems, generating training data that further improves the model. This self-improving feedback loop is the key to AlphaProof's ability to solve problems at IMO competition level — a level that requires multi-step mathematical creativity at a level surpassing most PhD mathematicians. > **Silver medal performance at IMO 2024:** AlphaProof (combined with AlphaGeometry 2 for geometry problems) solved 4 out of 6 problems from the 2024 International Mathematical Olympiad — running for minutes on one problem and up to three days on others, equivalent to a silver medal score. Of the four, **AlphaProof solved Problems 1, 2, and 6** (algebra and number theory) and **AlphaGeometry 2 solved Problem 4** (a Euclidean geometry problem, using a distinct neuro-symbolic architecture without MCTS over Lean proof states).(AlphaProof Team et al., 2024) This is the first time any AI system achieved competition-level performance on IMO problems.(AlphaProof Team et al., 2024) *Reference:*\ AlphaProof Team and AlphaGeometry Team, DeepMind. "AI Achieves Silver-Medal Standard Solving International Mathematical Olympiad Problems." *DeepMind Technical Report*, 2024. ### AlphaGeometry — A Parallel Architecture for Geometry > **Note on versions:** The system described here and cited as (Trinh et al., 2024) is **AlphaGeometry 1**, published in *Nature* in January 2024. **AlphaGeometry 2** is an enhanced successor described in a 2024 DeepMind technical report; it solved all 30 IMO geometry test problems and was the system deployed for IMO 2024. The architectural description below applies to both generations; the performance figures (25/30 problems) refer to AlphaGeometry 1. The IMO 2024 silver medal callout box refers to AlphaGeometry 2. **AlphaGeometry** (Trinh et al., 2024) was published alongside AlphaProof and solves the same challenge domain (IMO competitions) but with a fundamentally different architecture — making the comparison instructive. AlphaGeometry's architecture: * **Neural component:** A language model trained on 100M synthetic geometry theorems (generated by the symbolic engine). Given a geometry problem statement, the LM proposes **auxiliary constructions** — adding new points, lines, or circles to the diagram that are not in the original problem statement but make the proof tractable. * **Symbolic component:** A classical geometry deduction engine implementing a **Deductive Database with Algebraic Rules (DDAR)** — a symbolic engine that chains inference rules for angle chasing, ratio chasing, and algebraic manipulations over geometric constructions. Given the original diagram enriched with the LM's auxiliary construction, it exhaustively derives consequences until the goal is proved or the budget is exhausted. **The key architectural insight — different from AlphaProof:** | Dimension | AlphaProof | AlphaGeometry | | --------------- | ------------------------------------- | ------------------------------- | | Formal language | Lean 4 tactics | Euclidean geometry rules | | Neural role | Tactic generator in AlphaZero RL loop | Auxiliary construction proposer | | Verification | Lean 4 type checker | Deduction engine | | Self-play loop | Yes (online RL training) | No (synthetic corpus) | | Search | AlphaZero RL over proof states | Beam search over constructions | AlphaGeometry is an instance of the **"Neural Helps Symbolic"** pattern (§4.2) rather than the hybrid loop of AlphaProof: the neural component makes a one-shot proposal that the symbolic engine either accepts (and continues) or rejects. There is no iterative neural-symbolic back-and-forth. **Results:** Solved 25 of 30 IMO geometry problems from the approximately 2000–2022 problem set, matching average gold-medallist performance on geometry. Combined with AlphaProof's algebra/analysis performance, the system achieved silver-medal level overall at IMO 2024. *Reference:* Trinh, Trieu H., et al. "Solving Olympiad Geometry Without Human Demonstrations." *Nature* 625 (2024): 476–482. | Code: *** ## References 2. Booch, Grady, et al. "Thinking Fast and Slow in AI." *Proceedings of AAAI 2021*. 3. Marcus, Gary. "The Next Decade in AI: Four Steps Towards Robust Artificial Intelligence." *arXiv preprint* arXiv:2002.06177 (2020). 4. Kahneman, Daniel. *Thinking, Fast and Slow*. Farrar, Straus and Giroux, 2011. ISBN: 978-0374533557. 5. AlphaProof Team and AlphaGeometry Team, DeepMind. "AI Achieves Silver-Medal Standard Solving International Mathematical Olympiad Problems." *DeepMind Technical Report*, 2024. 6. Trinh, Trieu H., et al. "Solving Olympiad Geometry Without Human Demonstrations." *Nature* 625 (2024): 476–482. | Code: --- # Agent Instructions This documentation is published with GitBook. GitBook is the documentation platform designed so that both humans and AI agents can read, navigate, and reason over technical content effectively. Learn more at gitbook.com. ## Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter, and the optional `goal` query parameter: ``` GET https://neurosymbolicai.gitbook.io/neuro-symbolic-ai-in-practice/part-iii-core-approaches/chapter-4/4-3-hybrid-architectures/4-3-system1-system2.md?ask=&goal= ``` `ask` is the immediate question: it should be specific, self-contained, and written in natural language. `goal` is optional and describes the broader end goal you are ultimately trying to accomplish on behalf of the user. GitBook uses it to tailor the answer towards what is most useful for that goal. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.