ИИ Google DeepMind самостоятельно вывел и доказал математические закономерности для 11 машин Тьюринга

iXBT.com · 22.10.2026, 17:27:17

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