Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learning

要約

AI ベースの数学的副操縦士 (主に大規模な言語モデル) の数学的能力をトレーニングおよび評価するために一般的に使用される一連のデータセットには、いくつかの欠点があります。
これらの制限には、数学的複雑さの限定された範囲が含まれており、通常は低学年レベルの数学、バイナリ評価プロトコル、その他の問題を超えないため、包括的な証明に基づく評価スイートが困難になります。
私たちはこれらの限界を体系的に調査し、大規模な言語モデルの機能を強化したり、AI ベースの数学アシスタント (副操縦士または「思考パートナー」) の今後の進歩には、数学的データセットの設計とその評価基準のパラダイムシフトが必要であると主張します。
数学的能力: 結果ベースのデータセット (定理記述から定理証明) から離れ、数学的研究実践の豊富な側面を LLM がトレーニングできるデータに変換する必要があります。
これらの例としては、証明発見プロセスの重要な部分である数学的ワークフロー (新しい数学を作成するときに頻繁に実行される、サブフィールドに依存する可能性のあるアトミックなタスクのシーケンス) があります。
さらに、私たちは数学的データセット開発者に対し、1949 年に G. P\’olya によって導入された「動機付けられた証明」の概念を考慮することを推奨します。この概念は、より優れた証明学習シグナルを提供するデータセットの青写真として機能し、前述の課題の一部を軽減します。
制限。
最後に、データセット用の数学データシートを導入し、一般的なデータセットに依存しないデータシートのバリアントを拡張します。数学データセット専用に設計されたアンケートを提供しており、データセット作成者がデータセットに含めることを推奨しています。
これにより、作成者はデータセットの潜在的な制限を認識できるようになり、同時に読者は数学的副操縦士のトレーニングと評価の観点からデータセットを評価しやすくなります。

要約(オリジナル)

The suite of datasets commonly used to train and evaluate the mathematical capabilities of AI-based mathematical copilots (primarily large language models) exhibit several shortcomings. These limitations include a restricted scope of mathematical complexity, typically not exceeding lower undergraduate-level mathematics, binary rating protocols and other issues, which makes comprehensive proof-based evaluation suites difficult. We systematically explore these limitations and contend that enhancing the capabilities of large language models, or any forthcoming advancements in AI-based mathematical assistants (copilots or ‘thought partners’), necessitates a paradigm shift in the design of mathematical datasets and the evaluation criteria of mathematical ability: It is necessary to move away from result-based datasets (theorem statement to theorem proof) and convert the rich facets of mathematical research practice to data LLMs can train on. Examples of these are mathematical workflows (sequences of atomic, potentially subfield-dependent tasks that are often performed when creating new mathematics), which are an important part of the proof-discovery process. Additionally, we advocate for mathematical dataset developers to consider the concept of ‘motivated proof’, introduced by G. P\’olya in 1949, which can serve as a blueprint for datasets that offer a better proof learning signal, alleviating some of the mentioned limitations. Lastly, we introduce math datasheets for datasets, extending the general, dataset-agnostic variants of datasheets: We provide a questionnaire designed specifically for math datasets that we urge dataset creators to include with their datasets. This will make creators aware of potential limitations of their datasets while at the same time making it easy for readers to assess it from the point of view of training and evaluating mathematical copilots.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google