Официально


Указом Президента РФ в перечень федеральных государственных вузов, которые вправе разрабатывать и утверждать самостоятельно образовательные стандарты по всем уровням высшего образования, внесен Российский университет транспорта (МИИТ).



За многолетний труд на благо сельскохозяйственной науки, большой вклад в развитие отечественной аграрной науки и в связи с юбилеем Президиум РАН наградил Почетной грамотой Российской академии наук академика Эльмиру Крылатых. Почетной грамоты Российской академии наук также удостоен коллектив лбщественной организации «Центр-Клуб земляков-оренбуржцев в Москве». Они отмечены за совместное плодотворное сотрудничество с Российской академией наук и большую научно-поисковую и патриотическую работу.

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

Законопроект об обязательном распределении выпускников в госкомпании после окончания учебы в вузах внесен на рассмотрение Госдумы. Документ размещен в базе законопроектов на сайте ГД, его автором выступил депутат «Единой России» Сергей Вострецов.




Новости № 16(2018)

Регионы


СНГ


Интердайджест


















Виден выход из норы. Труд математиков можно облегчить.
Наука
№ 38(2015)

18.09.2015

Владимир Воеводский - человек в научных кругах заметный и знаменитый: Филдсовский лауреат, единственный профессор с российскими корнями в престижном Институте перспективных исследований (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 мог бы очень помочь, потому что он освобождает мозг от бесконечных проверок и перепроверок самого себя - не столько даже от рутины, сколько от неуверенности.
- Как вам видится - наверное, ваш проект бесконечный, его завершить нельзя? Как стремление к совершенству.
- Его не то чтобы нельзя завершить. Я хотел бы создать нечто, что будет жить. То есть придать этому информационному, интеллектуальному существу какие-то начальные правила и параметры, которые позволят ему развиваться дальше. И именно поэтому я вкладываю огромную энергию в то, чтобы у него была крепкая основа, чтобы оно могло долго расти и приносить пользу.

Беседовала
Светлана Беляева
Фото автора


 

Отзывы

Чтобы оставить отзыв необходимо авторизоваться или зарегистрироваться



 

Статьи на тему

Разминка для ума. От “игры в бисер” - к реальным проблемам робототехники и нейротехнологий.
Руководитель Научно-образовательного центра “Системы искусственного интеллекта и нейротехнологии” Саратовского государственного технического университета им. Ю.А.Гагарина профессор Александр ХРАМОВ и его научный коллектив стали обладателями крупного гранта РНФ по Президентской программе исследовательских проектов. /№ 16(2018)
Как ключ к замку. Новый метод доставки лекарств в разы увеличит их эффективность.
Ученые все искуснее применяют нанотехнологии в самых разных сферах. То, что они делают, иногда кажется настоящей фантастикой. Например, использование наночастиц для адресной доставки лекарств к больным клеткам. /№ 16(2018)
А орешки не простые… Позолоченные наношарики - универсальное оружие в борьбе с больными клетками.
Нанотехнологии становятся все сложнее. Скажем, нанокомпозиты для диагностики болезней и лечения покрывают сложной органикой - антителами и молекулами-репортерами. Основой для этого служат “шипастые” нанозвездочки или похожие на орешки нанооболочки... /№ 16(2018)

Новости


Совет по науке при Минобрнауки выступил с заявлением, в котором выражена глубокая обеспокоенность в связи с внесением в Госдуму законопроекта «О мерах воздействия (противодействия) на недружественные действия США и (или) иных иностранных государств». Члены совета считают, что предложенные в законопроекте меры могут нанести существенный ущерб развитию российской науки и технологий.



Россия должна привлекать на работу лучших ученых и продолжать взаимодействие с международными научными организациями. На решение этих задач направлены поручения Владимира Путина, которые он дал по итогам заседания Совета при Президенте РФ по науке и образованию и встречи с учеными Сибирского отделения РАН, прошедших в феврале 2018 года.



Совет Межрегионального общества научных работников обратился с заявлением к председателю Госдумы Вячеславу Володину.



На территории ВДНХ начал работу V Московский международный салон образования.



Федеральное агентство научных организаций завершило очередной прием заявок от подведомственных организаций на выполнение экспедиционных работ в Мировом океане и внутренних водоемах России на научно-исследовательских судах в 2019 году. Всего было получено более 60 заявок от 19 научных институтов, подведомственных ФАНО, сообщает пресс-служба ведомства.



НИЦ «Курчатовский институт» восстановит работу Черноморской коррозионной станции в Севастополе и рассмотрит возможность открытия в городе своего филиала, заявил президент НИЦ Михаил Ковальчук на встрече с губернатором Севастополя Дмитрием Овсянниковым во время церемонии подписания соглашения о сотрудничестве.



Рыбохозяйственные институты вместе с Российской академией наук разработают совместную программу по исследованиям Антарктики. В следующем году в бюджете на эти цели планируется заложить более 600 млн рублей.



Конференции


Пятая конференция разработчиков российских операционных платформ «OS DAY. Надежность» состоится 17-18 мая 2018 г. в Москве, в главном здании Российской академии наук. Основной темой для обсуждения среди теоретиков и практиков системного программирования и разработки ОС станет вопрос надежности. Участники рассмотрят методы проектирования и разработки надежных платформ, инструментальные средства обеспечения надежности программно-аппаратных систем как на этапе разработки, так и на этапе эксплуатации.

Центр научно-информационных исследований по науке, образованию и технологиям ИНИОН РАН совместно с Институтом экономических стратегий проводят МОСКОВСКИЙ ГОРОДСКОЙ СЕМИНАР ПО НАУКОВЕДЕНИЮ И НАУКОМЕТРИИ

Центр научно-информационных исследований по науке, образованию и технологиям ИНИОН РАН совместно с Институтом экономических стратегий проводят Московский семинар по науковедению и наукометрии.

Текущие конкурсы


Федеральное государственное автономное образовательное учреждение высшего образования “Московский физико-технический институт (государственный университет)” объявляет конкурс на замещение должностей педагогических работников, относящихся к профессорско-преподавательскому составу

Конкурс 2018 года на лучшие научные проекты междисциплинарных фундаментальных исследований по теме “Большие данные в постгеномную эру” (“мк”)

Конкурс 2018 года на лучшие научные проекты междисциплинарных фундаментальных исследований по теме “Правовое регулирование геномных исследований” (“мк”)

Конкурс 2018 года на лучшие научные проекты междисциплинарных фундаментальных исследований по теме “Модели правового регулирования международного научно-технического сотрудничества и международной интеграции России” (“мк”)

Конкурс 2018 года на лучшие научные проекты междисциплинарных фундаментальных исследований по теме “Трансформация права в условиях развития цифровых технологий” (“мк”)

Вакансии


02.03.2018
объявляет конкурс на замещение вакантных должностей:

17.11.2017
Федеральное государственное бюджетное учреждение науки Институт геологии рудных месторождений, петрографии минералогии и геохимии Российской академии наук (ИГЕМ РАН) объявляет конкурс на замещение вакантной должности...

03.11.2017
Федеральное государственное бюджетное учреждение высшего образования и науки Санкт-Петербургский национальный исследовательский академический университет Российской академии наук объявляет конкурс на замещение следующих вакантных должностей...




опрос

Какие рубрики нашей газеты Вам наиболее интересны?




Copyright 2010
Главная страница   |   О газете  |  Партнеры  |  Команда Поиска  |  Вакансии