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

В конце 1980-х годов два французских математика, Жерар Пьер Юэ и Тьерри Кокан, начали работать над проектом под названием «Исчисление конструкций» (Calculus of Constructions, сокращенно CoC). Поскольку во Франции принято давать средствам для научно-технических разработок названия животных, эта система впоследствии стала называться Coq, что означает по-французски «петух». Это название удачно совпало с первыми тремя буквами фамилии одного из создателей системы. Система Coq была создана для проверки доказательств и вскоре стала любимым инструментом всех тех, кого интересует верификация доказательств, созданных компьютерами.

Жорж Гонтье, руководитель исследовательской программы в кембриджском отделении Microsoft Research, решил организовать группу для проверки доказательства теоремы о четырех красках – первого доказательства, для разработки которого потребовался компьютер, – при помощи Coq. К 2000 году эта группа проверила программный код, созданный Аппелем и Хакеном, и подтвердила правильность доказательства (в предположении, что в самой системе Coq нет своих собственных ошибок). После этого при помощи Coq начали проверять «человеческую» часть доказательства – те построения, которые написали сами Аппель и Хакен.

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

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

Почему же мы должны доверять программе Coq больше, чем исходному компьютерному доказательству? Ответ на этот вопрос, что интересно, связан с индукцией. По мере того как система Coq подтверждает все больше доказательств, в правильности которых мы уверены, мы все больше убеждаемся в том, что в ней самой нет ошибок. По сути дела, тут работает тот же принцип, который мы используем для проверки фундаментальных математических аксиом. Тот факт, что, какие бы числа А и В

мы ни взяли, результаты сложения А + + В и сложения В

+ А получаются одинаковыми, заставляет нас признать справедливость аксиомы, утверждающей, что А + В

= В + А. Используя одну и ту же программу для проверки всех остальных, мы можем доверять ее заключениям больше, чем если бы мы работали с какой бы то ни было специализированной программой, специально созданной для проверки данного конкретного доказательства.

Когда группа Гонтье закончила проверку теоремы о четырех красках, он поставил перед ней новую задачу – теорему о нечетном порядке[70]. Это одна из самых важных теорем, направляющих исследования симметрии. Ее доказательство привело к созданию классификации конечных простых групп, перечня основополагающих элементов, из которых можно построить все симметричные объекты. Один из самых простых элементов в этой периодической системе – правильные двумерные многоугольники с простым числом сторон, такие как треугольник или пятиугольник. Но существуют и гораздо более сложные и экзотические примеры симметрий, от 60 вращательных симметрий икосаэдра до симметрий странной снежинки в 196 883-мерном пространстве: число ее симметрий больше количества атомов, входящих в состав Земли.

Теорема о нечетном порядке утверждает, что для построения любого симметричного объекта с нечетным числом симметрий не требуются никакие экзотические симметрии. Он может быть составлен из простых элементов многоугольника, количество сторон которого равно простому числу. Эта теорема важна, потому что она исключает из рассмотрения половину возможных объектов. С этого момента мы можем предполагать, что объекты, которые мы пытаемся идентифицировать, обладают четным числом симметрий.