Код креативности. Как искусственный интеллект учится писать, рисовать и думать

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

Доказательство того, что для раскрашивания карты достаточно пяти красок, уже существовало, но никому не удавалось уменьшить это число до четырех. Затем, в 1976 году, два математика – Кеннет Аппель и Вольфганг Хакен – объявили, что нашли способ доказать, что четырех красок достаточно. У их доказательства была одна интересная особенность: они показали, что, хотя разных карт можно нарисовать бесконечное количество, можно показать, что все они могут быть сведены к анализу всего 1936 карт. Но проанализировать такое множество карт вручную было невозможно – или, точнее говоря, невозможно для человека. Аппель и Хакен сумели запрограммировать компьютер на перебор списка карт и проверку их соответствия правилам четырех красок. Неспешному компьютеру 1970-х годов понадобилось более 1000 часов работы, чтобы проанализировать все эти карты.

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

В 2006 году в журнале Annals of Mathematics было опубликовано полученное при помощи компьютера решение другой классической задачи геометрии – доказательство гипотезы Кеплера. Томас Хейлз, человек, стоявший за этим доказательством, разработал стратегию, позволяющую безоговорочно подтвердить, что шестиугольная стопка, в которую укладывают апельсины в овощной лавке, – самый эффективный вариант упаковки шаров. Ни одна другая конфигурация не занимает меньше места. Подобно Аппелю и Хакену, Хейлз использовал компьютер для анализа конечного, но огромного количества разных вариантов. В 1998 году он объявил о завершении доказательства и представил статью в Annals of Mathematics вместе с кодом программы, которую он использовал в компьютеризованной части работы над доказательством.