Общий искусственный интеллект - страница 7

Шрифт
Интервал


Однако математика включает и другие когнитивные задачи, не только вычисления. Математики ведь не проводят все время за расчетами. Они развивают математику как науку. То есть доказывают теоремы и, что еще важнее, размышляют над тем, какие теоремы нужно доказывать и какими методами, чтобы создавать полезные и красивые математические концепции. Если признать, что развитие математики требует интеллекта, то система, способная доказывать теоремы на уровне человека, должна считаться искусственным интеллектом, а если она делает это лучше человека, то ИИ, превосходящим человека.

В 1956 году Аллен Ньюэлл и Герберт Саймон решили проверить, способен ли компьютер доказывать математические теоремы. Цифровых компьютеров тогда было совсем немного, и каждый занимал целую комнату. Они сосредоточились на доказательствах в области оснований математики, выбрав знаменитую книгу начала XX века «Основания математики», которая стремилась свести математику к чистой логике.[7] Созданная ими программа Logic Theorist должна была заново вывести теоремы из «Оснований математики».[8] По своей сути Logic Theorist представляла собой поисковый алгоритм, автоматически переписывающий доказательства согласно известным правилам преобразования уравнений, часть которых изучается еще в школе. Программа начинала с набора аксиом и последовательно преобразовывала их, пока не достигала намеченного доказательства. Существует колоссальное количество способов переписать эти аксиомы, но лишь немногие из них представляют ценность. Поэтому в Logic Theorist были заложены определенные правила и эвристики, имитирующие человеческий подход к поиску значимых способов переформулирования теорем. С помощью этих эвристик программа смогла самостоятельно вывести тридцать восемь из первых пятидесяти двух теорем «Оснований математики». Для своего времени это было выдающееся достижение, особенно если учесть, что таким блестящим математикам, как Бертран Рассел и Альфред Норт Уайтхед, потребовались долгие годы, чтобы изначально сформулировать эти теоремы.

Logic Theorist можно считать ИИ, превосходящим человека, поскольку он воспроизвел теоремы в тысячи раз быстрее Рассела и Уайтхеда, иногда предлагая даже более подробные доказательства. Однако его превосходство ограничивается крайне узкой областью – фактически только «Основаниями математики». Для доказательства теорем из других областей математики программе потребовались бы новые аксиомы и, скорее всего, новые эвристические правила.