FIMO：一个用于自动定理证明的形式化竞赛数据集
人工智能
2023-12-06 v2
摘要
我们提出 FIMO，一个由国际数学奥林匹克(IMO)短名单问题中的形式化数学问题陈述组成的创新数据集。FIMO 旨在促进 IMO 级别的先进自动定理证明，目前专为 Lean 形式化语言定制。它包含 149 个形式化问题陈述，并附有非形式化问题描述及其对应的基于 LaTeX 的非形式化证明。通过涉及 GPT-4 的初步实验，我们的发现凸显了当前方法的局限，表明在取得令人满意的 IMO 级别自动定理证明成果之前仍有漫长路程。
引用
@article{arxiv.2309.04295,
title = {FIMO: A Challenge Formal Dataset for Automated Theorem Proving},
author = {Chengwu Liu and Jianhao Shen and Huajian Xin and Zhengying Liu and Ye Yuan and Haiming Wang and Wei Ju and Chuanyang Zheng and Yichun Yin and Lin Li and Ming Zhang and Qun Liu},
journal= {arXiv preprint arXiv:2309.04295},
year = {2023}
}
备注
Added a hyperlink to the dataset made accessible on GitHub