要約
自動定理証明は、AIにおける重要なタスクの一つである。深層学習は定理証明器の訓練に有望な手法であるが、教師あり学習に利用可能な人間が書いた定理および証明のデータは限られている。この制約を克服するために、我々は、定理証明器の訓練を目的として、自動的に定理と証明を合成するニューラルジェネレータを学習する手法を提案する。実世界のタスクにおける実験により、本手法から生成された合成データが定理証明器の性能を向上させ、Metamathにおける自動定理証明の最先端技術を進展させることを示した。コードは https://github.com/princeton-vl/MetaGen で公開されている。