В последние месяцы резко выросло число доказательств старых и новых математических результатов, сгенерированных с помощью ИИ, часть из которых формализована на языке proof assistant'а Lean. Проверить, что конкретный Lean-репозиторий действительно доказывает заявленное утверждение, — задача не тривиальная, особенно для тех, кто не является экспертом в Lean: нужно убедиться, что заявленные формальные утверждения имеют доказательства, проходящие typecheck, что в доказательствах нет «читерства» вроде добавления посторонних аксиом, и что формальные утверждения семантически соответствуют неформальному описанию заявленных результатов.

Чтобы внести ясность в эту ситуацию, Terence Tao объявил об открытии для приёма заявок реестра Palomar — инициативы, запущенной при поддержке Lean FRO и ICARM. Тао входит в число участников проекта в нескольких ролях, включая научный консультативный совет, вместе с Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Ravi Vakil и Akshay Venkatesh.

Подробное обоснование идеи Palomar изложено здесь, а дополнительная информация о проекте — здесь. В первом приближении Palomar задуман как аналог препринт-сервера, но для доказательств на Lean. Название происходит от астрономической обсерватории: сервис представляет собой реестр внешних GitHub-репозиториев (точнее, «снапшотов» таких репозиториев, зафиксированных конкретным коммитом) с Lean-кодом, соответствующим текущим лучшим практикам формализации. В частности, каждый такой репозиторий должен содержать:

  • «Challenge-файл» — короткое, человекочитаемое описание заявленных результатов на Lean.
  • «Модуль решения» — доказательство (произвольной длины) результатов, заявленных в challenge-файле.
  • Файл «formalization.yaml» с неформальным описанием результатов на естественном языке и рядом других метаданных.

(Есть и дополнительные технические требования к репозиторию, которые здесь опущены.) При подаче снапшота репозитория в Palomar проверяется: (а) что модуль решения проходит typecheck и доказывает ровно те результаты, что заявлены в challenge-файле, и (б) что неформальное описание результата в formalization.yaml соответствует заявленному в challenge-файле, а сам репозиторий отвечает минимальным требованиям для записи в реестр. Проверка (а) полностью механическая и выполняется инструментом Lean — Comparator; проверка (б) недетерминированная и выполняется большой языковой моделью. Если репозиторий проходит обе проверки, он регистрируется в Palomar. Важно подчеркнуть: проверки (а) и (б) значительно уступают полноценному человеческому рецензированию по новизне, интересу и точности результата — Palomar не является рецензируемым журналом.

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

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

Обсуждение и обратная связь по Palomar ведутся в этом Zulip-канале.

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

Как сказано выше, Palomar не выполняет человеческое рецензирование репозиториев — это не масштабируется на тот объём репозиториев, который планируется обрабатывать. (Это похоже на arXiv, который выполняет минимальные проверки приемлемости препринтов, но также не проводит человеческого рецензирования.) Однако мы не против того, чтобы сторонние сервисы выполняли дополнительную проверку поверх минимальных проверок Palomar.

На вопрос о выборе GitHub в качестве единственной платформы для хостинга репозиториев и рисках, связанных с этим, последовал такой комментарий:

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

David Bevan обратил внимание на то, что записям в реестре не хватает понятного названия и аннотации в духе arXiv, из-за чего сложно понять, что именно доказывает та или иная заявка. Tao согласился передать замечание разработчикам, пояснив, что сейчас используются поля project.name и project.description из файла formalization.yaml, но они не полностью соответствуют формату «название + аннотация» препринта, поскольку заявляемый результат может быть лишь частью содержимого репозитория, а не всем проектом целиком.

Отдельно обсуждался вопрос о больших формализациях — например, репозитория, покрывающего целую статью с сотнями определений и теорем. Tao уточнил, что на challenge-файл действует жёсткое ограничение — 1000 строк и 100 КБ, чтобы файл оставался человекочитаемым и пригодным для проверки ИИ (предпочтительный размер — существенно меньше, порядка 300 строк). Если результатов слишком много для одного файла, потребуется несколько отдельных записей в реестре — по одной на каждый крупный результат. Если же для формализации нужны обширные определения, которых ещё нет в Mathlib, их можно вынести в отдельный репозиторий Tau Ceti и подключить как зависимость к challenge-файлу.

Также прозвучал вопрос о том, допустимо ли регистрировать важные результаты в Palomar до публикации препринта, пока текст статьи ещё пишется — обсуждение этого вопроса в комментариях осталось незавершённым на момент публикации.