Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Языковую модель научили отбирать математические гипотезы, которые коротко формулируются, но требуют длинного формального доказательства. В работе FAIR @ Meta, CERMICS, ENPC, Institut Polytechnique de Paris и New York University средняя «интересность» выросла вчетверо, а доля генераций с существенным или полным совпадением с mathlib снизилась с 91,9% до 30,6%. Хотя препринт не рецензирован и все числа получили сами авторы, работа предлагает практический сигнал для систем, которые должны сами выбирать следующие задачи.
Как измерили интересность теоремы
Авторы называют теорему интересной, если её легко сформулировать, но трудно доказать из доступных предпосылок. Метрика делит сложность доказательства на длину описания теоремы: чем больше результат, тем выше теорема в списке кандидатов.
Длина описания включает не только саму формулировку на Lean 4, но и определения, которых ещё нет среди предпосылок. Это мешает повысить оценку искусственно: нельзя склеить несколько несвязанных утверждений и получить «сложную» теорему лишь за счёт длинного доказательства — вместе с ним вырастет знаменатель.
Сложность доказательства зависит от контекста. Если библиотека уже содержит подходящую лемму, путь становится короче; если лемму убрать, потребуется заново вывести её результат. Оценщик должен учитывать эту разницу, а также не предсказывать рост сложности после добавления новых предпосылок.
Для обучения взяли около 100 тысяч примеров из mathlib. Авторы разворачивали граф зависимостей: убирали из контекста готовую лемму, подставляли её предпосылки и прибавляли длину её доказательства. На этих данных дообучили Qwen3.6-27B, который точнее GPT-5.5 и Claude Opus 4.6 предсказывал длину доказательств; при этом все сравниваемые модели недооценивали самые длинные случаи.
Отдельная метрика оценивает полезность теоремы: сколько строк удалось бы не повторять в последующих доказательствах, если добавить её в библиотеку. В mathlib полезность и интересность связаны с ранговой корреляцией 0,756. Поэтому отношение длин можно применять до того, как у новой теоремы появятся зависимые от неё результаты.
Как сигнал управляет расширением библиотеки
Система начинает с набора формальных предпосылок и просит Claude 4.6 предложить 400 новых утверждений. Семантический фильтр удаляет эквивалентные гипотезы и поддерживает разнообразие, после чего Claude Code пытается построить доказательства на Lean. Проверенные утверждения ранжируются, а десять лучших переходят в библиотеку и становятся предпосылками следующего раунда.
Такой цикл повторили шесть раз. Отбор по интересности сравнили с сохранением всех доказанных утверждений, случайным выбором и отбором по одной только длине доказательства. Отношение длины доказательства к длине формулировки дало более высокую среднюю интересность, а модель-оценщик Claude 4.6 также поставила этим наборам более высокие оценки за качество и разнообразие.
Разница с отбором по длине доказательства существенна для архитектуры системы. Длинный формальный код сам по себе может появиться из-за громоздкой формулировки или стиля тактик Lean. Нормализация по длине описания отдаёт приоритет компактным утверждениям, которые скрывают длинную цепочку вывода.
Для продукта это ранжировщик, а не автономный математик
Работа меняет планы команд, которые строят поиск по формальным библиотекам. Между генератором гипотез и доказателем появляется отдельный оценщик: он может отсеять слабые кандидаты до дорогого поиска доказательства. Если доказательство уже найдено, вместо прогноза можно использовать его фактическую длину.
Получается конвейер из генератора, фильтра повторов, формального проверяющего агента, ранжировщика и хранилища новых предпосылок. Веса генератора не обязательно обновлять после каждого цикла: библиотека расширяется за счёт отбора на этапе выполнения, а принятые теоремы меняют контекст следующего запуска.
Проверки ограничены формальными утверждениями Lean 4 и структурой mathlib. Итеративные опыты охватывают теорию графов, алгебру, теорию меры и вероятностей, а также теорию чисел. Система пока добавляет теоремы, но не создаёт новые определения; кроме того, эксперимент показывает высокую оценку выбранных утверждений, а не то, что они действительно помогают доказывать будущие результаты.
Метрика также не охватывает историческую значимость, связь с физическим миром или объединение далёких разделов математики. Длина кода зависит от выбранных тактик: автоматизация способна заменить много строк вычислительным временем. Поэтому сигнал подходит для управления поиском внутри конкретной формальной среды, но не служит общей оценкой математической ценности.
Источники
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
