Автоматическое доказательство теорем

Материал из MachineLearning.

Версия от 18:36, 6 июля 2026; Kirill Novoselov (Обсуждение | вклад)
(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)
Перейти к: навигация, поиск

Содержание

Автоматическое доказательство теорем (automated theorem proving, ATP) — область искусственного интеллекта, математической логики и теории программирования, изучающая методы машинного поиска и проверки формальных доказательств. В узком смысле ATP означает полностью автоматический поиск вывода в заданной логической системе. В широком современном смысле сюда относят также интерактивные ассистенты доказательств, SMT-решатели, SAT-решатели, системы формализации математики и нейросимвольные методы, в которых нейросеть предлагает шаги, а формальный проверяющий механизм удостоверяет корректность результата.

Центральная идея состоит в том, что математическое утверждение переводится на формальный язык, после чего доказательство становится конечным объектом, который можно проверить алгоритмически. Если проверка проходит, доверие к результату переносится с длинного человеческого рассуждения на сравнительно малое ядро формальной системы.

Изображение:Atp pipeline.png
Типичный цикл: формализация задачи, поиск доказательства и проверка малым доверенным ядром.

Мотивация

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

  • Проверка корректности. Формальный сертификат позволяет убедиться, что доказательство следует из явно заданных аксиом и уже доказанных лемм.
  • Поиск доказательств. Машина может перебрать множество вариантов вывода, применить леммы, переписать выражения, решить арифметические подзадачи или найти контрмодель.
  • Формализация больших теорий. Библиотеки вроде Mathlib в Lean и Mathematical Components в Coq/Rocq превращают фрагменты современной математики в проверяемый корпус.
  • Верификация программ и аппаратуры. Те же методы применяются к спецификациям компиляторов, протоколов, микропроцессоров и критически важных программ.
  • Обучение и объяснение. Ассистент доказательств делает скрытые зависимости явными и показывает, какие именно леммы нужны для вывода.

Проблема автоматического доказательства теорем отличается от обычного численного расчёта: требуется не только получить ответ, но и предъявить проверяемый вывод. Поэтому в современных системах различают поиск доказательства и проверку доказательства. Поиск может быть эвристическим, вероятностным или нейросетевым; проверка должна быть строгой.

Историческая справка

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

Обычно в истории ИИ ссылаются на Дартмутский семинар 1956 года, где был оформлен сам термин «искусственный интеллект». В тот же ранний период А. Ньюэлл, Г. Саймон и Дж. Шоу создали Logic Theorist, программу, доказывавшую теоремы из Principia Mathematica. Это был один из первых демонстрационных успехов символического ИИ.

В 1965 году Дж. Робинсон предложил метод резолюций для логики первого порядка. Вместе с унификацией он стал основой многих классических автоматических доказателей. В дальнейшем развились методы суперпозиции для равенств, табличные методы, переписывание термов, SAT и SMT-решатели, а также интерактивные системы, где человек управляет доказательством через тактики.

С конца XX века важную роль играют ассистенты доказательств: Mizar, HOL, Isabelle/HOL, Coq, Agda, Lean. Они сделали возможной формализацию крупных результатов: теоремы о четырёх красках, теоремы Фейта–Томпсона, существенных частей анализа, алгебры, топологии и теории чисел.

Формальная постановка

Пусть \Gamma — множество аксиом и уже доказанных утверждений, а \varphi — формула. Задача доказательства состоит в построении конечного объекта \pi, такого что \Gamma\vdash\varphi. Здесь \vdash означает выводимость в выбранной формальной системе.

Система автоматического доказательства обычно содержит:

  • формальный язык для записи утверждений;
  • правила вывода или типовую теорию, задающую корректные шаги;
  • алгоритм поиска или интерактивные тактики;
  • проверяющее ядро, принимающее или отвергающее найденный сертификат;
  • библиотеку определений и лемм.

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

Основные принципы

Формализация

Формализация переводит математическое высказывание с естественного языка в выражение формального языка. Например, утверждение «для всех натуральных n сумма первых n нечётных чисел равна n^2» должно быть записано через конкретные определения натуральных чисел, суммы, нечётности и степени.

Формализация трудна потому, что в обычной математике многие детали не проговариваются: области определения, неявные coercion-преобразования, выбор базовой теории множеств или типов, соглашения о равенстве структур. Ассистенты доказательств заставляют эти детали указать явно или вывести автоматически.

Поиск вывода

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

SAT-решатели работают с булевыми формулами, обычно в конъюнктивной нормальной форме. SMT-решатели расширяют SAT идеями из теорий: линейной арифметики, массивов, битовых векторов, неинтерпретируемых функций. Верификация программ часто сводит подзадачи именно к SMT.

Малое доверенное ядро

Многие системы строятся по архитектуре LCF: сложные тактики могут быть большими и эвристическими, но они не имеют права напрямую объявить теорему доказанной. Они должны построить объект, который принимает малое ядро. Это уменьшает доверенную часть системы.

Тактики

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

Curry–Howard

В теории типов используется соответствие Карри–Ховарда: утверждения рассматриваются как типы, а доказательства как термы этих типов. Проверить доказательство значит проверить тип терма. Этот принцип лежит в основе Coq/Rocq, Lean, Agda и ряда систем, связанных с конструктивной математикой.

Классические методы

Резолюция сводит доказательство от противного к выводу пустой дизъюнкции из множества дизъюнктов. Если отрицание цели вместе с аксиомами противоречиво, исходная цель доказана.

Унификация находит подстановки, делающие термы одинаковыми. Она необходима для применения общих лемм к конкретным выражениям.

Переписывание заменяет термы по равенствам и правилам редукции. В практических ассистентах оно используется постоянно: раскрыть определение, упростить арифметику, привести выражение к нормальной форме.

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

SAT/SMT эффективны для больших дискретных и арифметических подзадач. Они часто не заменяют ассистент доказательств, а служат внешними оракулами, выдающими сертификаты или проверяемые следы.

Современный инструментарий

Изображение:Atp tool landscape.png
Карта инструментов: автоматические доказатели, SMT/SAT, ассистенты доказательств, теория типов и нейросимвольные системы.

Lean

Lean — язык программирования и интерактивный ассистент доказательств на основе зависимой теории типов. Он используется как для формализации математики, так и для экспериментов с автоматическим доказательством. Экосистема Lean особенно известна библиотекой Mathlib, где формализованы большие разделы алгебры, анализа, топологии, комбинаторики и теории чисел.

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

Coq / Rocq

Coq — историческое название системы, ныне развиваемой как Rocq Prover. Это ассистент доказательств на основе исчисления индуктивных конструкций. Он позволяет записывать определения, программы и доказательства в единой конструктивной среде и извлекать программы из доказанных спецификаций.

С Coq/Rocq связаны крупные формализации: доказательство теоремы о четырёх красках, формализация теоремы Фейта–Томпсона, сертифицированный компилятор CompCert, библиотеки Mathematical Components и Software Foundations. Система также использовалась как платформа для развития гомотопической теории типов и унивалентных оснований.

Homotopy Type Theory

Гомотопическая теория типов (homotopy type theory, HoTT) — направление, связывающее зависимую теорию типов с гомотопической топологией. В HoTT типы интерпретируются как пространства, элементы как точки, а равенства как пути. Центральную роль играет аксиома унивалентности В. Воеводского: эквивалентные структуры можно отождествлять как равные в подходящем формальном смысле.

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

Нейросетевые методы и IMO

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

В 2024 году Google DeepMind представила системы AlphaProof и AlphaGeometry 2, которые вместе решили четыре из шести задач Международной математической олимпиады 2024 года и набрали 28 баллов из 42, что соответствует уровню серебряной медали. AlphaProof использовал формальный язык Lean: языковая модель переводила задачи и варианты рассуждений в формальные утверждения, а система поиска, связанная с идеями AlphaZero, искала доказательства и получала подкрепление от успешной проверки. AlphaGeometry 2 был нейросимвольной системой для геометрии: языковая модель предлагала вспомогательные построения, а символический движок проверял геометрические следствия.

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

Формализация Великой теоремы Ферма и найденная ошибка

Проекты формализации показывают, что ассистенты доказательств полезны не только для новых доказательств, но и для проверки оснований уже известных результатов. В проекте формализации Великой теоремы Ферма в Lean возникла ситуация, описанная Кевином Баззардом в декабре 2024 года: при формализации теории разделённых степеней, необходимой для построений в кристаллической когомологии, Lean не принял человеческое изложение одного стандартного аргумента. При внимательной проверке выяснилось, что ключевая лемма в работе Н. Роби, на которую опиралась литература, в такой формулировке кажется неверной; в применении выпадал один тензорный множитель.

Важно, что речь не шла о прямом опровержении Великой теоремы Ферма или доказательства Уайлса. Проблема находилась в технической литературной базе, через которую современный формализационный маршрут строит необходимые объекты. Позднее был найден обход: Б. Конрад указал на другой подход в приложении к книге Бертло–Огюса по кристаллической когомологии, после чего «доказательство снова стало на рельсы». Этот эпизод иллюстрирует практический смысл формализации: компьютер не «понимает авторитет» стандартного текста, а требует точного проверяемого перехода.

Ограничения

Автоматическое доказательство теорем не является универсальным решателем математики. Основные ограничения таковы:

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

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

См. также

Ссылки

Источник — «http://machinelearning.ru/wiki/index.php?title=%D0%90%D0%B2%D1%82%D0%BE%D0%BC%D0%B0%D1%82%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%BE%D0%B5_%D0%B4%D0%BE%D0%BA%D0%B0%D0%B7%D0%B0%D1%82%D0%B5%D0%BB%D1%8C%D1%81%D1%82%D0%B2%D0%BE_%D1%82%D0%B5%D0%BE%D1%80%D0%B5%D0%BC»
Личные инструменты