GamePad: как учат нейросети доказывать теоремы в Coq

Формальное доказательство теоремы — это не эссе, а последовательность строгих шагов, каждый из которых проверяет машина. В интерактивных пруверах вроде Coq человек вводит команды-тактики, а система следит, чтобы ни один переход не был мошенничеством. GamePad — это программная среда, которая открывает внутренности Coq наружу и превращает процесс доказательства в задачу для машинного обучения: по текущему состоянию доказательства предсказать следующий шаг. Работа была представлена группой из UC Berkeley (Daniel Huang и соавторы) и описана в статье GamePad: A Learning Environment for Theorem Proving.

Что вообще за задача

Coq — это интерактивный ассистент доказательств (proof assistant). Вы формулируете утверждение, а дальше двигаетесь к цели набором тактик: intro, apply, induction, rewrite и десятков других. После каждой тактики меняется состояние доказательства — набор ещё не доказанных подцелей и доступных гипотез. Доказательство завершено, когда подцелей не осталось.

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

Доказательство теоремы в этой постановке ближе не к сочинению текста, а к игре: есть состояние, есть набор ходов, есть выигрышная позиция — пустой список подцелей.

Как устроена среда

GamePad даёт программный интерфейс к Coq через Python: можно запускать доказательство, получать текущее состояние, применять тактики и откатываться назад. Это принципиально важно — без такой обвязки данные для обучения пришлось бы вытаскивать из логов вручную.

Авторы выделяют два уровня работы с состоянием:

• Термы доказательства — само выражение, которое строит Coq и которое затем проверяет ядро системы. Это дерево, а не строка, и модель работает именно со структурой.
• Состояние тактик — то, что видит человек: список подцелей и гипотез на каждом шаге. Именно по нему удобно предсказывать следующий ход.

Основным полигоном стал большой формализованный проект — доказательство теоремы Фейта — Томпсона¹ из теории групп, потому что это редкий пример по-настоящему объёмного корпуса реальных доказательств, а не учебных примеров.

Две задачи для модели

В работе рассматриваются две прогностические задачи, на которых можно честно измерять пользу представления:

1. Предсказание позиции. Насколько близко доказательство к завершению — своего рода оценочная функция, аналог value-функции в играх.
2. Предсказание тактики. Какую тактику применить в текущем состоянии — аналог policy, стратегии выбора хода.

Чтобы модель понимала структуру термов, авторы используют подход, при котором представление выражения собирается снизу вверх по дереву — от листьев к корню. Такое кодирование дерева даёт модели доступ к синтаксической структуре, а не к плоской строке символов.

Почему это сложнее, чем шахматы

Сравнение с играми напрашивается, но у доказательства теорем есть особенности, которые ломают привычные рецепты обучения с подкреплением.

Из-за разреженной награды и дорогого моделирования подходы вроде самоигры работают заметно хуже, чем в закрытых играх с чёткими правилами. Поэтому в этой области так ценятся именно готовые корпуса человеческих доказательств: они дают сигнал там, где чистое обучение с подкреплением буксует.

Что показали эксперименты

Главный результат — не готовый автопрувер, который сам доказывает произвольные теоремы, а демонстрация того, что структурное представление доказательства помогает. Модели, учитывающие древовидную структуру термов, предсказывали позицию и следующую тактику точнее простых базовых вариантов. То есть форма представления данных влияет на результат не меньше, чем архитектура модели.

Стоит трезво понимать границы: GamePad — это среда и постановка задачи, инструмент для исследований, а не продукт, который поставит доказательство теорем на поток. Конкретные метрики точности стоит смотреть в оригинальной статье, потому что они привязаны к конкретному корпусу и способу разбиения на обучение и тест.

Куда это встраивается

GamePad появился в череде проектов, соединяющих машинное обучение и формальные пруверы — Coq, Isabelle, Lean. Общая логика везде похожа:

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

Практический интерес здесь не абстрактный. Формальная верификация — это доказательство корректности критичного кода, протоколов и математических результатов. Чем дешевле становится строить такие доказательства, тем реалистичнее их применение за пределами академии: в компиляторах, криптографии, безопасности.

¹ Теорема Фейта — Томпсона — результат теории конечных групп: каждая конечная группа нечётного порядка разрешима. Её полная формализация в Coq — один из крупнейших проектов машинно проверенного доказательства, что и делает его удобным источником данных.