Logic Theorist

Герберт Саймон был политологом, занимавшимся изучением принятия решений в организациях; в этой области он выдвинул теорию, согласно которой основой информации служит «единица верования» — базовое положение, на основе которого человек или организация (компания, университет, госагентство) принимает решения. Эта идея легла в основу разработки Logic Theorist (L.T.). Весной 1952 года Саймон был приглашён RAND Corporation для участия в проекте по изучению систем противовоздушной обороны. Там он увидел устройство, моделирующее карты для авиации. Позже он вспоминал:^[2]

«Там у них было замечательное устройство для моделирования карт на старых табуляторах. Его использовали не только для печати статистики, но и для отображения карты. И тут стало ясно, что компьютер может не только считать числа, но и вообще вычислять координаты для вывода изображения — например, печатать картинки. И всё это делали не настоящие компьютеры, а простые картонные перфокарты»^[2].

Машина предназначалась для изучения взаимодействия человека и техники при моделировании центра ПВО. Аллен Ньюэлл, математик и исследователь RAND Corporation, занимался в то время логистикой и теорией организаций; именно он создал язык, применявшийся в эксперименте. Переломным моментом для Ньюэлла стала встреча на конференции с Оливером Селфриджем из Lincoln Laboratory, где были представлены успехи в области распознавания образов. Ньюэлл осознал, что сложные процессы могут моделироваться через множество простых условно активируемых подзадач, взаимодействующих друг с другом.

С лета 1955 года Ньюэлл и Саймон стали обсуждать возможность создания «мыслящей машины». Саймон сосредоточился на поиске задач и областей применения (логика, геометрия, шахматы), а Ньюэлл и Шоу, единственный системный инженер группы из RAND Corporation, занимались программированием. К 15 декабря того же года Саймон смог вручную смоделировать первую логическую проверку с использованием версии программы, вскоре получившей имя Logic Theorist.

В январе 1956 года состоялась первая полноценная симуляция:^[3]

«В январе 1956 года мы собрали мою жену, троих детей и несколько аспирантов. Каждому из них выдали карточку, превращая каждого в «компонент» компьютерной программы... Природа подражала искусству, которое подражает природе»^[3].

Из-за отсутствия языка программирования высокого уровня для выражения нужных концепций, были созданы собственные языки обработки информации — IPL-I и IPL-II. Как вспоминал Шоу:

«У программистов стояла творческая задача: придумать, какими средствами выразить на машине то, что мы легко описывали на английском. Логично было разработать более понятные, интерпретируемые языки высокого уровня, чтобы Аллен и Герберт могли задавать сложные концепты шахмат. Нужно было всё реализовать на машине, так мы создали языки обработки информации IPL-I и IPL-II. IPL — это название, которое мы дали задним числом языку, используемому Алленом и Гербертом для описания спецификации машины Logic Theorist»^[4].

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

К лету 1956 года программа была готова и представлена на первой научной конференции по искусственному интеллекту (ИИ), организованной Джоном Маккарти, Марвином Минским, Клодом Шенноном и Натаном Рочестером. На конференции обсуждались идеи и ранние приложения; Logic Theorist тогда уже был программой, способной рассуждать по-человечески. Однако работа Ньюэлла, Саймона и Шоу почти не получила внимания. Журналистка Памела Маккордак отмечала: «Похоже, никто, кроме самих Ньюэлла и Саймона, не увидел долгоиграющего значения их работы»^[5].

Вскоре Logic Theorist продемонстрировал доказательство 38 из 52 теорем главы II «Principia Mathematica»; причём теорема 2.85 решалась им эффективней, чем её автором — Расселом^[6]. Авторы направили статью с компьютерным доказательством в The Journal of Symbolic Logic, но её отклонили как не содержащую новых достижений для математики. Несмотря на это, сотрудничество продолжилось и привело к созданию General Problem Solver, архитектуры Soar, разработке общей теории мышления и основанию одной из первых лабораторий ИИ в Carnegie Tech.

Обработка списков

Для построения Logic Theorist не существовало машинных языков программирования, обеспечивающих высокоуровневые абстракции и эффективную работу с памятью, поэтому были созданы языки IPL; в них использовалась символьная обработка и повторное выделение блоков памяти. Это стало основой для семейства языков Lisp, широко используемых в будущем^[7][8].

Поиск в деревьях

Для поиска решения Logic Theorist применял процедуру, позднее получившую название «дерево решений»: в корне дерева — гипотеза, на каждом уровне — выводы из предыдущего, а на одной из ветвей — искомое математическое доказательство. Программа проходила по ветвям в поисках решения.

Эвристики

Построив дерево решений, авторы столкнулись с проблемой «взрыва ветвлений». Для их отсечения они реализовали в программе набор практических правил — эвристик, позволявших быстро отбрасывать заведомо бесперспективные ходы и ускорять поиск решения. Это был один из первых шагов в развитии области искусственного интеллекта — эвристических методов.

Цель Logic Theorist — доказательство истинности определённых логических выражений вида: −p → q ∨ −p, то есть вывод их в качестве теорем.

В отчёте для RAND (1956) авторы отмечали:

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

Язык

Переменные или атомарные выражения: p, q, r, A, B, C.
Связки: − (отрицание), ∨ (дизъюнкция), → (импликация).
Выражения: комбинации переменных и связок, например: −p → q ∨ −p

Утверждаемые выражения (теоремы)

p ∨ p → p
p → q ∨ p
p ∨ q → q ∨ p
p ∨ q ∨ r → q ∨ p ∨ r
p → q → r ∨ p → r ∨ q

Метод подстановки

1) Получить выражение (A), подлежащее доказательству;
2) Выбрать аксиому, через которую доказывается A; программа с помощью эвристик суужает выбор аксиом до тех, что схожи с A;
3) При совпадении — применить правила замены для попытки доказательства A; программа снова сокращает количество подстановок, используя эвристику сопоставления переменных аксиомы с A;
4) При успехе — завершить; неудачно — возврат к выбору другой аксиомы.

Метод отделения (modus ponendo ponens)

1) Получить выражение (A);
2) Выбрать правую часть аксиомы, через которую доказывается A; программа уменьшает выбор по схожести с A;
3) При совпадении — применить правила замены к правой части для попытки равенства с A;
4) Левую часть доказать методом подстановки;
5) Получить форму p → q, где p истинен, следовательно, q также истинен.

Метод цепочки (силлогизм)

1) Получить выражение p → q (A);
2) Найти аксиому B, имеющую форму r → c с правой частью, схожей с p;
3) Сопоставить r с p через замену, получив p → c;
4) Построить выражение c → q и доказать его методом подстановки;
5) Вывести из p → c и c → q требуемое p → q.

1) Получить выражение для доказательства.
2) Использовать метод подстановки — если успех, перейти к 6b;
3) Использовать метод отделения — если успех, к 6b;
4) Использовать метод цепочки — если успех, к 6b;
5) Применить правило подзадачи — если успех, к 6b;
6a) Сообщить, что выражение не доказано, завершить;
6b) Сообщить, что доказано, добавить в список аксиом и завершить.

Правило подзадач

Методы отделения и цепочки при неудаче метода подстановки заносят оставшийся недоказанный фрагмент (B) в список P. В шаге 5 берётся первая из списка P (A), удаляется из него и весь цикл повторяется для A; если A удаётся доказать, Logic Theorist утверждает истинность B и завершает по 6b.

Поскольку правило подзадач может приводить к бесконечному повторению, введены правила остановки:

Cписок P

Если при шаге 5 список P пуст, этот шаг пропускается, программа завершает по 6a.

Работа

Logic Theorist хранит число применений метода подстановки (W) и ограничение (WM). Если W достигло WM — завершение по 6a.

Обучение

Logic Theorist не изменяет собственные алгоритмы, но содержащиеся в доказательстве выражения заносит в список аксиом. После каждой итерации программа «обогащается» новым знанием для решения следующих задач^[9].