Доказательные помощники в эпоху ИИ

Леонардо де Моура

ИИ преобразует то, как мы пишем формальные доказательства. Языковые модели уже могут генерировать тысячи строк проверенной математики при минимальном участии человека, и стоимость этого процесса продолжает снижаться. Это впечатляет и естественно поднимает вопрос: какую роль играет выбор доказательного помощника (proof assistant), если ИИ делает всё больше работы?

Я считаю, что эта роль становится важнее, а не менее значимой.

Доказательный помощник — это не просто инструмент для ИИ. Это среда, в которой человек и ИИ работают вместе. Человеку нужно читать определения, понимать формулировки теорем, направлять стратегию доказательства и строить дальнейшие результаты на уже верифицированных утверждениях. ИИ должен эффективно генерировать доказательства, учиться на обратной связи и опираться на автоматизацию. Хорошо спроектированный доказательный помощник обслуживает обе стороны, и именно поэтому архитектурные решения становятся ещё более важными по мере того, как ИИ берёт на себя всё большую часть работы.

ИИ усиливает вашу основу

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

Подумайте об этом так: калькулятор не делает математику неважной. Он позволяет пропустить рутинную арифметику и сосредоточиться на самой задаче. Но калькулятор полезен лишь настолько, насколько полезна математическая рамка, которую вы ему даёте. Представление имеет значение.

То же верно и для ИИ с доказательными помощниками. Языковая модель, работающая с системой зависимых типов, классами типов и хорошо спроектированным языком тактик, может выражать математические идеи на нужном уровне абстракции. Доказательства становятся короче, структура — яснее, а ИИ работает на более высоком уровне абстракции. Это накапливающийся эффект.

Масштабируемость — это настоящий тест

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

Краткие, хорошо структурированные доказательства становятся лучшими данными для обучения ИИ, что приводит к более качественным доказательствам, делает библиотеку полезнее, привлекает больше пользователей и участников. Это положительная обратная связь, и именно доказательный помощник заставляет её работать. И этому есть растущие подтверждения: Google DeepMind построил AlphaProof — систему на основе обучения с подкреплением, которая получила серебро на Международной математической олимпиаде 2024 года, — на базе доказательного помощника с большой и хорошо структурированной библиотекой. Как отметил Pushmeet Kohli из Google DeepMind, ключевыми факторами были «расширяемость и возможности верификации». Независимо от этого, Harmonic построила Aristotle, который достиг уровня золотой медали на IMO 2025, на той же основе. ByteDance’s SEED Prover показал серебряный уровень на том же соревновании, тоже на той же основе. Три независимые команды, решающие одну и ту же задачу на высшем уровне, выбрали доказательных помощников с выразительными типами, большой библиотекой и программируемой экосистемой. И это не случайность: выбор основы оказался важен для успеха.

Быстрая проверка доказательств тоже имеет значение. Когда ИИ исследует тысячи вариантов доказательства в петле обратной связи, скорость ядра напрямую влияет на то, сколько он успевает «узнать» за единицу времени. Это реальное инженерное ограничение, и доказательные помощники должны инвестировать в него. Но одной лишь скорости ядра недостаточно. Быстрое ядро без автоматизации и без выразительной типовой системы будет быстро проверять длинные доказательства, тогда как хорошо спроектированная система производит такие краткие доказательства, что скорость проверки редко становится узким местом. Эти две инвестиции дополняют друг друга.

Хорошая автоматизация, выразительные типы и чистая редукция по определению — это то, что делает возможными компактные доказательства. Это инфраструктура, которая позволяет и людям, и ИИ работать на правильном уровне абстракции.

От теории к практике

Любую математику, в принципе, можно формализовать в теории множеств или в любой достаточно выразительной основе. Это так же верно, как и то, что любую программу можно реализовать на машине Тьюринга. Теоретический тезис тут не вызывает споров.

Но разрыв между «формализуемо в принципе» и «практически осуществимо» — это как раз та область, где и живёт дизайн доказательного помощника. Зависимые типы делают практичной формализацию абстрактной алгебры, теории категорий и современной алгебраической геометрии без утопания в избыточных кодировках. Классы типов делают большую математическую библиотеку навигационной и композиционной. Доказательный помощник — это не просто ядро, проверяющее доказательства. Это целая среда, которая определяет, что удобно выражать и поддерживать в масштабе.

Читаемые спецификации: человеческий контракт

Доказательные помощники гарантируют корректность доказательств, но одной корректности недостаточно. Кто-то должен читать формулировки теорем и подтверждать, что они действительно выражают нужную математику. Это человеческий контракт, который не устраняет никакая автоматизация.

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

Это становится ещё важнее, когда ИИ сам генерирует доказательства. Проверенное доказательство теоремы, формулировку которой вы не можете разобрать, даёт вам очень мало. Нужно доверять не только доказательству, но и самой спецификации.

Можно возразить, что ИИ может переводить формальные формулировки в естественный язык, чтобы человеку было удобно читать «человеческую» версию независимо от формализма. Но это вводит новый источник ошибок именно в той точке, где корректность наиболее важна. Формальная формулировка — это якорь доверия. Представьте сценарий атаки: кто-то утверждает, что доказал важный результат. Вам нужно проверить именно формальную формулировку, а не пересказ ИИ. Читаемые формальные спецификации — это не удобство, которое может заменить ИИ. Это основа доверия.

Автоматизация как ходы в игре

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

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

Поэтому инвестиции в автоматизацию доказательств — процедуры принятия решений, упрощатели, универсальные тактики — это не просто улучшение удобства для человека. Они напрямую повышают качество и эффективность доказательств, генерируемых ИИ. Каждая мощная тактика — это новая возможность, которую ИИ может использовать.

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

Программируемая экосистема

Доказательный помощник, который одновременно является языком программирования, даёт нарастающее преимущество, которое легко недооценить. Когда тактики, автоматизация, метапрограммы и верифицированный код живут в одном языке, всё усиливает всё остальное. Новую автоматизацию может писать кто угодно, включая ИИ, без переключения контекста или языка. Граница между «использовать систему» и «расширять систему» исчезает.

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

Взгляд вперёд

Следующий великий доказательный помощник, вероятно, будет создан при огромной помощи ИИ. В Lean FRO мы уже приняли ИИ как часть процесса разработки. Это действительно меняет всё, и мы уже не представляем себе создание Lean без него. В наших репозиториях уже есть множество коммитов, написанных совместно с ИИ. И это будет только ускоряться. ИИ поможет нам проектировать, генерировать базовые библиотеки, писать автоматизацию и тестировать эргономику. Но критерии того, что делает доказательный помощник хорошим, не меняются. Ему по-прежнему нужны выразительные типы, читаемые спецификации, мощная автоматизация, программируемая экосистема, отличные инструменты и масштабируемость. ИИ меняет то, как мы строим доказательные помощники, а не то, что делает их хорошими.

Системы, которые существуют сегодня, их библиотеки, их архитектурные решения, накопленные знания о том, что работает, а что нет, становятся обучающими данными и языком проектирования для систем следующего поколения. Эта работа не пропадает зря. Она становится основой.

Никакая технология не живёт вечно, и это признак прогресса, а не провала. Цель не в том, чтобы создать систему, которая будет существовать бесконечно. Цель — сдвигать траекторию вперёд, делать формальную математику, верифицированное ПО и железо практичными, доступными и полезными, чтобы всё, что придёт потом, начиналось с более высокой точки.

Для меня важно, чтобы эта траектория определялась реальным техническим прогрессом. Критерии хорошего доказательного помощника в эпоху ИИ ясны, и сегодня они важны как никогда.

Об авторе

Леонардо де Моура (в русской транслитерации также встречается вариант «Леонарду ди Моура») — ведущий научный сотрудник (Senior Principal Applied Scientist) группы автоматизированных рассуждений в AWS, а также главный архитектор и сооснователь некоммерческой организации Lean FRO, занимающейся развитием доказательного помощника и языка программирования Lean.

Его исследовательские области — автоматизированные рассуждения, доказательство теорем, процедуры принятия решений, а также SAT- и SMT-решатели; он является главным архитектором двух ключевых систем в этой области — Lean и Z3. За вклад в эти системы он получил премии Herbrand и CAV, а также награду ACM SIGPLAN Software Award — причём дважды, за Z3 и за Lean.

В числе его текущих проектов — тактика grind для Lean, вдохновлённая современными SMT-решателями и объединяющая E-matching, замыкание конгруэнтности и линейную арифметику, а также фреймворк sym для построения масштабируемых инструментов верификации программного и аппаратного обеспечения. Среди его недавних текстов — «Proof Assistants in the Age of AI», где он рассуждает о том, почему архитектура доказательных помощников становится ещё важнее в эпоху ИИ (этот же материал упоминался в нашем предыдущем дайджесте по вычислительным моделям).