feat: implement System 3 AI Reasoning Graph and Neuro-Symbolic Engine

crates/synapse-core/src/logic/metabolism.rs

@@ -4,6 +4,7 @@ use crate::{MemoryNode, NodeType};
 use std::sync::Arc;
 use chrono::Utc;
 use uuid::Uuid;
+use crate::logic::system3::{NeuroSymbolicEngine, ReasoningGraph, LogicNode, LogicNodeType};
 
 /// Metabolism: The process of digesting short-term buffer into long-term memory.
 ///
@@ -20,6 +21,7 @@ pub struct Metabolism {
     holographic: Arc<dyn HolographicPort>,
     sanitizer: Arc<dyn SanitizerPort>,
     threshold: usize,
+    neuro_symbolic: Option<Arc<NeuroSymbolicEngine>>,
 }
 
 impl Metabolism {
@@ -40,9 +42,16 @@ impl Metabolism {
             holographic,
             sanitizer,
             threshold: 10, // Default threshold
+            neuro_symbolic: None,
         }
     }
 
+    /// Enable System 3 validation using the Neuro-Symbolic Engine
+    pub fn with_system3(mut self, engine: Arc<NeuroSymbolicEngine>) -> Self {
+        self.neuro_symbolic = Some(engine);
+        self
+    }
+
     /// Push a new interaction to the short-term buffer.
     pub async fn push_interaction(&self, interaction: crate::Interaction) -> Result<()> {
         self.buffer.push(interaction).await
@@ -98,6 +107,59 @@ impl Metabolism {
         // 4. Summarize via LLM
         let summary = self.llm.summarize(&combined_text).await?;
 
+        // System 3 Validation: Ensure the summary reasoning does not contain hallucinations
+        if let Some(engine) = &self.neuro_symbolic {
+            // Very simplified: Generate a mock Reasoning Graph for the summary logic
+            // In a real scenario, the LLM should output the ReasoningGraph directly.
+            let mut graph = ReasoningGraph::new();
+            graph.add_node(LogicNode::new(
+                "1".to_string(),
+                LogicNodeType::Conclusion,
+                summary.clone(),
+                Some(summary.clone()) // Passing the summary directly as a translation to verify
+            ));
+
+            let is_sound = engine.evaluate_graph(&mut graph).await.unwrap_or(false);
+            if !is_sound {
+                // For MVP: Return error or silently drop/flag the invalid memory
+                // We'll log and skip digestion if the logic is flawed
+                println!("System 3 Validation Failed: Hallucination detected in memory digestion.");
+                return Ok(0);
+            }
+
+            // 5. Generate embedding
+            let embedding = self.embedder.embed(&summary).await?;
+
+            // 6. Diffuse validated logic into Holographic Memory
+            // Convert the discrete reasoning into a continuous latent representation (Diffusion / Entropy Injection)
+            let serialized_graph = serde_json::to_string(&graph).unwrap_or_default();
+            let neurogram = match self.holographic.diffuse_logic(&serialized_graph).await {
+                Ok(data) => Some(data),
+                Err(_) => None,
+            };
+
+            // 7. Store in Long-Term Memory
+            let memory = MemoryNode {
+                id: Uuid::new_v4().to_string(),
+                content: summary,
+                layer: 0,
+                node_type: crate::NodeType::Summary,
+                created_at: Utc::now().timestamp(),
+                updated_at: Utc::now().timestamp(),
+                embedding,
+                metadata: std::collections::HashMap::new(),
+                namespace: "default".to_string(),
+                source: "metabolism".to_string(),
+                holographic_data: neurogram,
+                loop_level: 0,
+            };
+
+            self.memory.store(memory).await?;
+            self.buffer.clear().await?;
+            return Ok(count);
+        }
+
+        // Fallback for non-System3 path (Continuous Mode)
         // 5. Generate embedding
         let embedding = self.embedder.embed(&summary).await?;
 

crates/synapse-core/src/logic/mod.rs

@@ -6,4 +6,5 @@ pub mod translator;
 pub mod dreaming;
 pub mod hirag;
 pub mod sanitizer;
+pub mod system3;
 // pub mod reranker;

crates/synapse-core/src/logic/system3/engine.rs

@@ -0,0 +1,136 @@
+//! The Neuro-Symbolic Engine
+//!
+//! Takes a Reasoning Graph generated by the continuous language model
+//! and deterministically verifies each node using a symbolic backend
+//! (e.g., Python math parser, Prover9 logic solver, etc.).
+//!
+//! If a node is invalid (e.g., result-oriented hallucination), it is marked
+//! Invalid, and the explicit reasoning graph provides targeted feedback
+//! for the LLM to learn or correct itself using graph-based reward thinking.
+
+use crate::error::Result;
+use crate::logic::system3::graph::{LogicNodeType, ReasoningGraph, VerificationStatus};
+use async_trait::async_trait;
+use std::sync::Arc;
+
+/// Verifier Interface (A2A-compatible in future via `rust-adk` tools).
+#[async_trait]
+pub trait SymbolicVerifierPort: Send + Sync {
+    /// Deterministically verify a formal statement.
+    /// Returns: (Is Valid, Reward Signal [0.0 - 1.0], Error Message if any)
+    async fn verify(&self, translation: &str) -> Result<(bool, f32, Option<String>)>;
+}
+
+/// A local mocked verifier for Python expressions/Math.
+/// In production, this would execute actual code or query a Prover9 solver.
+pub struct MockPythonVerifier;
+
+#[async_trait]
+impl SymbolicVerifierPort for MockPythonVerifier {
+    async fn verify(&self, translation: &str) -> Result<(bool, f32, Option<String>)> {
+        // Very basic mock:
+        if translation.contains("invalid") || translation.contains("False") {
+            return Ok((false, 0.0, Some("Failed validation check".to_string())));
+        }
+        // Simulating objective, unfalsifiable code-based reward signal (ImpRIF)
+        Ok((true, 1.0, None))
+    }
+}
+
+pub struct NeuroSymbolicEngine {
+    verifier: Arc<dyn SymbolicVerifierPort>,
+}
+
+impl NeuroSymbolicEngine {
+    pub fn new(verifier: Arc<dyn SymbolicVerifierPort>) -> Self {
+        Self { verifier }
+    }
+
+    /// Evaluates the entire reasoning graph step-by-step.
+    /// Returns true if all nodes are logically sound.
+    pub async fn evaluate_graph(&self, graph: &mut ReasoningGraph) -> Result<bool> {
+        if !graph.is_acyclic() {
+            // Cannot evaluate a cyclic graph
+            return Ok(false);
+        }
+
+        // In a real DAG, we would topological sort. For now, we iterate.
+        // A graph is considered sound if all Operations and Conclusions are valid.
+        let mut overall_soundness = true;
+
+        for node in graph.nodes.values_mut() {
+            if node.node_type == LogicNodeType::Knowledge || node.node_type == LogicNodeType::Requirement {
+                // Premises are assumed valid or validated differently.
+                node.status = VerificationStatus::Valid;
+                node.reward = 1.0;
+                continue;
+            }
+
+            if let Some(translation) = &node.formal_translation {
+                let (is_valid, reward, _err) = self.verifier.verify(translation).await?;
+                if is_valid {
+                    node.status = VerificationStatus::Valid;
+                    node.reward = reward;
+                } else {
+                    node.status = VerificationStatus::Invalid;
+                    node.reward = 0.0;
+                    overall_soundness = false;
+                }
+            } else {
+                // If there's no formal translation for an operation, we can't objectively verify it.
+                node.status = VerificationStatus::Invalid;
+                node.reward = 0.0;
+                overall_soundness = false;
+            }
+        }
+
+        Ok(overall_soundness)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::logic::system3::graph::{LogicNode, LogicNodeType};
+
+    #[tokio::test]
+    async fn test_valid_reasoning_graph() {
+        let mut graph = ReasoningGraph::new();
+
+        let mut node1 = LogicNode::new("1".to_string(), LogicNodeType::Knowledge, "x = 5".to_string(), Some("x = 5".to_string()));
+        let mut node2 = LogicNode::new("2".to_string(), LogicNodeType::Operation, "x * 2 = 10".to_string(), Some("assert x * 2 == 10".to_string()));
+        node2.add_dependency("1".to_string());
+
+        graph.add_node(node1);
+        graph.add_node(node2);
+
+        let verifier = Arc::new(MockPythonVerifier);
+        let engine = NeuroSymbolicEngine::new(verifier);
+
+        let is_sound = engine.evaluate_graph(&mut graph).await.unwrap();
+        assert!(is_sound);
+    }
+
+    #[tokio::test]
+    async fn test_invalid_reasoning_graph_hallucination() {
+        // Testing "Result-Oriented Hallucination" prevention.
+        let mut graph = ReasoningGraph::new();
+
+        let mut node1 = LogicNode::new("1".to_string(), LogicNodeType::Knowledge, "x = 5".to_string(), Some("x = 5".to_string()));
+        let mut node2 = LogicNode::new("2".to_string(), LogicNodeType::Operation, "x * 2 = 12".to_string(), Some("invalid assert x * 2 == 12".to_string()));
+        node2.add_dependency("1".to_string());
+
+        graph.add_node(node1);
+        graph.add_node(node2);
+
+        let verifier = Arc::new(MockPythonVerifier);
+        let engine = NeuroSymbolicEngine::new(verifier);
+
+        let is_sound = engine.evaluate_graph(&mut graph).await.unwrap();
+        assert!(!is_sound);
+
+        let node2_eval = graph.get_node("2").unwrap();
+        assert_eq!(node2_eval.status, VerificationStatus::Invalid);
+        assert_eq!(node2_eval.reward, 0.0);
+    }
+}

crates/synapse-core/src/logic/system3/graph.rs

@@ -0,0 +1,149 @@
+//! # System 3 AI - Reasoning Graph & Neuro-Symbolic Engine
+//!
+//! This module implements the "System 3 AI" paradigm described by the `LogicGraph` and `ImpRIF` models.
+//!
+//! ## Overview
+//! Current LLMs (System 1/2) suffer from "Result-Oriented Hallucination". They prioritize semantic fluency
+//! over logical soundness. To fix this, System 3 AI transitions from continuous differentiable spaces
+//! to discrete logical graphs (DAGs).
+//!
+//! A reasoning process is split into discrete `LogicNode`s. Instead of generating text autoregressively,
+//! the LLM generates a logic graph. Each node's validity is evaluated by a deterministic `NeuroSymbolicVerifier`
+//! (e.g., Python code execution, Prover9, Lean4 solver).
+//!
+//! The graph explicitly tracks:
+//! - Semantic knowledge nodes
+//! - Relationships
+//! - Operations
+//! - Requirements/Dependencies
+
+use serde::{Deserialize, Serialize};
+use std::collections::{HashMap, HashSet};
+
+/// Types of logic nodes in the reasoning graph.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+pub enum LogicNodeType {
+    /// Semantic knowledge / Premise
+    Knowledge,
+    /// Logical operation or deduction step
+    Operation,
+    /// Requirement or Goal
+    Requirement,
+    /// Conclusion
+    Conclusion,
+}
+
+/// Verification status of a discrete node.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+pub enum VerificationStatus {
+    /// Not yet verified by the symbolic engine
+    Pending,
+    /// Validated by deterministic logic (e.g., code executed successfully)
+    Valid,
+    /// Logically invalid (e.g., invalid deduction, math error)
+    Invalid,
+}
+
+/// A single step in the reasoning graph.
+/// In System 3 AI, natural language is compiled into these discrete blocks.
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct LogicNode {
+    pub id: String,
+    pub node_type: LogicNodeType,
+    /// Natural language representation of the step
+    pub proposition: String,
+    /// Formal translation for the symbolic engine (e.g., Python code, Lean4 statement)
+    pub formal_translation: Option<String>,
+    pub status: VerificationStatus,
+    /// IDs of nodes this node depends on
+    pub dependencies: Vec<String>,
+    /// Confidence or Reward given by the verification step (for explicit graph-based reward thinking)
+    pub reward: f32,
+}
+
+impl LogicNode {
+    pub fn new(id: String, node_type: LogicNodeType, proposition: String, formal_translation: Option<String>) -> Self {
+        Self {
+            id,
+            node_type,
+            proposition,
+            formal_translation,
+            status: VerificationStatus::Pending,
+            dependencies: Vec::new(),
+            reward: 0.0,
+        }
+    }
+
+    pub fn add_dependency(&mut self, dep_id: String) {
+        if !self.dependencies.contains(&dep_id) {
+            self.dependencies.push(dep_id);
+        }
+    }
+}
+
+/// The Reasoning Graph (DAG) that explicitly represents the logical path.
+#[derive(Debug, Clone, Default, Serialize, Deserialize)]
+pub struct ReasoningGraph {
+    pub nodes: HashMap<String, LogicNode>,
+}
+
+impl ReasoningGraph {
+    pub fn new() -> Self {
+        Self {
+            nodes: HashMap::new(),
+        }
+    }
+
+    pub fn add_node(&mut self, node: LogicNode) {
+        self.nodes.insert(node.id.clone(), node);
+    }
+
+    pub fn get_node(&self, id: &str) -> Option<&LogicNode> {
+        self.nodes.get(id)
+    }
+
+    pub fn get_node_mut(&mut self, id: &str) -> Option<&mut LogicNode> {
+        self.nodes.get_mut(id)
+    }
+
+    /// Checks if the graph is a valid DAG (no cycles)
+    pub fn is_acyclic(&self) -> bool {
+        let mut visited = HashSet::new();
+        let mut path = HashSet::new();
+
+        for node_id in self.nodes.keys() {
+            if self.detect_cycle(node_id, &mut visited, &mut path) {
+                return false; // Cycle detected
+            }
+        }
+        true
+    }
+
+    fn detect_cycle(&self, node_id: &str, visited: &mut HashSet<String>, path: &mut HashSet<String>) -> bool {
+        if path.contains(node_id) {
+            return true;
+        }
+        if visited.contains(node_id) {
+            return false;
+        }
+
+        visited.insert(node_id.to_string());
+        path.insert(node_id.to_string());
+
+        if let Some(node) = self.nodes.get(node_id) {
+            for dep in &node.dependencies {
+                if self.detect_cycle(dep, visited, path) {
+                    return true;
+                }
+            }
+        }
+
+        path.remove(node_id);
+        false
+    }
+
+    /// Determines if all nodes in the graph are marked as Valid.
+    pub fn is_logically_sound(&self) -> bool {
+        self.nodes.values().all(|n| n.status == VerificationStatus::Valid)
+    }
+}

crates/synapse-core/src/logic/system3/mod.rs

@@ -0,0 +1,7 @@
+pub mod engine;
+pub mod graph;
+pub mod parser;
+
+pub use engine::{NeuroSymbolicEngine, SymbolicVerifierPort, MockPythonVerifier};
+pub use graph::{LogicNode, LogicNodeType, ReasoningGraph, VerificationStatus};
+pub use parser::NeuroSymbolicParser;