技术摘要：通过组合数学中的机器发现绘制未charted 对称性

问题表述

本文探讨了一类特定的数学发现问题，将其表述为函数发现：给定两个集合 $X$ 和 $Y$，寻找一个函数 $f: X \to Y$，该函数在满足严格、精确的约束条件的同时，具备简洁的符号描述。作者将此设定形式化为严格比例下的简单学习（SLURP）。

在 SLURP 中，定义域 $X$ 被划分为“包”（bags）$B_i$，每个包关联着值域 $Y$ 上的一个目标分布 $D_i$。目标是发现一个函数 $f$，使得：

1. 严格比例约束：$f$ 在每个包 $B_i$ 上的输出必须精确匹配目标分布 $D_i$。近似满足是不够的；任何偏差都意味着问题未解决。
2. 简洁性要求：该函数必须以简洁的符号描述（封闭公式或算法）形式提供，且可在合理的时间界限内（例如多项式时间）进行评估。这一要求至关重要，旨在确保解决方案揭示数学结构，而非仅仅是任意、琐碎的数值赋值。

作者将此框架应用于代数组合学，具体研究 $q,t$-Narayana 多项式 $N_{n,k}(q,t)$。核心挑战在于寻找组合对象（非交叉划分）上的一对简单统计量（函数），使其共同生成这些多项式，并构建显式双射以证明其对称性 $N_{n,k}(q,t) = N_{n,k}(t,q)$。

方法论

本文引入了两种不同的机器学习方法来求解 SLURP 实例：

1. MapSeek-Functional（自训练方法）

该方法使用神经网络（具体为 Transformer 编码器）对目标函数进行建模，并在以下两个步骤之间交替进行：

• 约束投影：给定当前模型 $f_\theta$，算法寻找满足严格比例约束的最接近函数 $\hat{f}$。这涉及求解一个优化问题，以最小化 $f_\theta$ 与满足约束的函数之间的距离。
• 监督更新：投影后的函数 $\hat{f}$ 生成伪标签，用于通过监督训练（SGD）更新 $f_\theta$。
• 验证：执行严格的停止准则：仅当模型在验证集上完美满足约束时，运行才算成功。验证集的大小作为一个超参数，用于过滤掉复杂或不可解释的解决方案。
• 蒸馏：收敛后，将神经网络的行为手动或自动蒸馏为符号公式。

2. MapSeek-Symbolic（搜索方法）

该方法直接在定义的形式语言 $\mathcal{L}$ 中搜索符号公式。

• 搜索空间：公式由原始符号字母表（变量、算术运算符、逻辑运算符）构建。
• 优化：搜索采用基于生成式 Transformer 解码器的深度交叉熵方法（CEM）。它迭代地采样一组公式，评估其“距离”（约束违反程度），并选择一个精英子集来重新训练生成模型。
• 距离度量：距离函数 $\delta$ 衡量候选公式的输出分布与目标分布之间的 $L_1$ 差异。作者发现，将问题视为分类任务（使用平凡度量）比回归方法（使用排序后的 $L_1$ 距离）更有效。
• 稳定性：作者指出，公式表示法中显式的结构分隔符（空格和括号）对于训练稳定性至关重要，可防止模型生成语法有效但语义冗余的表达式。

主要贡献与结果

1. SLURP 框架与基准测试

作者形式化了 SLURP 框架，并发布了skip-pairing 基准测试。该基准测试的任务是发现非交叉划分上的统计量，使其与已知的"skip"统计量配对，以解释 $q,t$-Narayana 多项式。数据集包含基于非单元素块中最大元素的细化约束。

2. 新统计量的发现

将两种方法应用于 $k=3$ 的情况（具有 $n-2$ 个块的划分），作者发现了几种新的、可解释的统计量：

• Mag（幅度）：通过带有暖启动约束的 MapSeek-Functional 发现。它与 skip 统计量配对。
• Leap：通过带有同质性约束的 MapSeek-Functional 发现。它与 skip 统计量配对。
• Skew：通过 MapSeek-Symbolic 发现。它与 skip 统计量配对。
• Mingarc（最小间隙弧）：人类定义的翻转"skew"统计量的扩展，源自机器学习发现。

3. 解决组合学中的开放问题

最重要的数学成果是解决了 $k=3$ 情况下的开放问题 4.1：

• 对称性的组合证明：作者构建了一个显式的交换双射，将划分 $\pi$ 映射到 $\psi(\pi)$，使得统计量对 $(\text{skip}, \text{leap})$ 发生交换：$(\text{skip}(\psi(\pi)), \text{leap}(\psi(\pi))) = (\text{leap}(\pi), \text{skip}(\pi))$。
• 这提供了通过显式双射证明对称性 $N_{n,3}(q,t) = N_{n,3}(t,q)$ 的首个组合证明，该问题被广泛认为极其困难。
• 新解释：这项工作首次提供了 $N_{n,k}(q,t)$ 在所有 $k$ 值下的组合解释，基于非交叉划分（具体通过 $(\text{skip}, \text{mingarc})$ 配对）。

4. 形式化验证

为确保可复现性和严谨性，作者在 Lean 4 中形式化了所有数学发现，包括新统计量、双射和对称性证明。他们利用 Aristotle 系统辅助自动形式化和证明搜索，从而实现了对核心结果的完全机器检查验证。

意义与主张

本文声称是首个利用机器学习提出先前未知的组合统计量的研究，这些统计量随后被用于构建交换双射，从而解决了 $q,t$-组合学中的一个开放问题。

• 方法论意义：作者将 SLURP 定位为一种“证明驱动的发现框架”。与寻求近似泛化的标准机器学习不同，SLURP 要求在有限数据上精确满足约束，其最终目标是寻找简单的符号描述，这些描述可被数学证明在无限域上成立。
• 科学影响：这项工作表明，现代机器学习可以在可验证的数学发现中做出有意义的贡献，特别是在严格分布约束下寻找简单函数方面。
• 局限性与未来工作：作者谦逊地指出，虽然 $k=3$ 的情况产生了封闭形式解，但 $k=4$ 的实验目前显示出失效模式（例如，MapSeek-Functional 收敛到难以解释的解决方案，MapSeek-Symbolic 未能达到零距离）。他们承认，理解解空间的探索以及量化“简洁性”仍然是开放的方法论挑战。

本文总结认为，这些工具在专家数学家手中，能够利用人类直觉扩展数学发现的边界，特别是在构建显式双射是主要瓶颈的领域。