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

引用

@inproceedings{ huang2024mustard、 タイトル={{MUSTARD}: 定理と証明データの統一合成の習得}、 author={黄銀雅、林暁漢、劉正英、曹清興、新華建、王海明、李正国、宋林斉、梁暁丹}、 書籍タイトル={第12回学習表現に関する国際会議}、 年={2024}、 url={https://openreview.net/forum?id=8xliOUg9EW} }