Владимир Воеводский — человек в научных кругах заметный и знаменитый: Филдсовский лауреат, единственный профессор с российскими корнями в престижном Институте перспективных исследований (Institute for Advanced Study) в Принстоне (США), несколько лет занимается разработкой нового научного направления, которое, по его убеждению, может принести огромную пользу математическому сообществу. В интервью корреспонденту “Поиска” четырехлетней давности Владимир Воеводский рассказывал о работе над “основаниями математики” (“Foundations”), а в конце августа приехал на Форум лауреатов в Гейдельберг с лекцией о готовой программной оболочке UniMath, которая представляет собой формализованную библиотеку математических определений и теорем и по сути является той самой “палочкой-выручалочкой” для его коллег. О деталях работы мы и расспросили ученого.
— Давайте по порядку: почему вы двинулись в эту область?
— Я пришел с очень простым желанием — иметь компьютерную программу, которую можно использовать, чтобы проверять свои доказательства и не морочить себе голову сомнениями, что где-то допущена ошибка. Поначалу спрашивал у всех, кого знал: существует ли такая программа, чтобы проверила, например, доказательство леммы в 10 строк. Когда я только начал задавать эти вопросы — это было году в 2003, — то обнаружил, что существует множество программ-помощников (proof assistant), но ни одна из них мне не годится, ни в одной из них я не могу даже начать писать доказательство. В их языке не было тех слов, выражений и структур, которые нужны, чтобы сформулировать простую лемму. Выяснив это, я года на два отвернулся от темы.
У меня была альтернативная идея, чем заняться: я решил попытаться придумать некие математические подходы к исторической генетике, но обнаружилось, что в той математике, которую я начал строить, мне опять был нужен proof assistant. И все из-за того, что я снова начал делать ошибки (одну не замечал целый год)… Тогда я опять вернулся к этой теме и решил посмотреть, что изменилось за два года. Кое-какие изменения были, да и у меня самого начали появляться идеи, связанные с формализаций, я начал их разрабатывать, но снова отложил… Так было неоднократно, но в конце концов, когда я в очередной раз вернулся к задаче проверки доказательств (это было примерно в 2009 году), у меня как-то сразу получилась одна или две вещи, после чего я окончательно понял, что имеющиеся наработки позволяют заняться этим всерьез.
— Другими словами, идея отлежалась…
— Это не была одна идея, это, скорее, было желание, которое постепенно обрастало идеями по поводу того, как его можно осуществить. И когда оно обросло достаточным количеством идей и реальностей, я отложил в сторону остальное.
— Я правильно понимаю, что хотелось иметь программу, в которую можно заложить свои доказательства либо рассуждения и на выходе получить ответ, что где-то пробел в логике или иная ошибка (в том случае, если они есть)?
— Сначала я именно так это себе и представлял, и в голове была точно такая же картина. Но потом оказалось, что гораздо больший прогресс достигается в другом направлении. Не в том, когда сначала вырабатывается доказательство, а потом оно закладывается в машину. А в том, когда доказательство происходит в диалоге с машиной.
Это можно сравнить с компьютерной игрой. Вы говорите в режиме реального времени: я хочу доказать утверждение. Программа проверяет, что оно правильно написано, что оно имеет смысл, а потом вы ей предлагаете попробовать разные ходы доказательства. То есть происходит диалог. Иногда у вас заранее есть какой-то план, а иногда все делается без предварительной подготовки.
— Это похоже на разговор учителя с учеником. Ученик демонстрирует ход решения преподавателю, а тот корректирует, если надо.
— Тут не очень понятно, кто ученик, а кто учитель. Аналогия, которая приходит в голову мне, — это работа с тупым, но аккуратным аспирантом. Вы ему говорите: попробуй это. Он на следующий день сообщает: я попробовал, все получилось. То есть если ему четко сказать, что надо делать, он это выполнит и принесет вам результат. А дальше вы сами принимаете решение, что с этим результатом делать и куда двигаться. Здесь идет диалог и пошаговая проверка. Доказательство строится кирпичик за кирпичиком, и на каждом шаге система проверяет, чтобы все они лежали на своих местах.
— Получается очень педантичная работа. Говорить о каком-то озарении, которое может увести в сторону, при этом не приходится? Пошаговость в этом случае нарушится.
— Озарению ничто не мешает. Вот я строил в одну сторону доказательство, потом понял, что можно сделать по-другому, повернул в другую сторону, начинаю выстраивать по новой.
— Программа работает для тех целей, которые вы для себя обозначили?
— Да, мне удалось создать унивалентный подход к формализации, который позволяет использовать программную оболочку UniMath для того, чтобы записывать те утверждения, которые мне нужны. Сейчас я могу запросто записать лемму и проверить ее доказательство, у меня есть этот язык. Точнее, язык был давно — он называется Coq, но теперь я знаю, как его использовать для решения математических задач.
— Как все же родилась UniMath?
— Ее ядро — мои Foundations и еще несколько библиотек, которые использовали “основания” в качестве базиса. Я был инициатором всего этого, потом привлек к работе нескольких людей. Сегодня в команде Unimath Development Team четыре человека. Помимо меня это Бенедикт Аренс, Даниэл Грейсон и Майкл Уоррен. Само название UniMath года полтора назад подсказал Дэн Грейсон.
— Вы же не специалист в программировании, а здесь наверняка приходилось писать коды, программы.
— Кстати, я умею писать программы. Когда-то на первом курсе мехмата я подрабатывал, преподавая программирование. Так что в этой области я себя чувствую комфортно. Но практически мне этого делать не пришлось, потому что я задействовал готовую систему Coq, которая к тому времени существовала лет 20… Она очень общая, ее можно применять для многих целей. В том числе для того, чтобы проверять логические манипуляции. Оттолкнувшись от нее, я придумал новый стиль ее использования, новый способ записывать математику.
— А вы можете сказать: разработанная мною программа уже позволила мне сделать то-то и то-то? Или вы продолжаете работать над совершенствованием системы UniMath, и это сегодня основная ваша задача?
— Я сейчас продолжаю заниматься не столько даже совершенствованием UniMath, сколько тем, чтобы убедить математиков, что способу использования компьютерной системы, который я придумал, действительно можно доверять. То есть если система говорит, что доказательство правильное, то оно действительно правильное. Это неочевидно, в этом надо людей убедить. Иногда меня просят: вот утверждение, вот доказательство — запиши его на Coq и проверь. Допустим, я соглашаюсь, что-то начинаю писать — буковки-символы. И в итоге говорю: да, правильно. Но где гарантия того, что в этом есть какая-то ценность? Может, я вообще фигню полную написал, а потом сказал, что все отлично. Где гарантия того, что система действительно проверяет математические доказательства?
— То есть что выводы системы — истина.
— Да, где гарантия того, что этот так называемый преподаватель не ошибается, что он квалифицирован. И это очень непростой вопрос, потому что язык, на котором говорит этот преподаватель, отличается от того языка, на котором говорят математики.
— Было бы идеально, если бы он обнаруживал какие-то ошибки. Например, в общепринятом доказательстве.
— В общепринятых доказательствах система вряд ли найдет ошибку. Они на то и есть общепринятые, что их проверили миллион раз. Какие-то небольшие неточности, конечно, выплывают. Но у математиков другая психология. Их не интересуют доказательства, которые верны с вероятностью 99 процентов.
— Не их, а “нас, математиков” не интересуют…
— Я говорю “их”, потому что сейчас выступаю с позиций не математика, а человека, который пытается создать некий инструмент в помощь математикам. Если бы речь шла про медицину, то я бы выступал как человек, который пытается создать для врачей стерилизационный прибор, например. Но у врачей условие — им надо, чтобы стерилизационная машина убивала не 99 процентов бактерий, а всех. Примерно та же ситуация и здесь.
Тут есть еще одно обстоятельство, очень существенное. Дело в том, что компьютерную программу (Coq) пишет некий коллектив разработчиков. Этот коллектив ее все время улучшает, и каждые два года появляется новая версия, в которой что-то добавлено, что-то убрано, и доказывать математические утверждения становится проще. То есть программа становится более умной, ей можно давать менее точные указания, и она будет знать, как им следовать. Но допустим, что я уверен в предыдущей версии и доверяю ей. Откуда я знаю, что в новой версии не появилось ошибок? Да, она стала более умной, но где гарантия, что в процессе улучшений она не стала менее точной? То есть нужна некая методология, позволяющая сделать так, чтобы подобные системы могли развиваться, но при этом в них самих не начали накапливаться ошибки. Над этим я сейчас и работаю.
— Это уже задача из области Computer Science?
— Нет, она, скорее, математическая, потому что системы нужно описывать математикой. Получается довольно интересная и достаточно неожиданная прикладная математика, только все интересные структуры возникают не в приложении ее к физике, например, а в приложении математики к программированию. При этом объекты, которые надо изучать математическими методами, — не элементарные частицы в ускорителях, а компьютерные программы. Они, кстати, не менее сложны для изучения, чем частицы.
— А как восприняло математическое сообщество этот инструмент?
— Я бы сказал, что пока оно не доверяет ему. Сами Foundations были написаны в конце 2009 года. Но даже сейчас, когда проделана огромная работа, чистым пользователям работать с UniMath сложно. Там очень многому нужно обучиться. И, к сожалению, там еще многому нужно поверить. А математики этого не любят. Там надо поверить, что это не бред, грубо говоря.
— А как устроена жизнь в вашем сообществе математиков – вы, как пауки в банке, каждый другого не очень любит, часто не доверяет? Или, напротив, ревностно друг за другом следите, радуетесь чужим успехам?
— Там довольно сложная экология. Я несколько со стороны на нее смотрю сейчас, может быть, еще и потому, что в последние годы очень активно взаимодействую с Computer Science. Так вот, в математике есть много людей, которые мне в каком-то смысле ближе всего, и я за них переживаю. Это люди, которые до такой степени погружены в свои математические интересы… они пытаются решить некую задачу, причем не один год уже пытаются, и часто этот процесс очень тягостный… Я был в этом положении, я знаю, как это энергетически истощает, как это тяжело и как часто это может быть неэффективно. Такая работа не приносит никакого удовлетворения, при этом забирает у человека огромное количество энергии, и он оказывается изолирован от всего, что происходит вокруг. Там много умных и интересных людей — в этой биологической картинке они как будто залезли в какую-то “нору” и пытаются в ней что-то выкопать. Они там много лет сидят и ничего, кроме этой норы, вокруг себя не видят. Это один тип математиков, и среди них очень много хороших людей. У меня есть мечта, что как раз благодаря этой формальной системе, разработанному мною “помощнику”, многие из них смогут выбраться из своих убежищ.
Другой тип — это люди, которые “норы” давно покинули и теперь боятся туда заглядывать, а вместо этого занимаются совершенно другой деятельностью и нередко используют для своих целей тех, первых.
— В тот период, когда вы сами были в “норе”, вы отозвались бы на такого рода помощь?
— Думаю, да. Я чувствовал сложность ситуации, и proof assistant мог бы очень помочь, потому что он освобождает мозг от бесконечных проверок и перепроверок самого себя — не столько даже от рутины, сколько от неуверенности.
— Как вам видится — наверное, ваш проект бесконечный, его завершить нельзя? Как стремление к совершенству.
— Его не то чтобы нельзя завершить. Я хотел бы создать нечто, что будет жить. То есть придать этому информационному, интеллектуальному существу какие-то начальные правила и параметры, которые позволят ему развиваться дальше. И именно поэтому я вкладываю огромную энергию в то, чтобы у него была крепкая основа, чтобы оно могло долго расти и приносить пользу.
Беседовала
Светлана Беляева
Фото автора
Нет комментариев