本論文では、大量の潜在的前提を含む知識ベースを用いて、人間の証明から学習せずに自動定理証明を行う方法を示します。深層強化学習のシナリオにおいて、tf-idf（term frequency-inverse document frequency）に基づく検索によって選択された追加的前提を混ぜ込む探索メカニズムを提案します。これにより、新しい定理を証明するために関連する前提を探し出すための探索と学習が助けられます。我々の実験結果は、この探索メカニズムで訓練された定理証明器が、人間の証明のみで訓練された証明器よりも優れた性能を発揮することを示しています。また、模倣学習と強化学習の組み合わせで訓練された証明器に近い性能も達成しています。我々は複数の実験を行い、我々の探索アプローチが機能する基盤となる仮定の重要性を理解することで、設計選択肢を説明しています。