Официально


Правительство снизило объем средств, которые будут направлены из бюджета на повышение конкурентоспособности ведущих российских вузов в 2018-2020 годах. Постановление об этом опубликовано на официальном интернет-портале правовой информации.



Госдума приняла в первом чтении внесенный Правительством РФ законопроект об унификации структур по военной подготовке в вузах. Он предусматривает, что в вузах будет один вид структурных подразделений военной подготовки - военные учебные центры.



Госдума рассмотрела в первом чтении проект федерального закона «О внесении изменений в статью 87 ФЗ «Об образовании в РФ» и статью 19 ФЗ «О свободе совести и о религиозных объединениях» в части совершенствования правового статуса духовных образовательных организаций.



Рособрнадзор запретил прием в Институт «Верхневолжье» - за неисполнение предписаний в установленные сроки.






Новости № 27-28(2018)

Регионы


Томский госуниверситет вместе с IT-компанией Rubius приступают к реализации масштабного digital-проекта - “Виртуальный университет 4.0”.

В Совете Федерации прошли Дни Ярославской области. Участие в выставке, организованной в верхней палате принял в том числе Ярославский госуниверситет.

Студенты Воронежского госуниверситета стали победителями международного конкурса IT-Challenge. Его организовала французская корпорация Atos, специализирующаяся на IT-консалтинге, аутсорсинге бизнес-процессов, производстве серверов.

СНГ


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


Группа австралийских политиков опубликовала “дорожную карту” для законодательного закрепления возможности искусственного оплодотворения с донорством митохондрий, сообщает Nature News.

Жизнеспособные эмбрионы исчезающего северного белого носорога получены в лаборатории. С подробностями - The Scientist.


Председатель ВЦИК тов. Свердлов оглашает только что полученное по прямому проводу сообщение от Уральского областного совета о расстреле бывшего царя Николая Романова. В последние дни столице “красного” Урала Екатеринбургу серьезно угрожала опасность приближения чехословацких банд. В то же время был раскрыт новый заговор контрреволюционеров, имевший целью вырватъ из рук советской власти коронованного палача. Ввиду всех этих обстоятельств Президиум Уральского областного совета постановил расстрелять Николая Романова, что и было приведено в исполнение 16 июля...














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

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


 

Отзывы

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



 

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

Как не попасть в ловушки? Прогнозировать развитие страны поможет экономическая томография.
В последние два десятилетия Россия страдала то от дефолта 1998 года, то от мирового кризиса 2008-2009 гг., то от неприятностей, начавшихся в экономике с 2016 года. Можно ли предсказывать такие явления и им эффективно противодействовать? /№ 27-28(2018)
Если друг оказался френд. Как влияют на молодежь современные коммуникации.
Кандидат философских наук Андрей ГЛУХОВ, доцент кафед­ры социальных коммуникаций Томского государственного университета: "На наших глазах происходит цифровая революция в области как профессиональных, так и личных коммуникаций"... /№ 27-28(2018)
Еда по правилам. Надо есть меньше, но больше.
Современный человек так и не научился правильно питаться: с одной стороны, получать из пищи все необходимые микронутриенты, а с другой, - не толстеть и оставаться в хорошей форме. /№ 27-28(2018)

Новости


Около 674 млрд рублей планируется выделить из федерального бюджета на реализацию национального проекта «Образование», заявила вице-премьер Татьяна Голикова на заседании совета Российского союза ректоров. Она напомнила, что реализация нацпроектов рассчитана на шесть лет - до 2024 года.



Полномочия Рособрнадзора фактически остались прежними, сообщил руководитель Федеральной службы по надзору в сфере образования и науки Сергей Кравцов в интервью газете «Коммерсант». Ничего принципиально, по его словам, не меняется и в вопросе проверок институтов.



Ректор МГУ Виктор Садовничий провел первое заседание Центральной приемной комиссии МГУ. Общий конкурс в этом году составил примерно 7,6 человека на место - это чуть больше, чем в 2017 году, сообщил Виктор Антонович.



Самым возрастным участником экзаменационной кампании стал 77-летний мужчина, который сдавал ЕГЭ по математике профильного уровня и физике. Об этом сообщили ТАСС в пресс-службе Рособрнадзора.



Ученые высокого уровня продолжают уезжать из России - таков один из выводов авторов очередного Национального доклада об инновациях в России.

Все вузы должны иметь возможность проводить свое дополнительное вступительное испытание, заявил ректор МГИМО Анатолий Торкунов в эфире телеканала «Спас».

Более 1 миллиона человек стали выпускниками российских вузов в 2018 году, сообщила вице-премьер Татьяна Голикова на церемонии вручения красных дипломов выпускникам Российской академии народного хозяйства и государственной службы при Президенте РФ. Из них 455 тыс. человек учились на бюджетных местах.

Конференции


II Всероссийская научно-практическая конференция “Совершенствование системы взаимодействия Российского фонда фундаментальных исследований и субъектов Российской Федерации в вопросах проведения региональных и молодежных конкурсов”

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

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

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


Российская академия наук (РАН) и Национальная академия наук Беларуси (НАН Беларуси) объявляют конкурс на соискание трех премий за выдающиеся научные результаты, полученные российскими и белорусскими учеными при проведении совместных работ в области естественных, технических, гуманитарных и социальных наук и имеющие важное научное и практическое значение.

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

Конкурс на лучшие проекты фундаментальных научных исследований

Конкурс на лучшие проекты, выполняемые молодыми учеными (Эврика! Идея)

Международный научный фонд экономических исследований академика Н.П.Федоренко (МНФЭИ) объявляет конкурсы 2018 года

Вакансии


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

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

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




опрос

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




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