Constructing a Neuro-Symbolic Mathematician from First Principles
Keqin Xie
TL;DR
Mathesis presents a neuro-symbolic framework that targets the core weakness of large language models in formal mathematics by integrating a differentiable Symbolic Reasoning Kernel with a Hypergraph Transformer Brain. Mathematical reasoning is represented as higher-order hypergraphs, and logical correctness is enforced through a global energy $E(\mathcal{G})$ composed of domain-specific engines (Matrix, Ideal, Geometric). The SRK provides dense gradient feedback, enabling energy-guided training and enabling structured search via MCTS and Evolutionary Proof Search with semantic unification. Early results on synthetic data and the miniF2F subset suggest faster discovery of valid derivations compared to sparse-reward baselines, with a modular design ready for scaling to real analysis, topology, and beyond. This approach advances robust, differentiable reasoning for formal mathematics and opens avenues for automated conjecture generation and cross-domain verified synthesis.
Abstract
Large Language Models (LLMs) exhibit persistent logical failures in complex reasoning due to the lack of an internal axiomatic framework. We propose Mathesis, a neuro-symbolic architecture that encodes mathematical states as higher-order hypergraphs and uses a Symbolic Reasoning Kernel (SRK)--a differentiable logic engine that maps constraints to a continuous energy landscape. By defining a global energy function E(G), where zero energy implies logical consistency, the SRK yields gradient-based signals to train a Hypergraph Transformer Brain, turning proof search into energy minimization. Multi-step deduction is enabled via Monte Carlo Tree Search and Evolutionary Proof Search, guided by learned value functions and semantic unification.