Вышли две новые опенсорсные LLM-ки для автоматического доказательства теорем.

-------
Вы помните, в прошлом году DeepMind делали заголовки AlphaProof'ом, который, как утверждалось, решил четыре задачи с последнего межнара, чего хватило бы на серебро. Но исходного кода нам не показали, лишь файлы со сгенерированными Lean-решениями этих четырёх задач.

Чуть позже DeepSeek выложили в опенсорс свою небольшую бям DeepSeek-Prover-V1.5 на 7B. Они реализовали версию метода Монте-Карло поиска по дереву всевозможных доказательств, как в шахматных движках. Модель занимается генерацией доказательства в Lean, а когда оно перестаёт компилироваться, она обрезает до первой ошибки и пробует с разными тактиками доказать промежуточные утверждения, которые приблизят её к цели. И поверх ещё обучение с подкреплением.

Главная проблема — в ограниченности обучающей выборки. Не так много кода люди написали в Lean; самый большой его источник — библиотека Mathlib.

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

-------
На этой неделе вышел Goedel-Prover, где авторы реализовали эту идею. Они начали с DeepSeek-Prover-V1.5 и построили цепочку из десяти моделей, последовательно генерирующих больше и больше верных доказательств. Последняя модель оказалась довольно сильной и выбила SOTA.

Другая недавняя статья предлагает Self-play Theorem Prover. Авторы берут тот же DeepSeek-Prover-V1.5 и делят его на conjecturer и prover. Идея в том, чтобы conjecturer переформулировал исходное утверждение, придумывал разные связанные гипотезы, а prover их доказывал. Они придумали интересный процесс обучения, чтобы заставить conjecturer изобретать нетривиальные, но и не совсем уж сложные гипотезы, которые действительно помогут в доказательстве. Они тоже выбивают SOTA (честно пишут, что восемь раз обучились на валидации).

Пруверы оценивают на трёх бенчмарках: школьные задачи (сейчас SOTA ~60%), университетские задачи — матан, линал, общая топология — сейчас SOTA 25%, и задачи с Putnam — олимпиада среди университетов — сейчас SOTA восемь задач (всего 664).

Забавная деталь о методологии: к каждой задаче генерируется несколько возможных решений, которые затем проверяются Lean'ом, и если нашлось подходящее — задача считается решённой. Например, 60% выше получаются, если разрешить DeepSeek-Prover-V1.5 генерировать по 102400 (сто тысяч) решений на задачу. А если только по 128, получается ~50%.

-----
Такие вот дела. И все эти модели маленькие, помещаются на одну домашнюю видеокарту. Можно запускать локально. Если теперь вставить туда по-настоящему большие модели, как Orion или грядущий GPT-5 со встроенным reasoning'ом могут получиться результаты поинтереснее. А пока чистая GPT-4o гордо решает ровно 1 (одну) задачу с Putnam.