Курс Стэнфордского университета CS221 предлагает глубокое погружение в методы построения современных систем искусственного интеллекта. В шестнадцатой лекции подробно разбирается логика первого порядка, которая устраняет ограничения пропозициональной логики и позволяет эффективно кодировать сложные взаимосвязи реального мира. Лектор наглядно демонстрирует принципы построения синтаксиса, семантики и механизмов логического вывода, необходимых для создания интеллектуальных агентов.
🧠 Ограничения пропозициональной логики и мотивация 0:06
Использование логики в задачах искусственного интеллекта позволяет построить структурированную базу знаний, на основе которой агент может делать обоснованные выводы. В пропозициональной логике элементарным кирпичиком является пропозициональный символ, выражающий простое утверждение (например, «Алиса — студентка» или «В Фениксе жарко»). Однако при попытке описать более сложные закономерности этот подход быстро демонстрирует свою неэффективность.
Проблема пропозиционального подхода заключается в отсутствии внутренней структуры у символов и невозможности компактного обобщения. Если необходимо выразить утверждение «Все студенты знают арифметику» для группы из тысячи человек, в пропозициональной логике придется составлять гигантскую формулу, перечисляющую импликации для каждого конкретного имени. Еще более очевидным этот провал становится при попытке закодировать математические проблемы, такие как проблема Гольдбаха, где для формулировки утверждения потребовалось бы бесконечное число пропозициональных символов.
Пропозициональная логика оказывается слишком громоздкой, поскольку в ней отсутствуют понятия объектов, предикатов и кванторов. Лектор сравнивает попытку писать базы знаний на пропозициональном языке с программированием без использования циклов for. Логика первого порядка (First-Order Logic, FOL) решает эту проблему, предлагая компактный и мощный инструмент для описания мира, аналогичный по своей выразительности конструкциям из языков программирования высокого уровня.
📝 Синтаксис логики первого порядка: термы и формулы 16:50
Синтаксис логики первого порядка разделяет понятия, которые обозначают объекты, и понятия, которые выражают истинность утверждений. В отличие от пропозициональной логики, где любые формулы оперируют только логическими значениями, в FOL вводится разделение на термы и формулы.
Термы служат для обозначения объектов окружающего мира. Выделяется три основных вида термов:
- Константные символы (например, конкретные объекты «Алиса» или «арифметика»), которые представляют собой абстрактные или физические сущности, но сами по себе не являются истинными или ложными.
- Переменные (такие как x, y, z), выступающие в роли заполнителей для объектов.
- Функции (например, «отец(x)» или «сложение(x, y)»), которые принимают один или несколько термов в качестве аргументов и возвращают новый терм (объект).
Формулы в логике первого порядка конструируются на основе предикатов, применяемых к термам. Предикат — это сущность, принимающая термы и возвращающая логическое значение (истину или ложь). Предикаты обладают определенной арностью (количеством аргументов): например, предикат «идет_снег» имеет арность 0, «студент(x)» — арность 1, а «знает(x, y)» — арность 2.
Сложные формулы строятся рекурсивно с помощью стандартных логических связок (и, или, отрицание, импликация) и кванторов существования или всеобщности, которые применяются к переменным внутри формул. В академической практике принято использовать строчные буквы для обозначения термов и прописные — для предикатов и формул.
🌐 Семантика логики первого порядка и индирекция 26:08
Определив правила построения синтаксических конструкций, необходимо задать правила их интерпретации. В пропозициональной логике моделью (или возможным миром) называлось простое присвоение истинностных значений атомарным символам. Прямой перенос этого принципа на логику первого порядка наталкивается на серьезные препятствия.
Если определять модель как присвоение истинности предикатам от термов, то из-за наличия функций (например, «отец(отец(Алисы))») мы получим бесконечное число атомарных формул. Кроме того, разные синтаксические термы могут ссылаться на один и тот же физический объект (например, «Боб» и «отец Алисы» могут быть одним лицом), и без введения явной структуры модель не сможет обеспечить логическую согласованность.
Для решения этой проблемы в семантику вводится слой индирекции — домен объектов и функция интерпретации. Домен представляет собой явное множество объектов реального или вымышленного мира. Функция интерпретации связывает синтаксические символы с элементами этого домена:
- Константы напрямую проецируются на конкретные объекты домена.
- Функции сопоставляются с правилами отображения одних объектов домена в другие.
- Предикаты интерпретируются как отношения между объектами домена, возвращающие истину или ложь для конкретных комбинаций элементов.
Визуально такую модель можно представить в виде семантического графа (Knowledge Graph), где узлами являются объекты домена, константы служат указателями на эти узлы, унарные предикаты выступают метками узлов, а бинарные предикаты — ребрами между ними. Вычисление истинности всей формулы происходит рекурсивно, при этом квантор всеобщности фактически разворачивается в итерационный цикл по всем объектам заданного домена.
⚙️ Логический вывод: от пропозиционализации до модус поненс 45:03
Процесс логического вывода позволяет отвечать на запросы к базе знаний или добавлять в нее новые непротиворечивые данные. В определенных узких сценариях задачу логического вывода в FOL можно свести к уже известным методам пропозициональной логики с помощью процедуры пропозиционализации.
Для успешной пропозиционализации необходимо принять два жестких допущения:
- Уникальность имен (Unique Names): каждый объект домена соответствует максимум одной константе.
- Замкнутость домена (Domain Closure): каждый объект домена имеет как минимум одну соответствующую константу.
При выполнении этих условий между объектами и константами устанавливается взаимно-однозначное соответствие. Тогда кванторы всеобщности можно заменить на конъюнкцию формул для всех констант, а кванторы существования — на дизъюнкцию. Полученная пропозициональная база знаний может быть проверена стандартными алгоритмами на удовлетворимость (SAT).
Однако в общем случае, особенно при наличии функций, пропозиционализация невозможна. Для вывода в FOL используются специализированные правила, работающие с определенными типами формул — определенными дизъюнктами (definite clauses). Это формулы вида «если А1 и А2 и ... и Ак, то В», где не допускается использование дизъюнкций (оператора «или»). К ним применяется фундаментальное правило вывода — Modus Ponens.
🔄 Унификация и подстановка как основа обобщенного правила 55:31
Поскольку формулы в логике первого порядка содержат переменные, стандартное правило Modus Ponens, требующее строгого строкового совпадения посылок, не может быть применено напрямую. Для преодоления синтаксического барьера используются механизмы подстановки и унификации.
Подстановка (substitution) — это рекурсивная операция «поиска и замены», заменяющая переменные в формуле на заданные термы. Унификация (unification) представляет собой обобщенное равенство: алгоритм пытается найти такую подстановку (унификатор), которая сделает два синтаксически разных выражения абсолютно идентичными. Например, выражение «знает(Алиса, y)» и «знает(x, z)» могут быть унифицированы с помощью подстановки, где x заменяется на Алису, а y приравнивается к z. Напротив, выражения с разными константами (например, «Алиса» и «Боб») унифицировать невозможно.
Обобщенное правило Modus Ponens сначала находит унификатор для посылок из базы знаний и левой части правила, а затем применяет этот унификатор к выводимому следствию. Сложность такого вывода без использования функций конечна и ограничена количеством констант в степени максимальной арности предикатов. Если же в правилах присутствуют функции, вывод может уйти в бесконечную генерацию новых термов (например, создание цепочки «отец(отец(x))» до бесконечности).
Лектор подчеркивает, что Modus Ponens в FOL обладает свойством корректности (soundness) — любые выведенные факты гарантированно истинны. Однако это правило не является полным (complete), так как с его помощью невозможно выводить утверждения, содержащие дизъюнкции. Для достижения полноты вывода требуется более сложный метод резолюций, который в рамках текущей лекции опускается.
🗣️ Перевод с естественного языка на логику первого порядка 1:07:11
Практическое применение FOL во многом зависит от умения корректно транслировать фразы естественного языка в строгие логические формулы. Процесс напоминает перевод неформального технического задания на язык программирования.
При переводе лектор рекомендует опираться на базовое эмпирическое правило, справедливое в 99% случаев:
- Квантор всеобщности практически всегда используется в связке с импликацией.
- Квантор существования практически всегда сочетается с конъюнкцией.
Нарушение этого правила приводит к грубым семантическим ошибкам. Например, если записать утверждение «Все студенты знают арифметику», используя конъюнкцию вместо импликации, формула будет утверждать, что абсолютно каждый объект во Вселенной является студентом и одновременно знает арифметику. Если же использовать импликацию с квантором существования, утверждение станет тривиально истинным, как только в домене обнаружится хотя бы один объект, не являющийся студентом.
Несмотря на свою колоссальную гибкость, логика первого порядка имеет свои границы выражения. Фразы вроде «70% студентов знают машинное обучение» невозможно адекватно закодировать средствами FOL. Для работы с долями, процентами и операциями над целыми множествами объектов требуется переход к логикам высших порядков, поддерживающим функции от функций и квантификацию по множествам.
