Код креативности. Как искусственный интеллект учится писать, рисовать и думать
- Автор: дю Сотой Маркус
- Год: 2020
- Язык: русский
- Год: Аттикус
- ISBN: 978-5-389-18965-2
- Переводчик: Дмитрий Александрович Прокофьев
- Жанр: Зарубежная образовательная литература
Электронная книга - «Код креативности. Как искусственный интеллект учится писать, рисовать и думать». Краткое содержание книги:
«Искусственный интеллект потрясает самые основы нашего существования, демонстрируя, сколь многое из того, чем занимаются люди, машины могут делать не хуже, а то и лучше их. Но эта книга посвящена не столько будущему с беспилотными машинами и компьютеризованной медициной, сколько вопросу о том, смогут ли алгоритмы состязаться сколько-нибудь существенным образом с могуществом человеческого кода. Способны ли компьютеры к творчеству? Что нужно для творчества? В какой степени эмоциональная реакция на произведения искусства является результатом реакции мозга на определенные рисунки и структуры? Таковы некоторые из тем, которые мы рассмотрим». (Маркус дю Сотой)
В формате PDF A4 сохранен издательский макет книги.
Почему же мы должны доверять программе Coq больше, чем исходному компьютерному доказательству? Ответ на этот вопрос, что интересно, связан с индукцией. По мере того как система Coq подтверждает все больше доказательств, в правильности которых мы уверены, мы все больше убеждаемся в том, что в ней самой нет ошибок. По сути дела, тут работает тот же принцип, который мы используем для проверки фундаментальных математических аксиом. Тот факт, что, какие бы числа А и В мы ни взяли, результаты сложения А + + В и сложения В + А получаются одинаковыми, заставляет нас признать справедливость аксиомы, утверждающей, что А + В = В + А. Используя одну и ту же программу для проверки всех остальных, мы можем доверять ее заключениям больше, чем если бы мы работали с какой бы то ни было специализированной программой, специально созданной для проверки данного конкретного доказательства.
Когда группа Гонтье закончила проверку теоремы о четырех красках, он поставил перед ней новую задачу – теорему о нечетном порядке[70]. Это одна из самых важных теорем, направляющих исследования симметрии. Ее доказательство привело к созданию классификации конечных простых групп, перечня основополагающих элементов, из которых можно построить все симметричные объекты. Один из самых простых элементов в этой периодической системе – правильные двумерные многоугольники с простым числом сторон, такие как треугольник или пятиугольник. Но существуют и гораздо более сложные и экзотические примеры симметрий, от 60 вращательных симметрий икосаэдра до симметрий странной снежинки в 196 883-мерном пространстве: число ее симметрий больше количества атомов, входящих в состав Земли.
Теорема о нечетном порядке утверждает, что для построения любого симметричного объекта с нечетным числом симметрий не требуются никакие экзотические симметрии. Он может быть составлен из простых элементов многоугольника, количество сторон которого равно простому числу. Эта теорема важна, потому что она исключает из рассмотрения половину возможных объектов. С этого момента мы можем предполагать, что объекты, которые мы пытаемся идентифицировать, обладают четным числом симметрий.
Доказательство этой теоремы было довольно устрашающим. В нем было 255 страниц, и его публикация заняла целый выпуск журнала Pacific Journal of Math. До его появления доказательства по большей части занимали не более нескольких страниц, и в них можно было разобраться за день. Это же доказательство было таким длинным и сложным, что понять его было непростой задачей для любого математика. Учитывая его размеры, нельзя было не заподозрить, что где-то среди его многочисленных страниц может таиться какая-нибудь малозаметная ошибка.
Поэтому проверка этого доказательства при помощи Coq не только продемонстрировала бы мастерство этой системы: она укрепила бы нашу уверенность в справедливости доказательства одной из самых сложных теорем в математике. Это была достойная цель. Но преобразование доказательства, созданного человеком, в проверяемый код делало эту задачу еще более грандиозной. Гонтье предстояла нелегкая работа.
Он смущенно вспоминал:
Когда мы собрались и я впервые обнародовал свой великий план, группа сначала решила, что у меня мания величия. Но настоящей целью проекта было разобраться с доказательством, которое на момент начала этой работы явно считалось недосягаемым, понять, как создавать все эти теории, как добиваться их соответствия друг другу и как убеждаться в правильности всего этого.
После совещания один из программистов просмотрел доказательство. О своих впечатлениях он написал Гонтье по электронной почте: «Число строк – 170 000. Число определений – 15 000. Число теорем – 4300. Развлечений – масса!» Группа из кембриджского отделения Microsoft Research потратила на работу над этим доказательством шесть лет. Гонтье рассказывал о том восторге, который он ощущал по мере приближения проекта к завершению. Наконец, после множества бессонных ночей, он мог успокоиться.
«Математика – одна из последних великих романтических дисциплин, – сказал он, – в которой одному гению, по сути дела, приходится держать в голове и понимать сразу всё». Но аппаратное обеспечение человека подходит к пределу своих возможностей. Гонтье надеется, что его работа положит начало эпохе большего доверия и устойчивого сотрудничества между человеком и машиной.
Среди молодых математиков сейчас растет ощущение, что многие области математического мира становятся настолько дремучими и сложными, что все три года аспирантуры можно потратить только на то, чтобы понять ту задачу, которую поставил тебе научный руководитель. Можно работать долгие годы, осваивая эту территорию и отмечая на карте свои открытия, а затем обнаружить, что ни у кого другого нет ни сил, ни времени пройти тем же путем, чтобы понять или проверить их.
70
Она же теорема Фейта – Томпсона.