GamePad: Среда обучения для автоматического доказательства теорем02.06.2018 07:00

Аннотация

В этой статье мы представляем систему под названием GamePad, которую можно использовать для исследования применения методов машинного обучения к доказательству теорем в интерактивном помощнике доказательств Coq. Интерактивные средства доказательства теорем, такие как Coq, позволяют пользователям пошагово строить проверяемые на машине доказательства. Таким образом, они предоставляют возможность исследовать автоматическое доказательство теорем под контролем человека. Мы используем GamePad для синтеза доказательств простой задачи алгебраического переписывания и обучения базовых моделей для формализации теоремы Фейта — Томпсона. Мы рассматриваем задачи оценки позиций (т. е. прогнозирования количества оставшихся шагов доказательства) и прогнозирования тактик (т. е. прогнозирования следующего шага доказательства), которые естественным образом возникают при доказательстве теорем на основе тактик.