OEIS序列基准

OEIS序列基准是由捷克技术大学的研究团队创建的一个大型数据集，包含29687个问题，这些问题是从OEIS中自动提取的。每个问题都涉及两个生成相同OEIS序列的不同程序的等价性。数据集涵盖了广泛的数学领域，旨在评估归纳定理证明器在这一领域的进展。该数据集的创建过程涉及使用程序合成算法自动生成问题，并通过严格的验证确保问题的有效性。该数据集主要应用于数学定理自动证明领域，旨在帮助开发者和研究者提升归纳定理证明器的性能。

The OEIS Sequence Benchmark is a large-scale dataset created by a research team from the Czech Technical University, containing 29,687 problems automatically extracted from the On-Line Encyclopedia of Integer Sequences (OEIS). Each problem focuses on the equivalence of two distinct programs that generate the same OEIS sequence. Covering a broad range of mathematical domains, this dataset is designed to evaluate the progress of inductive theorem provers in this field. The creation of this dataset involved automatically generating problems via program synthesis algorithms and ensuring their validity through rigorous verification. Primarily applied in the field of automated mathematical theorem proving, this dataset aims to assist developers and researchers in improving the performance of inductive theorem provers.

原始信息汇总

数据集概述

该数据集包含与论文“Learning Program Synthesis for Integer Sequences from Scratch”相关的软件QSynt。数据集提供了在全规模自学习运行期间找到的解决方案，这些解决方案存储在文件results/solutions中。

安装指南

依赖安装

• 适用于Ubuntu操作系统。

• 需要安装的依赖包括：MKL、polyml、HOL、OpenBLAS。

• 安装命令： bash sudo apt install -y libgmp-dev rlwrap intel-mkl sh install_dep.sh

• 提示：安装intel-mkl需要2GB空间，但如果仅运行检查器则非必需。

oeis-synthesis安装

• 安装步骤： bash cd src sh install.sh

• 更新仓库后需重新运行sh install.sh。

使用指南

运行oeis-synthesis

• 进入src目录并运行： bash sh rl.sh expname

• 修改训练选项：编辑config文件并重新运行sh install.sh。

• 实验名称expname可自定义。

• 可随时通过ctrl+c中断训练，并从上次生成重新启动。

• 训练过程中找到的程序数量总结在src/exp/expname/log中。

• 生成的程序可在src/exp/expname/search/gen/full_prog目录中查看。

自定义序列搜索

• 在文件src/data/oeis末尾添加自定义序列，格式为A-number后跟逗号分隔的整数序列。

外部工具生成程序的检查

• 在src目录中创建exp和exp/expname目录。

• 在exp/expname中添加solold和cand文件。

• 运行检查命令： bash sh check.sh expname

• 修改检查选项：编辑config文件。

外部自学习过程的引导

• 从文件sol0和sol0gpt开始自学习过程。
• 下载文件： bash wget http://grid01.ciirc.cvut.cz/~thibault/oeis-gpt/sol0 wget http://grid01.ciirc.cvut.cz/~thibault/oeis-gpt/sol0gpt

已知问题

• 安装MKL的解决方案：参见https://github.com/eddelbuettel/mkl4deb。
• 编译FFI时的问题：在oeis-synthesis目录中安装openlibm。

搜集汇总

数据集介绍

构建方式

该数据集的构建方式是通过将在线整数序列百科全书（OEIS）中的29687个问题转化为SMT-LIB格式的问题。这些问题的来源是自动生成的，通过一个学习引导的合成系统，该系统使用具有循环运算符的语言。这些运算符实现了递归，因此许多证明都需要自然数的归纳。数据集中的问题难度不一，涵盖了广泛的数学领域。这种构建方式使得数据集成为衡量归纳定理证明器在该领域进步的有效工具。

使用方法

该数据集的使用方法是将SMT-LIB格式的问题输入到归纳定理证明器中进行求解。数据集中的问题已经被转化为SMT-LIB格式，因此可以直接使用现有的SMT求解器进行求解。此外，数据集还包含了问题的初始域和函数定义，这使得证明器可以更有效地进行证明。数据集还包含了未经验证的问题列表，供进一步分析使用。

背景与挑战

背景概述

OEIS序列基准数据集是数学领域的一项重要成果，旨在为归纳定理证明器提供一个全面的测试平台。该数据集包含29,687个问题，这些问题均来自在线整数序列百科全书（OEIS）。每个问题都表达了两段语法不同的程序生成相同OEIS序列的等价性。这些问题由一个学习引导的合成系统自动生成，该系统使用具有循环运算符的语言。这些问题涵盖了广泛的数学领域，具有不同的难度，为归纳定理证明器在该领域的进步提供了一个有效的评估标准。

当前挑战

OEIS序列基准数据集的挑战主要在于其复杂性。这些问题需要归纳推理，许多证明需要自然数上的归纳。此外，数据集构建过程中也面临挑战，例如，如何确保生成的程序覆盖OEIS序列的所有项，以及如何处理长运行程序或快速增长的程序中的等式。这些问题对当前最佳的归纳定理证明器来说仍然很难，但对于大学学生来说却相对容易。因此，该数据集对开发者来说是一个很好的挑战，可以帮助他们缩小这一差距。

常用场景

经典使用场景

OEIS序列基准数据集主要用于评估归纳定理证明器的性能和进展。该数据集包含了由学习引导的合成系统生成的29,687个问题，每个问题都表达了两个在语法上不同的程序生成相同OEIS序列的等价性。这些问题覆盖了从简单到复杂的各种数学领域，为归纳定理证明器提供了一个有效的测试平台。

解决学术问题

该数据集解决了归纳定理证明器在处理数学公式证明方面的挑战。它提供了一个基于数学理论的基准，有助于评估和改进归纳定理证明器在处理递归和归纳证明方面的能力。此外，该数据集还帮助研究者探索了各种技术，如项合成、rippling和基于模板的假设，以提高归纳定理证明器的效率。

实际应用

该数据集在实际应用中，可以用于教育和研究目的，帮助数学家和计算机科学家更好地理解和改进归纳定理证明器的性能。此外，该数据集还可以用于开发新的算法和技术，以解决更复杂的数学问题，并推动数学和计算机科学领域的发展。

数据集最近研究

最新研究方向

本数据集为归纳定理证明器提供了一个基于数学理论的自然基准，包含从在线整数序列百科全书（OEIS）中派生的29687个问题。这些问题涉及数学领域中不同难度的各种问题，旨在测试归纳定理证明器在证明数学公式方面的进展。该数据集的问题是通过程序合成算法自动生成的，它们表达两个语法不同的程序生成相同的OEIS序列的等价性。由于许多问题需要自然数上的归纳，这为归纳定理证明器提供了挑战。本数据集已翻译成SMT-LIB格式，并提供了评估基线，为未来的比较和研究提供了基础。

相关研究论文

• A Mathematical Benchmark for Inductive Theorem Provers

  捷克技术大学 · 2023年