Gemini научился находить и формально доказывать новые закономерности в работе вычислительных машин Исследователи Google DeepMind и Кембриджского университета разработали систему на базе Gemini, которая самостоятельно обнаружила новые математические закономерности в работе 11 машин Тьюринга и формально доказала их корректность. Система не просто анализировала заранее сформулированную математическую задачу: она выдвигала гипотезы о поведении вычислительных машин, разрабатывала правила для их описания и проверяла доказательства с помощью системы Lean 4. Машина Тьюринга — абстрактная модель компьютера, которая выполняет инструкции, записывая символы на ленту, перемещаясь по ней и меняя внутреннее состояние. Несмотря на простоту устройства, поведение таких машин может быть чрезвычайно сложным. Исследователи изучали задачу Busy Beaver, которая заключается в поиске машины с заданным числом состояний, способной проработать максимальное количество шагов до остановки. Для машин с шестью состояниями и двумя символами остаются экземпляры, для которых учёные пока не установили, завершится ли выполнение программы. Для анализа этих случаев команда создала агентную систему, которая объединяет несколько этапов исследования. Сначала алгоритмы выявляют повторяющиеся структуры в результатах симуляции машин. Затем языковая модель Gemini использует их для выдвижения гипотез и построения компактных математических правил, описывающих поведение программы. После предварительных проверок система формирует доказательство, а затем переводит его в формальный вид и проверяет в Lean 4 — среде, которая позволяет строго удостовериться в корректности математических рассуждений. Источник изображения: сгенерировано Muse В результате система вывела и формально подтвердила новые правила для 11 машин из класса BB(6), для которых ранее не было задокументированного анализа. Эти правила позволяют описывать сразу множество шагов вычисления, вместо того чтобы проверять каждый шаг по отдельности. По своей структуре обнаруженные закономерности напоминают системы, связанные с гипотезой Коллатца: поведение вычислительной машины можно представить через последовательность арифметических преобразований. Авторы также получили формальные доказательства похожих правил или новые способы ускорения анализа ещё для 15 машин, которые уже изучались математическим сообществом. Однако исследователи не решили главную загадку этих 11 машин: пока неизвестно, останавливаются ли они. Найденные правила точно описывают их поведение, но не обязательно позволяют определить, закончится ли вычисление. Поэтому авторы предлагают предварительно относить такие экземпляры к категории Cryptids — машин, для которых существует компактное математическое описание работы, но вопрос об остановке остаётся открытым. Окончательное признание этой классификации зависит от принятия результатов научным сообществом. Работа демонстрирует возможность перехода от ИИ, решающего поставленные человеком задачи, к системам, способным самостоятельно находить математические структуры и доказывать полученные результаты. При этом возможности нынешнего подхода ограничены: система ориентирована на обнаружение закономерностей, похожих на те, что возникают в задачах типа Коллатца. Авторы рассматривают расширение метода на другие виды вычислительного поведения как направление дальнейших исследований. В перспективе подобные агенты могут стать инструментом для самостоятельного поиска и формализации новых математических вопросов, хотя решение принципиально неразрешимых задач таким способом не гарантируется.