Гenerative language modeling for automated theorem proving07.09.2020 07:00

Аннотация

Мы исследуем применение языковых моделей на основе трансформеров для автоматического доказательства теорем. Данное исследование мотивировано предположением, что главный недостаток автоматических средств доказательства теорем по сравнению с человеком — генерация оригинальных математических терминов — может быть преодолен с помощью генерации на основе языковых моделей. Мы представляем GPT‑f, автоматический модуль доказательства и ассистент доказательств для языка формализации Metamath, а также анализируем его производительность. GPT‑f нашла новые короткие доказательства, которые были приняты в основную библиотеку Metamath. Насколько нам известно, это первый случай, когда система на базе глубокого обучения внесла свой вклад в виде доказательств, принятых сообществом специалистов по формальной математике.