С момента создания Logic Theorist в 1950-х годах был достигнут значительный прогресс. За 65 лет исследований в области автоматического доказательства теорем – подразделе искусственного интеллекта – были созданы впечатляющие системы ИИ, способные предлагать как новые теоремы, так и оригинальные доказательства уже известных теорем. Тем не менее математика остается делом математиков-людей: все статьи о последних достижениях в математических журналах написаны людьми. Правда, современные математики часто пользуются такими программами, как Mathematica, вобравшей в себя многие достижения автоматического доказательства теорем. В своей работе они также могут применять большие языковые модели типа GPT-4.
Любопытно, что Герберт Саймон, один из создателей Logic Theorist, утверждал, что они с Ньюэллом создали «мыслящую машину» и «решили проблему „сознание-тело“ (mind-body problem), показав, как материальная система может обладать свойствами сознания». С сегодняшней точки зрения это звучит как явное преувеличение – ведь их программа могла только доказывать теоремы из «Оснований математики». Она не могла работать даже с дифференциальными уравнениями, не говоря уже о том, чтобы сочинять сонеты, рисовать или завязывать воображаемые шнурки. Но программа, безусловно, стала важным достижением, и понятно, почему в то время было сложно увидеть ее ограничения. В конце концов, разве мышление не похоже на доказательство теорем?
Что еще, кроме доказательства математических теорем, требует от человека интеллекта? Может быть, игры? За всю историю исследований искусственного интеллекта именно игры стали одним из важнейших направлений, позволивших получить впечатляющие результаты.
Пожалуй, ни одна другая игра не сыграла такой важной роли в исследованиях ИИ, как шахматы. Это неудивительно – западная культура всегда считала эту классическую настольную игру воплощением интеллекта. Со времен Средневековья шахматы считались интеллектуальной игрой для дворян, студентов и священнослужителей. Даже в скандинавской мифологии всевидящий Один играл в игру, похожую на шахматы. И действительно, хорошая игра в шахматы требует сложного мышления. Чтобы победить серьезного противника, нужно разработать сложный многоходовый план и уметь видеть угрозы и возможности в ходах соперника. По сути, нужно превзойти противника в интеллектуальном плане. Логично предположить: если кто-то или что-то умеет играть в шахматы, значит, он обладает интеллектом. Поэтому неудивительно, что первые исследователи ИИ были одержимы созданием шахматного ИИ.
Как компьютер играет в шахматы? В основе большинства шахматных ИИ лежит алгоритм минимакс. Он моделирует все возможные ходы белых (если играет