ИИ. История машины, которая научилась говорить

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

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

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

Ньюэлл и Саймон хотели понять, чем эффективный поиск отличается от слепого перечисления. Здесь и появляются эвристики — правила выбора, которые помогают оценить, какие варианты стоит рассмотреть первыми. Греческое слово «эвристика» связано с нахождением, но в компьютерной программе эвристика не волшебная подсказка и не доказательство правильности маршрута. Это практическая стратегия: она повышает шанс быстро продвинуться, но может увести не туда или пропустить решение.

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

Для Logic Theorist это имело и психологическое значение. Исследователи связывали эвристический поиск со стратегиями решения задач у людей. Математик не применяет все возможные правила к каждой формуле: он замечает знакомые связи, выделяет подцели и сводит неизвестное к уже известному. Команда хотела описать такие приёмы настолько точно, чтобы выполнить их на компьютере и сравнить поведение программы с человеческими решениями.

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

Однако сходство на уровне общей стратегии ещё не устанавливает, что программа и человек думают одинаково. Если оба используют частичные цели, это не значит, что у них одни и те же внутренние переживания или знания. Чтобы модель была полезна, нужно указывать, какие именно действия она объясняет и какие наблюдения могли бы её опровергнуть. Logic Theorist давала исследователям объект для такого анализа: последовательность формальных шагов можно было сохранить, изучить и сопоставить с человеческими решениями.

В этом проекте эвристика стала признанием двух ограничений одновременно. Во-первых, пространство поиска слишком велико для механического перебора. Во-вторых, у исследователя нет универсального способа заранее знать, какой ход приведёт к успеху. Эвристика сокращает пространство за счёт предположений. Она делает поиск осуществимым и одновременно открывает дверь для ошибок. Скорость и риск здесь не противоположны: они рождаются из одного решения — не проверять всё.

Как выглядит один доказанный результат

Чтобы понять работу Logic Theorist, полезно отойти от больших слов и рассмотреть пример из публикации команды 1957 года. Исследователи просили программу доказать формулу, записанную как теорема 2.01 в соответствующем наборе из Principia Mathematica. Затем они показывали несколько шагов, в которых используются аксиома, подстановка и замена логических связок.

Правило подстановки позволяет заменить переменную в формуле другим выражением, соблюдая условие, что замена выполняется последовательно везде, где переменная встречается. Если исходная формула говорит о p, можно вместо p подставить составное выражение вроде «q или r» и получить другой экземпляр той же схемы. Правило замены позволяет переписать связку через её определение: например, импликация «если p, то q» выражается через отрицание и «или». Правило отделения, или modus ponens, говорит: если уже доказано p и доказано «если p, то q», можно заключить q.

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

В примере с теоремой 2.01 машина брала одну из аксиом, подставляла вместо переменной нужный символ, переписывала связку и применяла правило отделения. В отчёте говорится, что этот небольшой вывод был получен примерно за десять секунд вычислительного времени. Цифра зависит от конкретного запуска и машины того времени; её смысл не в сравнении скорости с современным процессором. Она показывает, что после задания аксиом и правил программа сама выдала цепочку, которую можно сверить.

Пример важен также потому, что демонстрирует разницу между проверкой и поиском. Когда читатель видит готовую последовательность, каждый шаг кажется почти очевидным. Но машине нужно было решить, какую аксиому взять, какую замену попробовать и когда применять правило. В отчёте печатается результат, но работа программы заключалась не в переписывании уже предложенного человеком решения. Она порождала варианты и оценивала их по процедуре поиска.

Более сложный пример показывает, как ситуация меняется с глубиной. В публикации авторы описывали, как Logic Theorist доказала теорему 2.45 примерно за двенадцать минут, используя набор из 38 ранее полученных результатов, доступных к этому моменту. Здесь поиск уже зависел не только от нескольких исходных аксиом: накопленный запас теорем расширял возможности программы. Каждое ранее доказанное утверждение становилось новым инструментом, хотя использование большого набора также усложняло выбор.

Есть и более важная деталь: машина не всегда находила доказательство. Для теоремы 2.31, приведённой в том же исследовании, программа работала около 23 минут, а затем сообщала, что исчерпала доступный ей поиск и не смогла доказать утверждение. Это не было доказательством того, что теорема неверна или что доказательства не существует. Это означало только, что данная процедура, с данным управлением поиска и при доступных ресурсах, не нашла путь.

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

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

Британский музей и цена полного перебора

В статье 1957 года Ньюэлл, Шоу и Саймон предложили мысленный эксперимент, чтобы показать, почему доказательства нельзя искать простым перечислением. Они назвали его «алгоритмом Британского музея»: представьте, что все возможные последовательности логических выражений уже где-то собраны, а задача состоит в том, чтобы найти среди них цепочку, заканчивающуюся нужной теоремой и соответствующую правилам доказательства.

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

Это различие многое объясняет в истории Logic Theorist. Проверить готовую цепочку можно сравнительно механически: убедиться, что начальные строки относятся к аксиомам или прежним теоремам, а остальные получены допустимыми переходами. Труднее придумать генератор, который не тратит всё время на бесполезные последовательности. Программа должна была производить варианты и фильтровать их, но её эвристики отвечали за то, какие из них появятся раньше и какие подцели будут поставлены. В такой схеме корректность доказательства и эффективность поиска — разные качества. Система могла быть совершенно надёжной в проверке и всё же долго не находить решение.

Когда авторы сравнивали подходы, они потому обсуждали не только число теорем, но и стоимость пути к ним. Можно гарантировать, что решение рано или поздно появится, и одновременно получить такой счёт вычислительного времени, при котором гарантия теряет практический смысл. Можно искать выборочно и решить задачу быстро, рискуя пропустить доказательство. Эта рамка — кандидат, проверка и цена поиска — помогала обсуждать поведение программы точнее, чем слово «умная».Такой алгоритм был бы надёжен в принципе: он перебирал бы варианты один за другим, проверял бы каждый и когда-нибудь нашёл бы доказательство, если оно существует. Но скорость делала гарантию пустой для практики. Авторы оценивали, что один из более сложных примеров мог занять при таком переборе тысячи лет вычисления, а расширение поиска на весь набор задач Principia Mathematica требовало бы колоссального времени. Это были грубые оценки по тогдашним методам и машинам, а не измерение современной вычислительной сложности, но мысль ясна: возможность перечислить всё ещё не означает, что ответ будет найден вовремя.

Для сравнения они предложили простую задачу — открыть кодовый замок. Можно перебирать все комбинации, проверяя каждую, пока замок не откроется. Если код конечен и комбинации исчерпываются, метод гарантирует успех. Но если комбинаций очень много, охранять ценности при помощи замка с таким кодом всё ещё имеет смысл: знать принцип перебора — не то же самое, что успеть его завершить. Этот пример не был описанием самой Logic Theorist. Он показывал разницу между алгоритмом, гарантирующим ответ, и эвристикой, которая может найти ответ быстрее, но не обещает, что справится во всех случаях.

Команда не считала, что эвристика автоматически лучше. Для некоторых задач надёжный алгоритм — правильный выбор, даже если он требует времени. Но когда полный поиск непосилен, приходится принимать риск: программа может не найти решение, хотя оно существует. Работа становится похожа на повседневное решение задач: ограниченный исследователь выбирает, какой вариант кажется более перспективным, и не может одновременно проверить всё.

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

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

Четыре способа искать дорогу к теореме

Logic Theorist не была одной универсальной догадкой. В описании 1957 года авторы разбирали несколько методов, которые могли по-разному сократить поиск. Для широкой аудитории важнее понять их логику, чем запомнить названия.

Первый путь — подстановка. Если аксиома задаёт общую схему, в неё можно подставлять конкретные выражения и получать новые утверждения. Это похоже на шаблон договора: сам бланк общий, но когда на места переменных вписывают имена и условия, появляется конкретный экземпляр. Подстановка не означает произвольной замены любого символа. Нужно соблюдать структуру формулы, чтобы вывод оставался корректным. Такой способ способен сразу производить новые теоремы, но число возможных подстановок быстро растёт.

Второй путь — отделение. Если известны утверждение A и условная формула «если A, то B», можно вывести B. Это знакомое рассуждение: если поезд отправится в 10:00, он успеет к пересадке; поезд отправится в 10:00; значит, пересадка возможна. В формальной системе примеры выражаются символами, но логическая связь та же. При поиске доказательства программа могла рассмотреть цель B и искать такое уже известное утверждение, которое говорит «A влечёт B». Тогда A превращается в подцель: сначала надо доказать её, чтобы получить B.

Третий и четвёртый методы в статье — цепочки вперёд и назад по импликациям. Если задача требует доказать, что A влечёт C, можно искать промежуточное утверждение B: найти уже известное «A влечёт B», а затем проверить, можно ли показать «B влечёт C». Или двигаться с другого конца: искать «B влечёт C» и сводить задачу к «A влечёт B». Такие переходы напоминают сбор моста с обоих берегов. Когда встречные участки соединяются, появляется доказательство. Если выбранные опоры не совпадают, приходится искать другую промежуточную точку.

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

Здесь особенно заметно различие между поисковым механизмом и критерием проверки. Механизм предлагает кандидатов; проверка определяет, допустим ли переход и достигнута ли цель. Можно менять очередность, стратегии и эвристики, не меняя математические правила корректности. Если программа нашла доказательство, оно не становилось правильным лишь потому, что эвристика считала путь перспективным. Каждое звено всё равно должно было пройти проверку.

Эти методы дают и более точное объяснение фразы «программа рассуждала». Logic Theorist не получала от человека готовое доказательство, которое лишь оформляла. Она строила варианты на основе формальных операций и пыталась связать цель с аксиомами и известными теоремами. Но пространство вариантов, правила перехода и сама цель были заданы заранее людьми. Программа самостоятельно выбирала следующий вычислительный шаг внутри созданной исследователями рамки. Именно это, а не таинственное появление мысли, было содержанием демонстрации.

Когда компьютер пропускает решение, а находит другое

Самым памятным эпизодом Logic Theorist часто называют теорему 2.85. По рассказам участников и последующим историческим исследованиям, программа построила доказательство, которое заметно отличалось от опубликованного в Principia Mathematica и оказалось короче или проще по структуре. Точность пересказа здесь важна: не нужно говорить, будто машина «обнаружила ошибку» в фундаментальной книге или превзошла человеческий разум вообще. Она нашла другую формально допустимую цепочку для конкретного результата в заданной системе.

Особенность состояла в том, что программу не писали специально ради создания более красивых доказательств. Исследователи задавали ей правила поиска, а не эстетический критерий «сделай элегантнее, чем Рассел». Новая цепочка появилась как побочный результат процедуры, которую строили для поиска доказательств и исследования эвристик. Иногда нужный эффект возникает без того, чтобы кто-то отдельно программировал его как цель. Программа не имела вкуса к краткости; она исследовала маршруты, и один из них оказался компактнее известного.

Этот результат помогает отделить механическую корректность от человеческой оценки качества. Корректность можно формализовать: каждый переход разрешён. Краткость тоже можно измерить, например числом шагов. А вот «элегантность» включает суждение математиков о том, почему доказательство хорошо устроено и что оно проясняет. Работа программы не отменяла человеческую оценку, но заставляла её обратить внимание на результат, которого раньше не было в привычном наборе решений.

Герберт Саймон отправил Бертрану Расселу описание работы. Рассел ответил письмом от 2 ноября 1956 года, что рад узнать: Principia Mathematica теперь можно выполнять с помощью машины, и готов поверить, что дедуктивную логику в принципе можно поручить механизации. Для Рассела это был не просто любопытный трюк с компьютером. Он десятилетиями работал над формальными основаниями математики, и теперь один из методов, описанных в книге, исполнялся машиной.

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

Для публики и профессионального сообщества это был эффектный сюжет. Машина не просто повторила арифметическое вычисление быстрее человека. Она нашла символический путь от аксиом к теореме. Но самый ценный итог был не в соревновании «кто умнее». Программа показывала, что компьютер способен участвовать в работе с формальными доказательствами, а исследователь может изучать эту работу как последовательность операций. Возможность доказать теорему становилась наблюдаемым экспериментом.

Результат относится к поиску в ограниченной формальной системе. Logic Theorist могла найти путь, который разработчики заранее не записали как ответ, — значимое свойство программы. Это показывает, что процедура способна производить новый и проверяемый результат, полезный людям. Оценка красоты, неожиданности и математической важности по-прежнему оставалась за человеком.

Программа была и моделью человеческого решения

Для Ньюэлла и Саймона Logic Theorist была не только автоматическим доказателем. Они рассматривали её как модель сложной обработки информации: система получает задачу, хранит представление о ней, выбирает операцию, оценивает результат и продолжает поиск. Если человеческое решение задач состоит хотя бы частично из таких операций, их можно попытаться формализовать и проверить на машине.

Такой взгляд отличался от идеи, что психологию следует изучать только по внешней реакции человека. Команда хотела говорить о процессах между условием и ответом: какие подцели человек строит, какие ходы рассматривает, как замечает знакомую структуру. Компьютер помогал сделать эти гипотезы явными. Вместо фразы «человек каким-то образом нашёл решение» исследователь мог записать предполагаемую процедуру, реализовать её и посмотреть, выдаёт ли она ответы в наблюдаемых условиях.

Здесь легко запутаться в значении слова «модель». Модель может быть похожа на объект в одном отношении и сильно отличаться в остальных. Карта метро точно показывает связи между станциями, но не передаёт длину туннелей или запах платформы. Logic Theorist могла моделировать поиск по подзадачам и использование эвристик, не моделируя человеческие чувства, биографическую память или опыт математического образования. Для научной модели это нормально, если исследователи ясно называют, какую часть поведения она объясняет.

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

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

Это сравнение не предполагало, что компьютер — эталон, а человек — несовершенная копия. Иногда программа успешно решала формальную задачу, но использовала стратегию, которую люди не применяли. Иногда человеческие участники находили способы, отсутствовавшие в программе. Такие различия были исследовательским материалом: они показывали, какие части модели согласуются с наблюдениями, а какие требуют пересмотра.

Здесь находится один из важных результатов Logic Theorist, который легко потерять за рекордом «первая программа доказала теорему». Компьютер дал способ проверять теории о мышлении с помощью работающих систем. Программа стала не только инструментом для решения задач, но и лабораторным объектом, чьё поведение можно было менять, сравнивать и объяснять. Для психологии и ранней когнитивной науки это был новый тип эксперимента.

Но модель и человек оставались разными вещами. У программы были правила, структуры данных и вычислительное время; у человека — тело, опыт и сложная способность ориентироваться в ситуации. Даже если некоторый ход поиска совпадал, это не доказывало совпадение внутреннего мира. Logic Theorist показала, что имитация определённой деятельности может быть научно полезной без заявления, будто машина приобрела сознание.

Что именно показали 38 доказательств

Позднейшие краткие истории часто сводят успех Logic Theorist к одной цифре: программа доказала 38 из первых 52 теорем, предъявленных ей из второй главы Principia Mathematica. Эта цифра опирается на исторические свидетельства и стала удобным способом передать масштаб результата. Но без пояснения она звучит так, будто машине дали произвольную книгу, а она прочитала и поняла её. В действительности человеческая подготовка была значительной.

Исследователи выбрали формальную систему, задали символическое представление, подготовили аксиомы и правила вывода, формализовали теоремы и написали процедуры поиска. Человек определил, какие фрагменты книги окажутся входными данными и что будет считаться корректным доказательством. Программа не сама выбрала Principia Mathematica в библиотеке, не извлекла из страниц математическую структуру и не сформулировала вопрос, который надо исследовать.

Это не обесценивает результат. Научные инструменты обычно требуют, чтобы люди подготовили эксперимент. Телескоп не выбирает астрономическую гипотезу; микроскоп не решает, какие клетки сравнивать. Важен точный вклад системы в процедуру: после того как цель и формальные правила были заданы, Logic Theorist искала цепочки, а не просто воспроизводила заранее введённые доказательства. Проверяемый шаг за пределами ручной подготовки и был центральной демонстрацией.