Введение в принципы бережливого производства для программистов

Синтаксис и семантика математики

Делиться

Введение в системы автоматического подтверждения доказательств

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

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

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

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

1. Создание доказательства похоже на программирование.
2. В условиях начала века я никак не могу заниматься математикой. Мне нужна интегрированная среда разработки (IDE) с подсказками типов, подсветкой синтаксиса и подробными сообщениями об ошибках, и я должен взаимодействовать с ней в интерактивном режиме.

Мои мысли не были новыми. Первая идея называется соответствием Карри-Ховарда, объяснение которого приведено ниже. Последняя является целью систем автоматического доказательства, таких как Lean и их расширения для IDE (обычно это расширение для VS Code).

Интерактивные системы доказательства против автоматических систем доказательства теорем

Системы проверки теорем, такие как ядро Lean, могут определить, являются ли выражения корректными, допустимы ли шаги проверки и корректен ли окончательный вывод. Интерактивные помощники по доказательствам основываются на них и также помогают вам строить доказательства и предлагают шаги. Автоматические доказывающие теоремы (АТП) пытаются найти доказательство самостоятельно, используя методы искусственного интеллекта. Lean работает как система проверки доказательств и помощник, но хорошо сочетается с генеративным ИИ, эффективно функционируя в качестве АТП.

Теренс Тао транслирует на своем YouTube-канале доказательства, созданные с помощью ИИ, используя Lean 4 и GitHub Copilot. Большинство заголовков типа «ИИ только что решил открытую проблему, существовавшую x лет», вероятно, были формализованы с помощью Lean (пример 1, пример 2 и 3). Проекты и бенчмарки ИИ, такие как LeanDojo, miniF2F, ProofNet, PutnamBench, FormalMATH, используют Lean. OpenAI и Meta обучили модели для использования Lean, а AlphaProof от DeepMind использовала его для завоевания серебряной медали на Международной математической олимпиаде.

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

Переписка Карри-Ховарда

Начнём с простой логической теоремы, которую вам, возможно, придётся доказать на курсе логики в университете:

(P → Q → R) → (P ∧ Q → R)

Оператор → обозначает логическую импликацию, но в соответствии Карри-Ховарда между доказательствами и компьютерными программами его можно читать как функцию. ∧ — это логическое «и». Проще говоря, мы спрашиваем, истинно ли следующее утверждение: «Если у меня есть функция, которая, если задано P, порождает функцию из Q в R, то если у меня уже есть и P, и Q, я могу породить R».

Примечание: (P → Q → R) — это «каррированная функция» (Haskell Curry тоже виноват), и синтаксис эквивалентен (P → (Q → R)) . В терминах программирования это функция, которая возвращает другую функцию, которую впоследствии можно вызвать как foo(bar)(baz) . Логически это эквивалентно тому, что foo получает bar и baz в виде кортежа foo((bar, baz)) , но именно это мы и пытаемся доказать здесь. Аналогично, всё предложение можно записать как (P → Q → R) → P ∧ Q → R

Давайте рассмотрим конкретный пример: если у меня есть торговый автомат, который, получив монету (P) возвращает стаканчик лапши быстрого приготовления (Q → R) , а получив горячую воду (Q) возвращает лапшу (R) , то это означает, что я могу создать систему, которая, получив на вход и монету, и горячую воду (P ∧ Q) , вернет лапшу.

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

Попробуйте в среде разработки TypeScript, любые изменения приведут к ошибкам типов.

Написано в общем и упрощенном виде (игровая площадка):

Мы определили функцию — нашу теорему — которая принимает в качестве параметра каррированную функцию (P → Q → R) и выдает функцию, которая принимает произведение типов P ∧ Q и выдает R , то есть (P ∧ Q → R) . Эта функция выступает в качестве «свидетеля» истинности логической теоремы. Доказательство выглядит корректным и даже удовлетворяет типам , которые определяют исходную теорему в TypeScript:

Давайте сформулируем это ещё более убедительно: доказательство корректно, потому что оно удовлетворяет типу. Утверждения — это типы, а доказательства — это термины этих типов. Мы также видели, что конъюнкции ∧ являются произведениями типов/кортежами, и что логические импликации Q → R — это функции (q: Q) => R Стрелка эквивалентна как синтаксически, так и семантически.

Давайте внедрим это в рамках концепции Lean:

Вы можете поиграть с этим на игровой площадке Lean.

example — это способ определения анонимных объявлений только для проверки типов (в отличие от theorem о ключевых словах), а его тип (то, что следует за двоеточием : вплоть до определения := ) — это наша теорема. Доказательство достигается, когда определение «обитает» в этом типе. Как это модно в функциональном программировании, применение функции — это просто пробел: самая фундаментальная операция отображается на самый базовый оператор в языке. P ∧ Q — это тип произведения/кортеж, и доступ к его элементам осуществляется через .left и .right .

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

Другие письма Карри и Ховарда

* Лучшим типом суммы было бы дискриминированное объединение: { tag: “left”; value: P } | { tag: “right”; value: Q }

То, чего вы ещё не видели

Зависимые типы

Рассмотрим следующий, более сложный тип:

Это означает: «Для всех значений ( ∀ ) x , являющихся натуральными числами, 0 меньше или равно x ». Первое, что бросается в глаза, — это математические символы Unicode; их можно либо автоматически дополнить в IDE с помощью forall , либо просто заменить ключевым словом ASCII forall .

Нам кажется, что это не похоже на тип. Тип зависит от значения x — то, что мы обычно получаем из сложных библиотек проверки типов, таких как Zod, а не из статических средств проверки типов, таких как TypeScript. Это тип, который «зависит» от значений. Однако типы Lean не полагаются на проверки во время выполнения, как это делает Zod; это все еще тип, хотя и сложный. Это является источником путаницы при чтении синтаксиса Lean.

Вселенные

В песочнице или IDE мы можем проверить тип терминов с помощью #check :`.

Теперь давайте проверим тип Nat :

Nat относится к Type . Но зачем останавливаться на достигнутом?

Type — это тип Type 1 , и так далее. Это показывает, что в Lean нет четкого синтаксического различия между типами и терминами. Типы — это термины, которые имеют свои собственные типы, расположенные, как слои луковицы — эти слои называются «вселенными». 3 — это термин типа Nat , а Nat — это термин типа Type , Type n имеет тип Type Type (n+1) , и так далее.

В рамках подхода Lean необходимо отслеживать уровни вселенных, чтобы избежать парадокса парикмахера: «Парикмахер бреет всех, кто не бреется сам, разве сам парикмахер бреется?» В случае вселенных типов парикмахер — это процедура, тип которой может оперировать только над элементами типа из вселенной ниже, он не может оперировать элементами своего собственного уровня, включая самого себя. Это позволяет избежать самореферентных парадоксов, которые могли бы вызвать противоречие. Противоречие означало бы, что мы могли бы доказать истинность утверждения False и, таким образом, доказать все остальные утверждения.

Предложения

Давайте попробуем еще более сложный вариант:

Проще говоря: «Верно ли это? Для каждого натурального числа x , y , z и n , имея доказательство того, что n > 2 и x * y * z ≠ 0 , мы можем привести доказательство того, что xⁿ + yⁿ ≠ zⁿ ».

Это Великая теорема Ферма, которая ошеломляла математиков на протяжении 358 лет после того, как Ферма заявил, что его собственное доказательство не помещается на полях страницы. В определении используется sorry , что является заполнителем для неполного доказательства. Программа скомпилируется, но выдаст сообщение: declaration uses `sorry` . Это похоже на использование any в TypeScript для подавления ошибок типов, но рецензент может это заметить и попросить исправить ошибку линтера. Предоставление этого доказательства — ваша «цель».

Давайте вернемся к чему-нибудь попроще:

Это абсурд. Как я могу определить термин, тип которого равен 2 + 2 = 4?

Начнём с рассмотрения типа:

Тип — это Prop , сокращение от proposition (предложение). Предложение — это утверждение, которое может быть истинным или ложным. Как мы уже говорили выше, в соответствии с правилом Карри-Ховарда, предложение — это тип, а доказательство — это терм или программа этого типа. Предложение истинно, если тип имеет «обитателя», и ложно, если его нет. Lean не «преобразует» предложение в логическое значение «истина» или «ложь» в вычислительном смысле; мы просто говорим, что оно «истинно» или «ложно». Использование Lean в качестве помощника для доказательств означает работу в основном с предложениями.

В фоновом режиме средство проверки типов Lean нормализует этот тип до 4 = 4 , но не более того. Нам нужно лишь предоставить терм, который находится в этом нормализованном типе. Мы делаем это с помощью rfl , конструктора сущностей, автоматически импортируемого из пакета Prelude в ваше пространство имен.

Это работает. Это декларативный синтаксис для утверждения истинности утверждения 2 + 2 = 4 на основе рефлексивности. Чтобы понять, почему это работает, давайте проверим тип:

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

rfl.{u} — это название функции и уровень её универсального множества (ваш слой типов в луковице). {α : Sort u} означает, что α — это тип на уровне универсального множества u, не имеющий ничего общего с «сортируемым», он просто относится к «сорту» u. {a : α} означает, что a — это терм типа α , и тип rfl в конечном итоге соответствует утверждению a = a . В нашем случае α — Nat , a — 4 , rfl имеет тип 4 = 4 , соответствующий типу Lean, нормализованному выше. Мы нашли обитателя для 2 + 2 = 4 доказывающего утверждение рефлексивностью.

Тактика

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

Это позволяет вам шаг за шагом строить доказательство, в то время как правая панель вашей IDE (InfoView) постепенно отображает ваши локальные предположения и вашу цель, отмеченную знаком ⊢ . Тактики представляют собой комбинацию макросов и синтаксического сахара, которые определяют состояние доказательства для ядра языка с проверкой типов. Они помогают вам мыслить аналитически и декларативно, решая ваши задачи. Это решение в императивном стиле внутри функционального языка, работающее внутри монады.

Вам придётся ознакомиться с тактикой, подобно тому как изучающий SQL знакомится с аналитическими конструкциями, такими как GROUP BY , PIVOT и LEFT JOIN . Удаление sorry отобразит состояние и цели в InfoView:

У нас одна цель — доказать. Coin и HotWater — это утверждения. Noodles — это неизвестное значение типа ?u.29 , случайный идентификатор для еще не назначенного уровня вселенной. Наша цель — представить доказательство (Coin → HotWater → Noodles) → Coin ∧ HotWater → Noodles .

Давайте воспользуемся intro приемом, чтобы ввести предположение в область видимости. Он автоматически определит тип входных данных (Coin → HotWater → Noodles) — одно из доказательств, которое у меня уже есть для работы:

Информационное окно обновится и отобразит обновленные локальные предположения и цель:

В дополнение к Coin , HotWater и Noodles , у нас теперь есть локальная гипотеза (или предположение): noodleVendingMachine , константа типа Coin → HotWater → Noodles (каррированная функция). Наша цель теперь — произвести Coin ∧ HotWater → Noodles .

Давайте введём ещё одну переменную, которая будет автоматически учитывать следующее предположение, типа Coin ∧ HotWater :

Теперь в InfoView отображается:

Теперь нам нужно лишь вернуть Noodles используя наш набор тактик и предположения о локальной области видимости. У нас есть каррированная функция noodleVendingMachine и тип продукта (кортеж) coinAndHotWater . Давайте применим Coin и HotWater из coinAndHotWater к noodleVendingMachine :

Тактика exact используется в качестве ключевого слова return, когда нам нужно вернуть точный тип. .left и .right — это элементы типа продукта / кортежа coinAndHotWater , которые мы применили к каррированной функции noodleVendingMachine . Помните, что пробелы — это применение функции.

В InfoView отображается:

Это можно записать в общем виде следующим образом:

Удовлетворение нашей исходной теоремы (P → Q → R) → (P ∧ Q → R) приведенной выше.

Некоторые тактики помогают разложить цель на более мелкие задачи, такие как intro , cases , constructor , apply или refine . Другие переписывают выражения, используя предположения об эквивалентности, например, rw или simp . Другие тактики нормализуют выражения с помощью вычислений или алгебраических преобразований, например, rfl и ring . А некоторые обеспечивают целевую автоматизацию: linearinth , omega , aesop . Обратитесь к справочнику тактик.

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

Общая концепция доказательств теорем

Лейбниц мечтал об универсальном формальном языке мышления (Characteristica universalis) в паре с механическим калькулятором (Calculus ratiocinator), который мог бы доказывать все теоремы и философские аргументы, вращая рукоятку. Гильберт спрашивал: «Возможно ли это?» — будучи до самой смерти убежден, что «нет ничего, чего бы мы не знали». Это считалось «главной проблемой математической логики» и «самой общей проблемой математики». Гёдель размышлял над этим и доказал, что некоторые истины нельзя доказать, в то время как Чёрч и Тьюринг независимо друг от друга доказали, что «часто вы будете вращать эту рукоятку вечно», возможно, положив начало области информатики. Используя шахматную аналогию, автоматическое доказательство теорем похоже на поиск выигрышных позиций в игровом дереве, но в математике доска бесконечна, поэтому поиск может никогда не закончиться — некоторые ходы «неразрешимы». Однако мы все еще можем проверить, является ли ход допустимым, и именно на этом этапе мы сейчас находимся с помощью систем автоматического доказательства.

В 1956 году Бертран Рассел написал письмо о программе Logic Theorist, которая автоматически доказывала теоремы из «Principia Mathematica» и которую иногда называют первой программой искусственного интеллекта:

«Жаль, что мы с Уайтхедом не знали об этой возможности раньше, чем потратили десять лет, делая это вручную. Я вполне готов поверить, что всё в дедуктивной логике можно сделать с помощью машин».

Заключение

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

Освоив основы, попробуйте перейти к более сложным темам с помощью книги «Математика в Lean», где вы будете решать задачи по дискретной математике, линейной алгебре, дифференциальному исчислению и топологии. Или же углубитесь в основы, начиная с нуля (буквально) с помощью пособия Тао по Lean к книге «Анализ I». Mathlib, библиотека для совместной работы в Lean, уже содержит 1,6 миллиона строк формализованной математики, которую вы можете использовать для связи со всеми разделами математики.

Ронен Лахат Посмотреть все от Ронен Лахат

Источник: towardsdatascience.com