用符号逻辑与神经网络结合，让AI自动解数学题并自我修正错误。
Constructing a Neuro-Symbolic Mathematician from First Principles
- 把数学推理建模为超图，用能量函数衡量逻辑一致性。
- 通过梯度优化训练模型，使证明过程变成能量最小化问题。
- 适合研究逻辑推理、AI数学能力的学者与工程师。
大型语言模型在复杂推理中因缺乏内部公理体系而持续出现逻辑错误。我们提出Mathesis，一种神经符号架构：将数学状态编码为高阶超图，并使用可微分的符号推理核（SRK）将约束映射到连续能量景观。通过定义全局能量函数E(G)，零能量表示逻辑一致，SRK生成梯度信号以训练超图变换器大脑，将证明搜索转化为能量最小化。多步演绎通过蒙特卡洛树搜索和进化证明搜索实现，由学习到的价值函数与语义统一引导。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。