Exploiting Generative AI to Scale up Intelligent Tutoring Systems
Jakubův, Jana, Chvalovský, Karela, Goertzel, Zarathustraa, Kaliszyk, Cezaryb c, Olšák, Mirekd, Piotrowski, Bartosza, Schulz, Stephane, Martin Sudaa, Urban, Josefa
- aCzech Technical University in Prague, Czech Republic
- bUniversität Innsbruck, Austria
- cINDRC, Prague, Czech Republic
- dInstitut des Hautes Études Scientifiques, Paris, France
- eDHBW Stuttgart, Germany
Papers open inside SciRah from the original publisher or repository; SciRah never hosts them.
Abstract
As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60% of the Mizar theorems in the hammer setting. We also automatically prove 75% of the Mizar theorems when the automated provers are helped by using only the premises used in the human-written Mizar proofs. We describe the methods and large-scale experiments leading to these results. This includes in particular the E and Vampire provers, their ENIGMA and Deepire learning modifications, a number of learning-based premise selection methods, and the incremental loop that interleaves growing a corpus of millions of ATP proofs with training increasingly strong AI/TP systems on them. We also present a selection of Mizar problems that were proved automatically.