📌LEAP: система, которая помогла LLM решить все задачи олимпиады Putnam 2025

Google опубликовала интересный пейпер о системе LEAP, предназначенной для автодоказательства теорем. Она позволяет языковым моделям строить формальные, машинно проверяемые доказательства на языке Lean.

Доказательство на естественном языке трудно проверить автоматически - оно почти всегда содержит логические пробелы.

Формальное доказательство записывается на машинном языке и проверяется компилятором, что даёт гарантию корректности, но писать его значительно сложнее.

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

Главная исследовательская победа проекта - олимпиада Putnam 2025, ежегодное соревнование по математике для студентов в США.

LEAP формально решила все 12 задач, тогда как ни Gemini 3.1 Pro сама по себе, ни открытый специализированный прувер Goedel-Prover-V2 не решили ни одной.

Закрытую систему Aristotle, получившую на математической олимпиаде IMO 2025 результат уровня золотой медали, авторы в собственных тестах оценили в 9 решённых задач из 12.

В рамках работы также представлен набор IMO-LeanProofBench из 60 формализованных в Lean задач олимпиадного уровня, требующих весьма нестандартных выводов и структурно сложных доказательств.

На нём LEAP, что неудивительно, достигает в среднем по basic и advanced сэтам около 70% против примерно 48% у Aristotle.

Попутное достижение - LEAP формально проверила вспомогательную часть одной из комбинаторных задач, восходящих к математику Дональду Кнуту, сгенерировав более 5000 строк кода на Lean 4.

🟡Стоит отметить иронию

В статье авторы критикуют закрытые системы-конкуренты (Axiom3, Numina, Aristotle) за то, что те недоступны для научной проверки. При этом код самого LEAN тоже не опубликован.

Открытие итоговых доказательств это частично смягчает (их можно перепроверить компилятором Lean), но полная воспроизводимость гугловского проекта пока невозможна.


@ai_machinelearning_big_data

#AI #ML #LLM #LEAP #Research #Google