生成证明的等式蕴涵级联：SAIR EQT2 阶段2求解器
A Certificate-Producing Cascade for Equational Implication: The SAIR EQT2 Stage 2 Solver
浏览论文内容
中文总结 AI 辅助
本文提出SAIR EQT2阶段2求解器，采用代价优先级联架构，可判定等式理论的蕴涵关系并生成Lean验证器可接受的证明，在公开测试集上表现良好。
中文摘要 AI 辅助
SAIR数学蒸馏挑战中的等式理论任务要求求解器判定一个 magma 恒等式是否蕴涵另一个，且无论判定结果如何，都需返回确定性Lean验证器可接受的证明。本文提出一个单文件求解器，采用代价优先级联架构：其假分支结合结构化代数族上的系数测试、有界有限模型搜索、显式中心广群见证及多个无限载体见证；其真分支是生成证明的有序单元超归结过程，采用Knuth-Bendix序、双向归约、索引、记忆化替换及任意时刻规模深化。搜索结果不进入可信基：成功推导以小型Lean项形式复现，反模型由竞赛验证器重新检查。该冻结求解器是189504字节的Python文件，SHA-256值为f2392533c9f4c03b……；在官方验证器修订版2848228的本地运行中，其对6个公开集共1889行均生成了可接受的证明，未调用任何语言模型。独立测量显示，其在800个已发布的阶段1评估分布问题上完全一致，在无令牌的规范马拉松清单中获得100行接受结果，在托管 playground 中获得200行接受结果。这些是回归和 playground 测量，非排行榜结果，也非关于隐藏集的证据。所有定量声明均绑定到不可变结果账本，本文不提出完整性或比较优势声明。
英文摘要
The SAIR Mathematics Distillation Challenge on Equational Theories asks a solver to classify whether one magma identity implies another and, for either verdict, to return a certificate accepted by a deterministic Lean judge. We present a single-file solver organized as a cheapest-first cascade. Its false branch combines coefficient tests over structured algebra families, bounded finite-model search, an explicit central-groupoid witness, and several infinite-carrier witnesses. Its true branch is a proof-producing ordered unit superposition procedure with Knuth-Bendix ordering, bidirectional demodulation, indexing, memoised substitution, and anytime size deepening. Search results remain outside the trusted base: successful derivations are replayed as small Lean terms, and countermodels are rechecked by the competition judge. The frozen solver is a 189,504-byte Python file with SHA-256 f2392533c9f4c03b.... In local runs through official judge revision 2848228, it produced accepted certificates for all 1,889 rows of the six public sets with no language-model calls. Separate measurements recorded full agreement on the 800 published Stage 1 evaluation-distribution problems, 100 accepted rows in the canonical Marathon manifest without tokens, and 200 accepted rows in the hosted playground. These are regression and playground measurements, not a leaderboard result and not evidence about a hidden set. All quantitative claims are tied to immutable result ledgers; the paper makes no completeness or comparative-superiority claim.
发表机构
- ChronoAI Pte. Ltd.（ChronoAI私人有限公司）
- National University of Singapore（新加坡国立大学）
- Bytepro AI（Bytepro人工智能公司）
机构由 AI 辅助整理，请以论文原文为准。
