Moxia用符号计算+规则路由实现数学推理自解释,答案可信可验证。
Moxia: A Trust-First Neuro-Symbolic Execution Architecture for Self-Explaining Mathematical Reasoning

- 语言模型仅做文本规范化,后续由符号系统严格推导答案
- 在MATH测试中准确率达90.2%,且无错误自信回答
- 每步推导自动生成解释,支持导入Lean 4形式化验证
我们提出Moxia(前称AXIOM),一种以信任为核心的神经符号架构,用于自然语言输入的自解释数学推理。其语言模型仅作为规范器:将非正式问题文本重写为窄范式,交由确定性计算机代数系统(CAS)流水线推导并验证答案,或作为首类输出放弃。路由遵循问题形状正则、模式特定提示与闭式CAS处理函数的一一对应,共部署4,783条路径,其中71%无需调用语言模型即可作答,且从未出现正确答案丢失(LOST_CORRECT)情况,作为发布门槛。由于答案是推导而非生成,解释亦随之生成:每个处理函数输出计算步骤轨迹,由覆盖全部4,785个任务文件的层转化为自然语言,确保每段叙述均对应实际执行步骤。推导结果还可导出至Lean 4:479个任务文件(10%)生成定理,445个被Lean内核与Mathlib接受,构成真实运行输出,非仅机器检查。我们报告两个独立数值,从不合并。在设计对抗的7类别MATH测试集上,Moxia准确率达90.2%(4,510/5,000),仅1次自信错误(99.98%信任度于可解析样本)。在未设计对抗的持有数据集MATH-500上,准确率89.2%(446/500),零自信错误。1.0个百分点差距即核心发现:若仅记忆问题形态的注册表将在新数据上崩溃,而此系统不会。纯规则路径在包含20,000记录的lm-eval算术基准上达100%准确率,每条耗时1毫秒。我们强调的并非准确率数字,而是正向动态:每次记录的放弃都可能是下一周期的正确解,因新任务组合不引发注册表退化。
原文摘要 · Abstract (English)
We present Moxia (formerly AXIOM), a trust-first neuro-symbolic architecture for self-explaining mathematical reasoning over natural-language input. Its language model is strictly a canonicalizer: it rewrites informal problem text into a narrow schema consumed by a deterministic Computer-Algebra-System (CAS) pipeline, which derives and verifies the answer or abstains as a first-class output. Routing follows a 1:1:1 alignment of problem-shape regex, schema-specific prompt, and closed-form CAS handler, with 4,783 routes shipped, 71% of which answer without invoking the language model, and zero LOST_CORRECT regressions as a standing release gate. Because the answer is derived rather than generated, so is its explanation: every handler emits a step trace of the computation it performed, rendered as prose by a layer covering all 4,785 task files that cannot narrate a step the handler did not take. Derivations export to Lean 4 as well: 479 task files (10%) emit a theorem from the problem's declared data, 445 accepted by the Lean kernel with Mathlib; that gate covers a fixture corpus, so live output is generated, not machine-checked. We report two numbers and never fuse them. On the full 7-category MATH test split, designed against, Moxia answers 90.2% (4,510/5,000) with one confident-wrong answer (99.98% trust on parseable). On held-out MATH-500, never designed against, it answers 89.2% (446/500) with zero confident-wrong answers. The 1.0 pp gap is the substantive result: a registry that had merely memorized problem shapes would collapse on held-out data, and this one does not. The rule-only path answers the 20,000-record lm-eval arithmetic benchmark at 100%, 1 ms per record. What we emphasize is not an accuracy figure but the forward dynamic: every logged abstain is a candidate correct after one ship cycle, since new tasks compose without regressing the registry.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。