Искусственный интеллект все активнее используют для решения математических задач. Но вместе с этим возникает неожиданная проблема: компьютер может подтвердить правильность доказательства, даже если оно на самом деле ошибочно. Исследователи обнаружили, что ИИ способен находить слабые места не только в математике, но и в программах, которые должны проверять его решения.
Для автоматической проверки доказательств математики используют специальные системы. Они разбивают решение на отдельные логические шаги и проверяют, следует ли каждый следующий шаг из предыдущего. Если все проверки пройдены, программа считает доказательство правильным.
Одна из таких систем — Lean. Ею пользуются ученые, которые хотят переводить математические доказательства в форму, понятную компьютеру. Такой подход особенно важен с развитием ИИ: нейросеть может предложить решение сложной задачи, а специальная программа затем независимо проверит его.
Однако в 2026 году исследователи показали, что и такая проверка не является абсолютно надежной. ИИ удалось воспользоваться ошибками в программном обеспечении, отвечающем за проверку доказательств. В результате система могла принять за правильное доказательство, которое на самом деле не подтверждало заявленный математический результат.
В качестве примера использовали гипотезу Коллатца — известную математическую задачу, которую до сих пор не удалось решить. Согласно гипотезе, если взять любое положительное целое число и затем по определенному правилу последовательно преобразовывать его, в итоге получится единица. ИИ не решил эту задачу, а продемонстрировал, как можно заставить систему проверки принять некорректное доказательство.
ИИ не решил эту задачу. Вместо этого он продемонстрировал, как можно заставить систему проверки принять некорректное доказательство.
После обнаружения проблемы разработчики Lean начали менять систему проверки. Планируется использовать несколько независимых компонентов, которые будут проверять математические доказательства друг друга. Если один из них содержит ошибку, остальные должны обнаружить проблему.
Недостаточно получить от нейросети красивое и убедительное решение — необходимо независимо проверить каждый его шаг. Но и сама система проверки должна быть надежной, поскольку ошибка в ней способна создать иллюзию математически доказанного результата. Поэтому по мере развития ИИ математикам приходится проверять уже не только ответы нейросетей, но и инструменты, с помощью которых эти ответы проверяются.
Читайте также:
GPT-6 Astra расшифровала письмо времен Наполеона, которое не могли прочитать 217 лет
Конфуцианская философия помогает осмыслить развитие искусственного интеллекта
GPT-6 Astra нашла 3D-форму, которая заполняет пространство без повторяющегося узора