Стюарт Рассел - Совместимость. Как контролировать искусственный интеллект

Чтобы создание экспертной системы стало возможным, нужно ответить на два вопроса. Во-первых, как хранить знание в компьютере? Во-вторых, как добиться, чтобы компьютер правильно мыслил на основе этого знания, делая новые выводы? К счастью, древнегреческие философы, особенно Аристотель, дали базовые ответы на эти вопросы задолго до появления компьютеров. В действительности кажется вполне вероятным, что если бы Аристотель получил доступ к компьютеру (и электроэнергии, разумеется), то стал бы исследователем ИИ. Ответ Аристотеля, заново данный Маккарти, состоял в использовании формальной логики Бкак основы знания и рассуждения.

Для компьютерной науки по-настоящему важны два типа логики. Первая, так называемая пропозиционная , или Булева логика , была известна грекам, а также древнекитайским и индийским философам. Это тот же язык, что использует логические соединения «и», «нет» и т. д., составляющие структуру компьютерных чипов. В самом буквальном смысле современный микропроцессор — это просто очень большое математическое выражение, в сотни миллионов страниц, написанное на языке пропозиционной логики. Второй тип логики, тот, что Маккарти предложил для ИИ, называется {2} 2 В русскоязычной литературе используется название «узкое исчисление предикатов». — Прим. ред. логикой первого порядка Б. Язык логики первого порядка намного более выразителен, чем логики пропозиционной; это означает, что есть вещи, которые очень легко выразить в логике первого порядка, но чрезвычайно трудно или невозможно — в пропозиционной. Например, правила го занимают около страницы в логике первого порядка, но миллионы страниц в пропозиционной логике. Также легко выражается знание о шахматах, британском гражданстве, налогообложении, купле-продаже, движении, живописи, кулинарии и многих других сторонах нашего практического мира.

В принципе, способность мыслить в логике первого порядка позволяет нам далеко продвинуться на пути к универсальному интеллекту. В 1930 г. блестящий австрийский логик Курт Гёдель опубликовал знаменитую теорему о полноте [63] Оригинальная статья, описывающая теорему о полноте для логики первого порядка: Kurt Gödel, «Die Vollständigkeit der Axiome des logischen Funktionenkalküls», Monatshefte für Mathematik 37 (1930): 349–60. , доказывающую возможность существования алгоритма со следующим свойством [64] Алгоритм рассуждения в логике первого порядка тем не менее имеет недостаток: если ответа нет — то есть если доступного знания недостаточно, чтобы дать ответ, — то алгоритм может никогда не завершиться. Этого невозможно избежать: математически невозможно , чтобы верный алгоритм всегда прерывался, отвечая «я не знаю», в сущности, по той же причине, по которой ни один алгоритм не может решить проблему остановки. :

Для любого собрания знания и любого вопроса , выразимого в логике первого порядка, алгоритм даст нам ответ на этот вопрос, если тот существует.

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

Следует сказать, что Гёдель не предложил сам алгоритм — он только доказал его существование. В начале 1960-х гг. стали появляться реальные алгоритмы логического вывода [65] Первый алгоритм доказательства теорем в логике первого порядка, занимающийся сокращением предложений первого порядка до (очень многочисленных) пропозиционных предложений: Martin Davis and Hilary Putnam, «A computing procedure for quantification theory», Journal of the ACM 7 (1960): 201–15. Алгоритм разрешения Робинсона выполнял действия непосредственно над логическими предложениями первого порядка, используя «унификацию» для сопоставления комплексных выражений, содержащих логические переменные: J. Alan Robinson, «A machine-oriented logic based on the resolution principle», Journal of the ACM 12 (1965): 23–41. , и казалось, что мечта Маккарти об универсальных интеллектуальных системах на основе логики вот-вот сбудется. Первый в мире проект создания крупного мобильного робота, стэнфордский «Шеки», был основан на логическом рассуждении (см. рис. 4). Шеки получал цель от разработчиков-людей, с помощью алгоритмов визуализации создавал логические предположения, описывающие текущую ситуацию, выводил логическое умозаключение, чтобы построить план, гарантированно приводящий к цели, а затем выполнял этот план. Шеки был «живым» доказательством того, что аристотелевская концепция человеческого мыслительного процесса и действия по крайней мере частично верна.