🔥 AlphaProof Nexus: формальные доказательства начинают превращаться в инженерный пайплайн

Google DeepMind показали AlphaProof Nexus - систему, которая автономно закрыла 9 открытых задач Эрдёша, часть из которых висела десятилетиями. По оценке авторов, стоимость решения одной задачи составила всего несколько сотен долларов.

Кроме этого, система доказала 44 открытые гипотезы из OEIS, закрыла 15-летний вопрос в алгебраической геометрии и нашла новый алгоритмический параметр в оптимизационной теории, который раньше не был описан людьми.

Модель генерирует идеи и фрагменты доказательств, а Lean проверяет каждый логический шаг через компилятор. Если доказательство некорректно, оно просто не проходит проверку. Не нужен рецензент, который вручную ищет дыру в рассуждении.

Базовый агент, который просто чередует генерацию LLM и обратную связь от компилятора, смог повторить все 9 успешных решений задач Эрдёша. Более сложная версия с эволюционным поиском и reinforcement learning дала заметный выигрыш только на самых тяжёлых случаях.

Чем сильнее становятся foundation models, тем чаще простые циклы «сгенерировал - проверил - исправил» начинают догонять специализированные архитектуры.

Отличие от неформального подхода к математическим доказательствам принципиальное. Модель часто придумывала несуществующие леммы, ссылалась на «известные результаты» и пыталась спрятать сложность задачи в вспомогательное утверждение. В обычном текстовом доказательстве такие ошибки легко пропустить. Lean отсекает их сразу.

Ещё один неожиданный эффект: агент находил неточности в формализациях уже существующих математических утверждений. То есть он работал не только как решатель, но и как диагностический инструмент для самой постановки задачи.

Успехи пока сосредоточены там, где библиотека Lean уже достаточно зрелая: комбинаторика, теория чисел, оптимизация. Задачи, где нужно строить большой пласт новой теории, всё ещё далеко не закрыты. И большинство задач Эрдёша система не решила.


Та же схема подходит для кодигша, спецификаций, верификации протоколов, компиляторов, криптографии.

Формальная проверка отсекает галлюцинации.
Модель может придумать лемму или сослаться на несуществующий результат, но Lean это не пропустит.


@Python_Community_ru