Apprendre à prouver des théorèmes en apprenant à générer des théorèmes

Nous considérons la tâche de démonstration automatique de théorèmes, une tâche clé en intelligence artificielle. L'apprentissage profond a montré un potentiel prometteur pour former des démonstrateurs de théorèmes, mais les théorèmes et preuves rédigés par des humains disponibles pour l'apprentissage supervisé restent limités. Pour pallier cette limitation, nous proposons d'apprendre un générateur neuronal capable de synthétiser automatiquement des théorèmes et leurs preuves, dans le but de former un démonstrateur de théorèmes. Des expériences menées sur des tâches du monde réel démontrent que les données synthétiques produites par notre approche améliorent significativement le démonstrateur de théorèmes et avancent l'état de l'art de la démonstration automatique de théorèmes dans Metamath. Le code est disponible à l'adresse suivante : https://github.com/princeton-vl/MetaGen.