MUSTARDSAUCE 数学定理問題データセット

香港城市大学、中山大学、ファーウェイのノアの方舟研究所などの研究者は、正確かつ人間的で高品質な大量の数的推論データを生成できる統合数理推論データ合成フレームワーク MUSTARD を提案しました。 -読みやすく、理解できる。このデータ セットは、研究用オープン ソース MUSTARDSAUCE データ セットです。各データには、自然言語による問題の説明と複数ステップの解決策、および二重形式言語 Lean 3 での問題の説明と複数ステップの解決策が含まれています。 MUSTARDSAUCEのデータには、数学の応用問題や定理証明問題が含まれており、小学校から高等教育までの難易度をカバーしています。質問の推論ステップの数は、質問の難易度に応じて増加します。最も難しい問題には、約 30 の解決ステップと約 20 のリーン 3 戦術が必要です。