要約
大規模なコンピュータが理解可能な証明は、数百万の中間論理ステップから構成されています。これらのステップの大部分は、中間目標に対して手動で選択され、手動でガイダンスされたヒューリスティックによって生成されます。これまで、機械学習は一般的にこれらのステップのフィルタリングや生成には利用されていませんでした。本論文では、高階論理（Higher-Order Logic: HOL）証明に基づく新しいデータセットを紹介します。このデータセットは、BSDライセンスのもとで公開されています。また、このデータセット上で実行できるさまざまな機械学習タスクを提案し、その定理証明における重要性について議論します。さらに、これらのタスクに適した単純なベースラインの機械学習モデル（ロジスティック回帰、畳み込みニューラルネットワーク、および再帰ニューラルネットワークを含む）のベンチマークを行いました。私たちのベースラインモデルの結果は、機械学習をHOL定理証明に適用することの可能性を示しています。