VERITAS: новый метод формального доказательства теорем достиг 40.6% на miniF2F
Исследователи представили VERITAS — фреймворк для формального доказательства теорем, который эффективно использует сигналы от верификатора. В отличие от стандартных подходов, сводящих эти сигналы к бинарному ответу «успех/неудача», VERITAS анализирует синтаксические ошибки, несоответствия типов и частичный прогресс в доказательстве.
Метод основан на двухфазном протоколе. Первая фаза — выборка Best-of-N, где генерируется несколько вариантов доказательства. Вторая фаза использует критик-управляемый поиск по дереву Монте-Карло (MCTS), который обрабатывает неудачи первой фазы как явные отрицательные примеры. Это позволяет направлять дальнейший поиск.
На бенчмарке miniF2F, включающем задачи олимпиадной математики, VERITAS достиг точности 40.6%. Для сравнения: независимо запущенный Best-of-5 показал 36.9%, а метод Portfolio — 26.2%. Важно, что VERITAS сохраняет все теоремы, решённые на первой фазе, поэтому прирост на второй фазе однозначно связан с обратной связью от верификатора.
В рамках работы создан новый бенчмарк VERITAS-CombiBench, содержащий 55 теорем из комбинаторики. На нём VERITAS набрал 7.3%, тогда как Best-of-5 — 1.8%, а Portfolio — 3.6%. Авторы отмечают, что неориентированная выборка хуже справляется с задачами, в которых правильные имена лемм нужно итеративно восстанавливать по сигналам верификатора.
Артефакты проекта доступны на GitHub. VERITAS демонстрирует, что учёт всей информации от верификатора существенно повышает эффективность автоматического доказательства теорем на основе больших языковых моделей.
