Учёные научили ИИ отличать интересные математические теоремы от скучных
Языковые модели всё лучше решают сложные математические задачи, включая проблемы, десятилетиями остававшиеся открытыми. Это открывает путь к расширению математического знания в беспрецедентных масштабах, но остаётся открытым вопрос: интересно ли и полезно ли то новое знание, которое производят ИИ-системы, или это просто поток технически верных, но малоценных утверждений.
Авторы работы предлагают конкретный количественный ответ. Они определяют «внутреннюю интересность» теоремы как отношение длины её доказательства к длине формулировки: чем сложнее и длиннее доказательство относительно самого утверждения, тем теорема содержательнее. Показано, что эта простая метрика сильно коррелирует с независимой, «внешней» оценкой практической полезности теоремы, то есть короткая формула не врёт и действительно отражает ценность результата.
Ключевым строительным блоком для расчёта метрики стала сложность доказательства при заданном наборе исходных посылок (премисс). Для её предсказания авторы обучили модель размером 27 миллиардов параметров, которая оценивает сложность доказательства точнее, чем современные универсальные (frontier) модели общего назначения.
Когда систему настроили на оптимизацию именно этой метрики интересности, она начала производить заметно более оригинальные теоремы: пересечение (совпадение по существу или полностью) с содержимым библиотеки формальной математики Mathlib упало с 91,9% до 30,6%. Это означает, что система стала генерировать математику, куда менее похожую на уже известную, то есть по-настоящему новую, а не переформулировки существующих результатов.
Система умеет не только оценивать, но и сама предлагать теоремы-кандидаты, отбирать среди них наиболее интересные и на этой основе итеративно наращивать самопополняющуюся математическую библиотеку. По словам авторов, предложенные метрики дают практический и измеримый сигнал для ранжирования гипотез и направления поиска доказательств внутри формальных математических библиотек, открывая путь к самопополняющимся, машинно-проверяемым библиотекам, которые сами выбирают достойные внимания утверждения, без опоры на заранее заданные человеком цели.
Ключевые факты
- Интересность теоремы формально определена как отношение длины доказательства к длине формулировки
- Эта метрика сильно коррелирует с независимой оценкой практической полезности теоремы
- Обучена модель на 27 млрд параметров, предсказывающая сложность доказательства точнее универсальных моделей общего назначения
- Оптимизация под метрику снизила совпадение генерируемых теорем с библиотекой Mathlib с 91,9% до 30,6%
- Система способна сама генерировать, отбирать и итеративно наращивать самопополняющуюся библиотеку формальных теорем
Почему это важно
ИИ-модели уже умеют доказывать сложные теоремы, но до сих пор не было хорошего способа отличить содержательный математический результат от тривиального переформулирования известного факта. Предложенная метрика, простое отношение длины доказательства к длине формулировки, даёт измеримый и, что важно, проверенный на корреляции с полезностью критерий качества автоматически генерируемой математики.
Кому это важно
Разработчикам систем автоматического доказательства теорем и формальных математических библиотек (вроде Mathlib), исследователям в области ИИ для науки, а также тем, кто занимается автоматизацией научного открытия и оценкой качества генерируемого моделями контента за пределами естественного языка.
Как это применить
Метрику и обученную модель предсказания сложности доказательства можно использовать как сигнал для ранжирования гипотез и направления поиска доказательств: вместо перебора случайных утверждений система целенаправленно выбирает и развивает те теоремы, которые с большей вероятностью содержательны и малопохожи на уже известные результаты, постепенно наращивая библиотеку формально проверенной математики.
Можно ли доверять
Источник, препринт исследовательской работы с конкретными количественными результатами (обучена модель на 27 млрд параметров, приведены цифры снижения пересечения с Mathlib с 91,9% до 30,6%), но в доступном тексте не указаны авторы, аффилиации и дата публикации, а также нет названий конкретных сравниваемых «универсальных моделей общего назначения», это стоит учитывать как ограничение при оценке заявленного превосходства.
Риски и подводные камни
Сама метрика интересности (отношение длины доказательства к длине формулировки), эвристика, и хотя авторы показывают её корреляцию с полезностью, длина доказательства не гарантирует глубины или значимости результата: система может генерировать формально сложные, но математически малоценные для человека теоремы. Кроме того, отсутствие подробностей о методике расчёта сложности доказательства и о том, с какими именно моделями проводилось сравнение, затрудняет независимую проверку заявленных цифр.