Логик-теоретик

Логик-теоретик (англ. Logic Theorist, также Logic Machine) — одна из первых компьютерных программ, предназначенная для автоматического доказательства теорем из математической логики. Созданная в 1955—1956 годах, она считается первым проектом в области искусственного интеллекта (ИИ) и прототипом систем символьных вычислений. Программа была разработана Алленом Ньюэллом, Клиффом Шоу и Гербертом Саймоном и впервые продемонстрирована на практике способность компьютера к «интеллектуальному» поведению, отличному от простых арифметических расчётов.

История создания

Предпосылки и контекст

В середине 1950-х годов вычислительная техника в основном использовалась для численных расчётов — баллистических таблиц, метеопрогнозов, инженерных задач. Однако группа исследователей из корпорации RAND (США) и Университета Карнеги-Меллона (тогда — Технологический институт Карнеги) задалась вопросом: могут ли машины обрабатывать не только числа, но и символы, имитируя человеческое мышление? Ключевым вдохновением послужила книга Бертрана Рассела и Альфреда Норта Уайтхеда «Principia Mathematica» (1910—1913), в которой математические истины выводились из аксиом с помощью формальных правил.

Разработка

Аллен Ньюэлл, психолог по образованию, и Герберт Саймон, экономист и политолог, совместно с программистом Клиффом Шоу начали работу над «Логик-теоретиком» летом 1955 года. Программа писалась на языке ассемблера для компьютера JOHNNIAC, установленного в корпорации RAND. JOHNNIAC был ламповой машиной с памятью на магнитных барабанах и быстродействием около 1 000 операций в секунду.

Первая успешная демонстрация состоялась 15 августа 1956 года. Программа доказала первую теорему из «Principia Mathematica» — теорему 2.01 (¬p ∨ p) — за 52 минуты. Позднее Ньюэлл, Саймон и Шоу представили результаты на Дартмутской конференции по искусственному интеллекту (лето 1956 года), которая считается рождением ИИ как научной дисциплины.

Публикация и признание

В 1957 году вышла статья «Elements of a Theory of Human Problem Solving» (Ньюэлл, Саймон, Шоу), где «Логик-теоретик» описывался как модель человеческого мышления. В 1963 году программа была переписана для компьютера IBM 7090 и получила название «General Problem Solver» (GPS) — более общую систему для решения задач.

Принцип работы

Представление знаний

«Логик-теоретик» оперировал символическими выражениями, записанными в виде формул логики высказываний. Исходными данными служили аксиомы из «Principia Mathematica» (например, аксиома 1.1: (p ∨ p) → p). Целью было доказать заданную теорему, применяя к аксиомам и уже доказанным утверждениям разрешённые правила вывода: подстановку, замену и модус поненс.

Алгоритм поиска

Программа использовала эвристический поиск в пространстве состояний. В отличие от полного перебора всех возможных выводов (что было бы непрактично из-за комбинаторного взрыва), «Логик-теоретик» применял набор эвристик, основанных на сходстве целевой формулы с текущим выражением. Основные стратегии:

• Метод подцелей: если прямое доказательство невозможно, программа разбивала задачу на подзадачи, пытаясь свести их к известным аксиомам.
• Правило подстановки: замена переменных на конкретные выражения.
• Правило замены: замена подформулы на эквивалентную (с использованием законов логики, например, закона двойного отрицания).
• Модус поненс: если доказано A и A → B, то B считается доказанным.

Ограничения

Программа не могла оперировать кванторами (∀, ∃) и работала только с пропозициональной логикой. Она не «понимала» смысла теорем, а лишь механически применяла правила. Тем не менее, для своего времени это был прорыв: «Логик-теоретик» доказал 38 из первых 52 теорем «Principia Mathematica», а для некоторых нашёл более короткие доказательства, чем у Рассела и Уайтхеда.

Классификация и место в истории ИИ

Отличие от других ранних программ

• 1951 — Ferranti Mark I (Кристофер Стрейчи): программа для игры в шашки, но без обучения и символьных преобразований.
• 1952 — IBM 701 (Артур Сэмюэл): программа для игры в шашки, обучающаяся на основе оценок позиций.
• 1956 — «Логик-теоретик»: первая программа, которая манипулировала абстрактными символами, а не числами или игровыми досками.

Влияние на последующие проекты

«Логик-теоретик» стал предшественником:

• General Problem Solver (GPS) (1957) — более универсальной системы, использующей анализ средств и целей.
• STRIPS (1971) — системы планирования для роботов.
• Современных систем автоматического доказательства теорем (например, Coq, Isabelle, Prover9).

Применение и значение

Научное значение

1. Демонстрация «интеллекта»: программа показала, что компьютер может решать задачи, традиционно считавшиеся прерогативой человека (доказательство теорем).
2. Модель когнитивных процессов: Ньюэлл и Саймон использовали «Логик-теоретик» для проверки гипотез о том, как люди решают логические задачи. Они утверждали, что программа имитирует стратегии мышления человека (например, разбиение на подзадачи).
3. Эвристическое программирование: впервые был применён подход, при котором программа не следует жёсткому алгоритму, а использует эвристики для сокращения перебора.

Практическое применение

В чистом виде «Логик-теоретик» не использовался в промышленности или науке за пределами исследовательских лабораторий. Однако его идеи легли в основу:

• Систем проверки корректности программ (например, статический анализ кода).
• Экспертных систем 1970-х годов (MYCIN, DENDRAL).
• Современных алгоритмов символьного вывода в математических пакетах (Mathematica, Maple).

Критика и ограничения

Критика со стороны математиков

Некоторые математики (например, Пол Халмош) скептически относились к идее автоматического доказательства теорем, утверждая, что творческий процесс в математике не сводится к перебору правил. «Логик-теоретик» доказал лишь простейшие теоремы, не затрагивая глубокие результаты.

Технические ограничения

• Ограниченная мощность: память JOHNNIAC (около 4 000 слов) не позволяла обрабатывать длинные цепочки выводов.
• Отсутствие обучения: программа не улучшала свои результаты с опытом.
• Зависимость от аксиом: все доказательства были привязаны к конкретному формализму «Principia Mathematica».

Философские споры

В 1960-е годы вокруг «Логик-теоретика» развернулась дискуссия: можно ли считать его «думающим»? В ответ на критику (например, тест Тьюринга) Ньюэлл и Саймон утверждали, что программа демонстрирует «интеллектуальное поведение» в узком смысле — способность решать задачи, требующие символьных преобразований.

Интересные факты

• Первое «изобретение» ИИ: «Логик-теоретик» нашёл более элегантное доказательство теоремы 2.85 (p ∨ (q ∨ r) → (p ∨ q) ∨ r), чем в «Principia Mathematica». Это считается первым случаем, когда компьютер «открыл» новое знание.
• Награда: в 1975 году Ньюэлл и Саймон получили премию Тьюринга (высшую награду в области информатики) за вклад в искусственный интеллект, включая создание «Логик-теоретика».
• Сохранность: исходный код программы на перфокартах не сохранился, но её реконструкция была выполнена в 2000-х годах для эмулятора JOHNNIAC.
• Параллель с шахматами: в том же 1956 году Алан Тьюринг написал программу для игры в шахматы (но не реализовал её на компьютере), что также стало вехой в ИИ.

Источники

• Newell, A., Shaw, J. C., & Simon, H. A. (1957). «Elements of a Theory of Human Problem Solving». Psychological Review, 65(3), 151-166.
• Russell, S., & Norvig, P. (2020). Artificial Intelligence: A Modern Approach (4th ed.). Pearson.
• Crevier, D. (1993). AI: The Tumultuous History of the Search for Artificial Intelligence. Basic Books.
• McCorduck, P. (2004). Machines Who Think (2nd ed.). A. K. Peters.
• Документация проекта RAND Corporation: «The Logic Theorist: A Case Study in the History of AI» (1956).