Использование генеративного искусственного интеллекта для масштабирования интеллектуальных обучающих систем

В качестве подарка Mizar к его 50-летнему юбилею мы разрабатываем систему искусственного интеллекта и автоматического доказательства теорем (AI/TP), которая автоматически доказывает около 60% теорем Mizar в режиме hammer. Кроме того, нам удаётся автоматически доказать 75% теорем Mizar, если автоматическим доказчикам помогают, используя только посылки, задействованные в написанных человеком доказательствах Mizar. Мы описываем методы и крупномасштабные эксперименты, приведшие к этим результатам. В частности, они включают доказчики E и Vampire, их модификации с обучением ENIGMA и Deepire, ряд методов выбора посылок на основе обучения, а также итеративный цикл, в котором расширение корпуса, содержащего миллионы доказательств ATP, чередуется с обучением на нём всё более мощных систем AI/TP. Мы также представляем подборку задач Mizar, доказанных автоматически.