HOList: 高次定理証明の機械学習環境

私たちは高階論理のための環境、ベンチマーク、および深層学習駆動型の自動定理証明システムを提示します。高階対話型定理証明システムは、任意の数学理論の形式化を可能にし、これにより深層学習にとって興味深いオープンエンドの課題を提供します。私たちはHOL Light定理証明システムに基づいたオープンソースフレームワークを提供しており、これが強化学習環境として利用可能です。HOL Lightには、微積分とケプラー予想の形式証明に関する基本的な数学定理が広範囲にわたって含まれています。これから導き出される自動推論のための挑戦的なベンチマークも提供しています。また、このベンチマークにおいて初期段階で優れた結果を示した深層強化学習駆動型の自動定理証明システムであるDeepHOLについても紹介します。（注：「Kepler conjecture」は「ケプラー予想」と翻訳しました。「DeepHOL」は固有名詞としてそのまま使用しています。）