Symbolic Computation for All the Fun
有趣的符号计算
https://arxiv.org/abs/2404.12048
摘要
受到最近1000万美元AIMO挑战的启发，本文针对寻找符合给定规范的所有函数的问题。这是一个在数学竞赛中非常流行的问题，它带来了许多挑战，主要是合成可能的解决方案并证明不存在其他解决方案。通常有无限多的解决方案，然后必须以符号形式捕捉解决方案集合。我们提出了一种解决这个问题的方法，并在出现在数学竞赛和奥林匹克中的一组问题上对其进行评估。
关键词 AIMO，合成，量词消除，SMT
1. 引言
AIMO挑战承诺向能够在国际数学奥林匹克竞赛（IMO）中赢得金牌的AI模型颁发1000万美元奖金。在本文中，我们强调符号计算工具可以为旨在应对这一挑战的系统提供重要帮助。我们针对数学竞赛中遇到的一个流行问题，即寻找符合某种规范的所有函数。这项一般任务看起来几乎不可能完成。事实上，获得单一函数已经很困难，通常通过合成方法实现，如SyGuS[1]，或者通过特定逻辑片段的特定程序，参见[2, 3, 4, 5, 6]。然而，竞赛中的问题被构建得具有“漂亮”的解决方案。作为一个激励性的例子，考虑一个要求我们找到所有满足以下恒等式的函数𝑓的问题。
2. 问题描述
作为我们问题的来源，我们使用了由Vít Musil [7] 编译的集合，包括来自多个来源的问题，包括国际竞赛以及来自布拉格数学研讨会的一些（较简单）问题。我们将这些问题转录为SMT2格式，其中每个原始问题被分为3种类型的查询。
- 规范的可满足性，即是否存在解决方案（问题查找）；对于上述例子：
• 规范的不可满足性以及所有提议解决方案的否定（问题证明）；对于上述例子：
• 检查每个提议的解决方案确实是规范的解决方案（问题检查），即提议的解决方案与规范的否定的不可满足性；
对于上述例子：
这样，我们要求SMT求解器解决特定步骤，尽管这些步骤不一定涵盖函数方程的完整解决方案。我们没有提供有效解决方案可以包含的内容的正式描述（这可能是使用例如SyGuS [1]的进一步工作）。相反，我们使用我们自己的方法来找到特定形式的所有解决方案集合，该方法在第3节中描述。SMT2问题作为一个GitHub仓库提供，描述了87个问题。在某些情况下，如果存在多个不同的解决方案，检查查询会被分割成多个SMT2文件。我们注意到，在这项工作中，我们发现了在从源材料翻译到SMT时的几个错误。但同时，我们也发现了原始源材料中的一个问题。即问题C9（Cvičení 9）在原始[7]中是不可满足的，我们创建了两个版本的这个问题，作为两种不同的纠正方式（C9和C9a）。
2.1. 选定问题的解决方案
第3节描述了我们通过尝试证明它符合固定模板来解决问题的方法，特别是我们专注于可以表示为多项式的函数。在大多数情况下，这可能不是人类会解决它的方式。将这种联系起来是未来工作的主题。为了比较，我们在这里展示了三个示例问题及其原始（人类）解决方案：
• 问题U24，这是我们能够完全解决的最有趣的问题之一；
• 问题C12，我们无法解决它，但它不需要任何高级技术，所以解决它是可行的；
• 问题U2，它展示了一个需要归纳法来解决的问题，我们假设目前还无法解决。
3. 模板和量词消除
人们可以将这个问题视为在未解释函数理论中的量词消除，同时伴随着描述问题本身所需的理论——在我们的情况下，是实数或有理数的理论。由于这类问题的不可判定性，量词消除算法不能直接使用。一种可能的方法是合成一个符合规范的函数，然后加强规范，使得不再接受个别解决方案。然后，必须重复这个过程，希望解决方案是有限的，或者观察解决方案并将它们概括为更紧凑的描述。所有这些步骤都极其复杂。
相反，我们提出了一种尝试固定模板然后执行量词消除的方法：模板和量词消除，它包括以下子任务。
1. 确定解决方案的模板，例如 \( f(x) \equiv ax + b \)。
2. 证明所有解决方案必须符合这个模板（模板验证）。
3. 对函数的输入变量执行量词消除。
请注意，在实数的情况下，除了任务2之外，所有任务都是可计算的。本节的其余部分详细阐述了各个步骤。
3.1.1. 使用Waldmeister
除了假设的单元等式，Waldmeister还期望有一个单元等式作为要证明的目标。目标根据我们正在针对的模板而变化，并对应于SMT求解器的问题的第二变体。在每种情况下，我们固定了一个类型为 \(R\) 的常数 \(d\)（在假设中未提及）。对于每个模板，目标单元等式如下：
3.2. 量词消除
3.3. 后处理器以获得解决形式
3.3.1. 延迟验证
我们现在简要考虑上述方法的一个替代方案。当考虑一个模板时，我们不需要事先验证所有解决方案是否都在该模板类别中。相反，我们可以使用量词消除（QE）来为一个固定的模板找到一个解决方案类别，然后证明没有其他解决方案。这种方法的优势可以通过以下例子来说明。问题C1要求找出所有满足以下条件的函数f：
4. 实验
我们报告了第3节中介绍的模板和量词消除方法在第2节提出的基准测试上的结果。我们的方法的延迟扩展（第3.3.1节）留作未来的工作。模板验证（第3.1节）被证明是最困难的任务。表1a总结了模板验证的结果。所有这些我们都解决了量词消除任务。十三个实例被自动化方法完全解决。这十三个中，有两个可以追溯到竞赛事件。问题U24来自波罗的海之路竞赛——见第2节的“人类”解决方案。问题U71来自布拉格研讨会（PraSe-18-6-1）。在这两种情况下，唯一的解决方案是恒等于0的函数。
验证任务的结果通常导致可满足的问题，即如果存在一个解决方案在提议的模板之外（表1a中的×符号）。这些可满足的问题是非平凡的，因为它们涉及创建一个针对模板的反例。为此，我们还运行了cvc5的SyGuS方法（选项——sygus-inference）及其线性模型构建器[27]。
我们还报告了对手工编写解决方案正确性的验证，这包括两个组成部分：证明——显示所有可能的解决方案都被建议的解决方案覆盖；检查——检查所有建议的解决方案确实是问题解决方案（见第2节）。表1b总结了获得的结果。提供的手写解决方案中有六十五项成功通过了检查，即各个解决方案满足原始规范。手写的二十个解决方案被证明覆盖了所有个别解决方案。不出所料，证明任务比检查任务更难。我们注意到，对于U79的解决方案进行检查是微不足道的，因为没有个别解决方案。更详细的结果可以在作者的网页[28]上找到。
5. 结论和未来工作
本文加入了应对挑战的努力，目标是使计算机像国际数学奥林匹克竞赛（IMO）的金牌获得者一样强大。像AlphaGeometry [29]这样的努力表明，机器学习模型对这项任务是有用的，但同时，进一步的研究表明，它们从现有的符号方法中受益[30]。在这里，我们展示了符号方法确实已经在解决高度非平凡的任务方面非常强大，即找出满足特定规范的所有函数。
