GPT-f — это языковая модель, которую обучили генерировать доказательства теорем. В качестве архитектуры использовали transformer-модель GPT-3. GPT-f призван ассистировать математикам при доказательстве теорем. Модель работает для формального языка для доказательства теорем Metamath. По результатам экспериментов, GPT-f находила новые короткие доказательства, которые приняли в библиотеку Metamath. Это первый раз, когда модель глубокого обучения сгенерировала доказательства для теорем, которые были приняты сообществом математиков.
Зачем автоматизировать доказательство теорем
Автоматическое доказательство теорем является перспективным направлением исследований по следующим причинам:
- Доказательство теорем требует умение делать логический вывод и рассуждать;
- Быстрые поиск доказательства и проверка его на корректность;
- Автоматическая генерация данных для обучения моделей поиска доказательств
Подробнее про GPT для доказательства теорем
Исследователи использовали формальную среду Metamath для проверки доказательств. Основная библиотека Metamath содержит ~38 тысяч доказательств, основанных на системе аксиом Цермело — Френкеля. В качестве моделей использовали две предобученные GPT-3:
- На отфильтрованном CommonCrawl;
- На данных Github, arXiv и Math StackExchange
Дообучали модель на синтетических датасетах.
GPT-f является state-of-the-art подходом для среды Metamath. Лучшая из моделей сгенерировала 56.22% доказательств из тестового датасета. Предыдущая SOTA модель MetaGen-IL смогла доказать только 21.16% теорем.
