Код креативности. Как искусственный интеллект учится писать, рисовать и думать
- Автор: дю Сотой Маркус
- Год: 2020
- Язык: русский
- Год: Аттикус
- ISBN: 978-5-389-18965-2
- Переводчик: Дмитрий Александрович Прокофьев
- Жанр: Зарубежная образовательная литература
Электронная книга - «Код креативности. Как искусственный интеллект учится писать, рисовать и думать». Краткое содержание книги:
«Искусственный интеллект потрясает самые основы нашего существования, демонстрируя, сколь многое из того, чем занимаются люди, машины могут делать не хуже, а то и лучше их. Но эта книга посвящена не столько будущему с беспилотными машинами и компьютеризованной медициной, сколько вопросу о том, смогут ли алгоритмы состязаться сколько-нибудь существенным образом с могуществом человеческого кода. Способны ли компьютеры к творчеству? Что нужно для творчества? В какой степени эмоциональная реакция на произведения искусства является результатом реакции мозга на определенные рисунки и структуры? Таковы некоторые из тем, которые мы рассмотрим». (Маркус дю Сотой)
В формате PDF A4 сохранен издательский макет книги.
Кроме того, если мы заставляем компьютер проверять доказательство и подтверждать обоснованность каждого его шага, не меняем ли мы тем самым шило на мыло? Откуда нам знать, что в самой компьютерной программе, ищущей ошибки, нет своих ошибок? Можно проверить эту программу на наличие ошибок при помощи другого компьютера, но будет ли конец этим проверкам? Эта дилемма всегда преследовала естественные науки и математику. Как можно быть уверенным, что используемые методы ведут к истинному знанию? Любые попытки это доказать неизменно зависят от методологии, достоверность которой мы пытаемся продемонстрировать.
Как первым отметил Юм, наука в значительной степени основывается на процессе, который называется индукцией: выводе общих законов или принципов на основе наблюдения отдельных случаев. Почему эту процедуру можно считать доброкачественным методом получения научной истины?
В целом на основании той же индукции! Мы можем привести множество примеров, в которых принцип индукции порождал, по-видимому, справедливые научные теории. Это позволяет нам заключить (методом индукции), что индукция – действенный подход к занятиям наукой.
По мере появления все новых и новых доказательств, полученных при помощи компьютерных программ, стала ощущаться необходимость в каких-то средствах, позволяющих убедиться, что этим программам можно доверять. В прошлом математические выкладки, созданные людьми, могли проверить люди. Теперь же нужно было создать новые программы для проверки программ, создающих доказательства, так как люди уже не могли проверять их вычисления – они были слишком сложны.
В конце 1980-х годов два французских математика, Жерар Пьер Юэ и Тьерри Кокан, начали работать над проектом под названием «Исчисление конструкций» (Calculus of Constructions, сокращенно CoC). Поскольку во Франции принято давать средствам для научно-технических разработок названия животных, эта система впоследствии стала называться Coq, что означает по-французски «петух». Это название удачно совпало с первыми тремя буквами фамилии одного из создателей системы. Система Coq была создана для проверки доказательств и вскоре стала любимым инструментом всех тех, кого интересует верификация доказательств, созданных компьютерами.
Жорж Гонтье, руководитель исследовательской программы в кембриджском отделении Microsoft Research, решил организовать группу для проверки доказательства теоремы о четырех красках – первого доказательства, для разработки которого потребовался компьютер, – при помощи Coq. К 2000 году эта группа проверила программный код, созданный Аппелем и Хакеном, и подтвердила правильность доказательства (в предположении, что в самой системе Coq нет своих собственных ошибок). После этого при помощи Coq начали проверять «человеческую» часть доказательства – те построения, которые написали сами Аппель и Хакен.
Одна из трудностей проверки доказательства, созданного человеком, состоит в том, что в нем редко бывают изложены все шаги. Люди пишут доказательства не так, как компьютерные программы. Они пишут их для других людей, используя код, который должен работать только на нашем собственном аппаратном обеспечении – в человеческом мозге. Это значит, что, формулируя доказательство, мы часто пропускаем неинтересные или повторяющиеся шаги, зная, что те, кто будет его читать, сумеют восполнить эти пробелы. Но компьютеру необходимы все шаги. В этом разница между сочинением романа, в котором не нужно детально рассказывать о всех банальных действиях героя, и инструктированием новой няньки, при котором приходится описывать весь день в мельчайших подробностях, в том числе о времени дневного сна, хождении в туалет и всех до последнего пунктах меню ребенка.
Подтверждение правильности человеческой части доказательства заняло у компьютера пять лет. У этого процесса были и интересные побочные результаты: исследователи открыли новые и довольно неожиданные математические жемчужины, которых не заметили авторы исходного доказательства.