FIMO: A Challenge Formal Dataset for Automated Theorem Proving

要約

FIMO は、国際数学オリンピック (IMO) の最終候補問題から得られた正式な数学の問題ステートメントで構成される革新的なデータセットです。
FIMO は、IMO レベルでの高度な自動定理証明を容易にするように設計されており、現在はリーン形式言語に合わせて調整されています。
これは 149 の正式な問題ステートメントで構成され、非公式な問題の説明とそれに対応する LaTeX ベースの非公式な証明の両方が伴います。
GPT-4 を含む初期実験を通じて、我々の発見は現在の方法論の既存の限界を強調し、満足のいく IMO レベルの自動定理証明結果を達成するまでにはかなりの道のりが必要であることを示しています。

要約(オリジナル)

We present FIMO, an innovative dataset comprising formal mathematical problem statements sourced from the International Mathematical Olympiad (IMO) Shortlisted Problems. Designed to facilitate advanced automated theorem proving at the IMO level, FIMO is currently tailored for the Lean formal language. It comprises 149 formal problem statements, accompanied by both informal problem descriptions and their corresponding LaTeX-based informal proofs. Through initial experiments involving GPT-4, our findings underscore the existing limitations in current methodologies, indicating a substantial journey ahead before achieving satisfactory IMO-level automated theorem proving outcomes.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google