DeepTheorem は、自然言語に基づく非公式な定理証明を通じて大規模言語モデル (LLM) の数学的推論機能を強化することを目的とした数学的推論データセットです。

このデータセットには、複数の数学分野を網羅する121,000件のIMOレベルの非公式定理と証明が含まれています。それぞれの定理と証明のペアには、以下のように厳密に注釈が付けられています。

• o3-mini 証明: o3-mini モデルによって生成または検証された証明は、数学的な正確性を保証します。
• 真理値: o3-mini 証明から抽出された定理の真理値。定理が真か偽かを示します。
• 難易度: さまざまな LLM 能力に合わせて複雑さによって分類されます。
• カテゴリー: 代数学、幾何学、数論などを扱います。
• 変形: 元の定理と同じまたは反対の真理値を持つ定理の正または負の変形。