Формальный доказатель выбирает метод по применимости, а не по сходству

Формальный доказатель научили выбирать математический метод по тому, как именно он поможет решить текущую задачу, а не только по сходству формулировок. Работа команды из University of Illinois at Urbana-Champaign, Tsinghua University, Imperial College London и Google пока не рецензирована, а все числа в ней получили сами авторы: на задачах Putnam подходящий метод попадал в первую пятёрку в 95,0% случаев против 84,2% у сильнейшего варианта с повторным ранжированием. Для систем на Lean это повод вынести выбор стратегии в отдельный этап перед генерацией доказательства.

Каждый метод сначала объясняет, как применит себя

Обычный поиск находит теоремы, доказательства и методы, похожие на условие задачи. Но сходство не отвечает на практические вопросы: к какой части цели относится метод, какое преобразование он выполнит и какие предпосылки придётся доказать.

Предложенная самопрезентация (self-advertisement) меняет порядок выбора. Модель получает текущую цель и библиотеку методов, а затем одним пакетным вызовом составляет отдельное предложение для каждого кандидата. В нём кандидат указывает цель, действие и необходимые условия.

После этого фильтр понижает методы с расплывчатым или неподтверждённым предложением. В примере из работы AM-GM выглядит тематически подходящим, но требует неотрицательности величин, которой нет в условии. Поэтому система поднимает выше Cauchy–Schwarz, для которого может назвать обоснованный следующий шаг.

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

Контракт связывает идею с кодом Lean

Библиотека состоит из 82 контрактов методов. У каждого есть сторона для выбора и сторона для исполнения. Первая описывает назначение метода, его предпосылки, целевую конструкцию и ожидаемое действие.

Исполнительная сторона содержит ориентиры в Mathlib, проверенный пример или параметризованный каркас доказательства, а также список обязательств, которые останутся после применения метода. Например, контракт может свести исходную цель к проверке знака выражения и нескольким вспомогательным равенствам.

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

После фильтрации предложения ранжируются. Если особенно важен первый кандидат, система может ещё раз напрямую сравнить несколько лидеров. Выбранный контракт вместе с инструкциями передают в цикл, который пишет код Lean, компилирует его и исправляет ошибки.

Планы стоит менять только вместе с контуром проверки

Библиотеку построили по более ранним задачам Putnam, а проверяли на последующих задачах этого конкурса и на IMO ProofBench. Сравнение включало поиск по словам, поиск по векторным представлениям и повторное ранжирование с LLM; во всех вариантах LLM-селекторы запускали с одинаковой базовой моделью. На IMO ProofBench подходящий аннотированный метод попадал в первую пятёрку в 91,7% случаев против 88,3% у сильнейшего конкурента.

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

Проверка в полном цикле показывает направление эффекта. При бюджете в 10 компиляций Lean добавление выбранного контракта подняло долю решённых задач Putnam с 5,8% до 12,5%, а на IMO ProofBench — с 10,0% до 15,0%. При этом в цикл передавали весь контракт, поэтому эксперимент не разделяет пользу выбора и пользу готовых инструкций.

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

Заменять таким селектором проверку Lean нельзя: большинство задач в эксперименте осталось нерешённым. Работа меняет архитектуру этапа планирования, но не устраняет генерацию кода, компиляцию и исправление ошибок.

Источники

• Let the Library Speak: Self-Advertised Method Selection for Formal Proving

Иллюстрация: рисунок из статьи «Let the Library Speak: Self-Advertised Method Selection for Formal Proving», Xiaopeng Yuan, Suijin Wang, Yanli Wang и др., CC BY 4.0