OEIS序列基准|数学定理自动证明数据集|程序等价性验证数据集

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

原始信息汇总

数据集概述

该数据集包含与论文“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。