NeSy Progression #414

The problem

Currently, ECHIDNA operates as a Type 2 (Symbolic[Neuro]) architecture with a hard computational boundary between the Julia ML tactic suggester and the Tier-1 formal verification engines (Z3, Lean, CVC5). Because the neural layer operates as a discrete heuristic subroutine, it cannot learn dynamically from structural proof failures in real-time. Furthermore, the ML layer is ignorant of strict logical invariants at the generation stage, leading to hallucinated or invalid tactic suggestions that waste expensive prover cycles in the Rust backend. ECHIDNA is unable to natively perform mathematically guaranteed fuzzy deductive reasoning, creating a throughput and scalability bottleneck by forcing complete reliance on traditional external solvers.

Proposed change

We propose a phased architectural evolution up the Kautz taxonomy to systematically dissolve the boundary between the machine learning and formal verification layers:

Milestone 1: Bidirectional Feedback Loops (Type 3: Neuro; Symbolic)
Modify src/rust/dispatch.rs and the Julia GNN integration to support real-time feedback. The Rust orchestrator must feed structured logical counter-examples back to the neural network during an active proof search, allowing the ML layer to adapt dynamically without requiring an offline batch retraining session.

Milestone 2: Logic-Compiled Neural Weights (Type 4: Neuro: Symbolic → Neuro)
Embed the structural logic constraints (currently housed in axiom_tracker.rs and the Idris2 ABI) directly into the Julia neural network's architecture and loss function. This ensures the ML model is mathematically constrained from generating invalid starting states or suggesting dangerous axioms.

Milestone 3: Tensor-Grounded Logic Integration (Type 5: Neuro_Symbolic)
Implement a Logic Tensor Network (LTN) framework to replace the discrete hand-off mechanism. Formal concepts (tactics, theorems, states) will be mapped into continuous neural embeddings, allowing logical operations (AND, OR, IMPLIES) to be computed natively as tensor operations.

Milestone 4: Unified Cognitive Manifold (Type 6: Neuro[Symbolic])
Shift primary deductive workloads fully into the inherently verified neural architecture. The legacy Rust dispatcher and external Tier-1 backends will be retained strictly as fallback validation mechanisms, achieving native mathematical reasoning within the neural manifold.

Alternatives considered

Doing nothing (Maintaining Type 2): This is insufficient because the neural layer will remain structurally blind to logical constraints, creating an artificial ceiling on proof success rates and wasting substantial compute on evaluating hallucinated tactics.

Horizontal Scaling of Tier-1 Provers: Adding more external formal provers (e.g., expanding Wave-2/Wave-3 integrations) merely parallelizes the bottleneck without improving the ML layer's actual deductive intelligence or reducing the network overhead of cross-prover arbitration.

Offline Batch Retraining Only: Relying on scheduled offline retraining on VeriSimDB logs is insufficient because the system cannot dynamically adapt to novel mathematical domains encountered during an active, live proof session.

Scope

Repo-local — affects only this project