Система работает как игра: математик формулирует теорему для подсистемы Lean proof assistant (помощник, умеющий доказывать) и пишет слово «sorry» вместо доказательства. AlphaProof пытается заполнить пробел, то есть вписать вместо «sorry» полное доказательство.
ИИ-модель AlphaProof доказывает теоремы и находит ошибки в определениях
Группа специалистов Google DeepMind рассказала детали работы системы AlphaProof, которая год назад впервые в истории достигла уровня серебряной медали на Международной математической олимпиаде. Система использует подсистему Lean proof assistant (помощник, умеющий доказывать) и самообучается на 80 миллионах формальных математических утверждений, проверяя корректность своих решений автоматически.
На Международной олимпиаде по математике среди школьников модель AlphaProof заработала серебряную медаль. AlphaProof https://thesequence.substack.com/
Lean proof assistant (помощник, умеющий доказывать) — это программа, которая проверяет математические доказательства автоматически. Математик взаимодействует с ней пошагово: формулирует теорему, затем применяет тактики — высокоуровневые стратегии, которые помогают приблизиться к цели. На каждом шаге система обновляет текущую цель или вводит новые подцели в виде утверждений, которые тоже нужно доказать. Когда не остается недоказанных целей, это означает, что построен логический аргумент, который может проверить логический верификатор. Для ИИ это дает надежную обратную связь при обучении, а для математиков — гарантию корректности, в отличие от доказательств на естественном языке, где могут скрываться тонкие ошибки.
Попытка доказательства.
Инструмент особенно эффективен при работе со стандартными определениями из библиотеки mathlib, но испытывает трудности с нестандартными концепциями. Математик Алекс Конторович из Ратгерского университета отметил: «Этот диалог между высказыванием утверждений и проверкой, можно ли их доказать или опровергнуть, был критически важен для правильной формализации». Работа опубликована в журнале Nature.
Обучение модели
Схема обучения AlphaProof. Обучение модели искусственного интеллекта решению сложных математических задач. AlphaProof была обучена математические доказательства в три этапа. Первый этап представлял собой предварительное обучение, в ходе которого модель изучала логику, программирование и математический язык на основе набора данных, состоящего из кода и математического текста. Затем на этапе тонкой настройки модель была специализирована с использованием набора данных из утверждений, написанных на языке Lean proof assistant, математического инструмента, используемого для генерации доказательств. В основном цикле обучения модели был представлен «учебный план» задач, которые были переведены с естественного языка на формальный математический синтаксис. Модель пыталась генерировать доказательства с помощью подсистемы Lean, разбивая каждое из них на последовательность логических шагов, которые можно было проверить с помощью вычислений. По мере решения все большего числа задач модель адаптировала свой подход к генерации доказательств, что привело к улучшению ее производительности.
Обучение AlphaProof состояло из трех этапов. Сначала модель изучала логику и математический язык на текстах с кодом. Затем проходила тонкую настройку на тысячах доказательств, написанных людьми в подсистеме Lean. Наконец, система использовала языковую модель на базе Gemini для перевода математических утверждений из научных статей в формат Lean — процесс, называемый автоформализацией. Для каждого утверждения создавалось несколько вариантов перевода, и AlphaProof училась на них, даже если перевод был неточным.
Не все математики нашли инструмент полезным. Кевин Баззард из Имперского колледжа Лондона работал над переводом доказательства Великой теоремы Ферма в Lean и столкнулся с множеством специфических определений, с которыми AlphaProof не справилась.