Apprentissage de la Raisonnement dans de Grandes Théories sans Imitation

Dans cet article, nous démontrons comment effectuer la démonstration automatique de théorèmes en présence d'une grande base de connaissances de prémisses potentielles, sans apprendre à partir de preuves humaines. Nous proposons un mécanisme d'exploration qui incorpore des prémisses supplémentaires sélectionnées par une recherche basée sur le tf-idf (term frequency-inverse document frequency). Ce mécanisme est intégré dans un scénario d'apprentissage par renforcement profond. Cela aide à explorer et à apprendre quelles prémisses sont pertinentes pour la démonstration d'un nouveau théorème. Nos expériences montrent que le démonstrateur de théorèmes formé avec ce mécanisme d'exploration surpasse les démonstrateurs formés uniquement sur des preuves humaines. Il approche les performances d'un démonstrateur formé par une combinaison d'apprentissage par imitation et apprentissage par renforcement. Nous menons plusieurs expériences pour comprendre l'importance des hypothèses sous-jacentes qui rendent notre approche d'exploration efficace, expliquant ainsi nos choix de conception.