要約
トランスフォーマー型言語モデルを自動定理証明への応用について検討する。本研究の動機は、自動定理証明システムと人間との間にある主要な差異——すなわち、独創的な数学的用語の生成能力の欠如——が、言語モデルによる生成によって克服可能である可能性にある。本研究では、メタマス（Metamath）形式化言語を対象とする自動証明システムおよび証明補助ツール「GPT-f」を提案し、その性能を分析する。GPT-fは、メタマス公式ライブラリに採択された新たな短い証明を発見した。これは、深層学習に基づくシステムが形式数学コミュニティによって採用された証明を初めて提供したと認識される、現時点において初めての事例である。