Официально


Комитет Госдумы по образованию и науке рассмотрел законопроект, касающийся предоставления льгот детям-сиротам при поступлении в высшие учебные заведения, «О внесении изменения в статью 92 ФЗ «Об образовании в РФ» (в части установления в Положении о государственной аккредитации образовательной деятельности порядка учета сведений о независимой оценке качества подготовки обучающихся)».



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



Правительство обсудило ход выполнения федеральных целевых программ и федеральной адресной инвестиционной программы. По итогам заседания отмечена «низкая эффективность реализации за 9 месяцев 2018 года федеральных целевых программ «Исследования и разработки по приоритетным направлениям развития научно-технологического комплекса России на 2014-2020 годы» и «Развитие космодромов на период 2017-2025 годов в обеспечение космической деятельности РФ»».



Правительство установило ограничение, в соответствии с которым среднемесячный размер зарплаты президента Российской академии наук не может превышать 13-кратный размер среднемесячной зарплаты сотрудников академии.




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

Регионы


СНГ


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


Пауки-скакуны вскармливают потомство “молоком”. Без этого чудодейственного секрета паучата погибают в первые десять дней жизни.

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

Радиоуглеродный анализ ДНК “сибирского единорога” показал, что он вымер почти одновременно с заселением мест своего обитания людьми, но люди к этому не причастны.


Сообщают, что на оружейном заводе розыгрыш галош происходил между всеми рабочими, не выключая тех, кто выиграл галоши летом. Таким образом, один мог выиграть галоши и летом и теперь, а другой - ни тогда, ни теперь. Надо на следующие разы исключать тех, кто получил галоши в прежние розыгрыши, чтобы не было обидно оставшимся без галош.














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

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


 

Отзывы

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



 

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

Сон в руки. Стоит выспаться - и все получится.
Можно ли треть жизни провести в обнимку с подушкой?! Да, мы принадлежим к млекопитающим, но нельзя же, как и все зверье, тупо следовать традициям эволюции. Между прочим, мозг, а это - наше все, никогда не отдыхает. Так почему бы нам не следовать его примеру? /№ 49(2018)
Недостатки достатка. Как богатому не стать больным.
Научный руководитель Федерального исследовательского центра питания, биотехнологии и безопасности пищи академик Виктор ТУТЕЛЬЯН выступил на заседании Президиума РАН с докладом “Об актуальных проблемах оптимизации питания населения России: роль науки”. /№ 48(2018)
Век интеграторов. Ученые объединяются, чтобы прочнее связать территорию страны.
Во Дворце культуры Московского авиационного института (национального исследовательского университета) прошла V Международная неделя авиакосмических технологий Aero-space Science Week (ASW). /№ 48(2018)

Новости


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



В 2019 году планируется создание международной Ассоциации академий образования. Об этом президент Российской академии образования Юрий Зинченко сообщил на заседании Попечительского совета РАО.



МГУ им. М.В.Ломоносова и ректор университета академик Виктор Садовничий удостоены орденов Дружбы Социалистической Республики Вьетнам. Награды вручил посетивший вуз посол Вьетнама в РФ Нго Дык Мань.



Более 640 тысяч россиян воспользовались программами материнского капитала на получение образования ребенком с момента появления такой услуги, сообщает сообщила пресс-служба Минпросвещения.

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

Ассоциация «Глобальная энергия» подвела итоги Общероссийского конкурса молодежных исследовательских проектов в области энергетики «Энергия молодости».

Спикер Совета Федерации Валентина Матвиенко, выступая на заседании Совета по вопросам интеллектуальной собственности при верхней палате парламента, предложила подумать о введении в России должности уполномоченного по защите прав изобретателей. «Это придаст новые силы нашим изобретателям. Они будут знать, что защищены он и его права», - сказала она.

Конференции


22 ноября ИСП РАН им. В.П. Иванникова в рамках своей Открытой конференции, посвященной 70-летию отечественного ИТ-сектора, заключил соглашение с АО «НПО РусБИТех» о продаже лицензии на статический анализатор Svace и динамический анализатор Crusher. Сделка позволит предприятию-разработчику отечественной сертифицированной операционной системы Astra Linux обнаруживать ошибки кода на ранних стадиях и повысить доверие к безопасности своей платформы, используемой в государственных и коммерческих информационных системах, в том числе в критически важных секторах экономики.

22-23 ноября в здании Президиума Российской академии наук прошла Открытая конференция ИСП РАН им. В.П.Иванникова, посвященная 70-летию российского ИТ-сектора. На ней обсудили проекты и технологии, имеющие глобальное значение.

Международная научная конференция ПАРАЛЛЕЛЬНЫЕ ВЫЧИСЛИТЕЛЬНЫЕ ТЕХНОЛОГИИ 2-4 апреля 2019 года, Калининград, Балтийский федеральный университет

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


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

Региональный конкурс проектов фундаментальных научных исследований, выполняемых молодыми учеными

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

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

Конкурс работ, представляемых на соискание премий Правительства Российской Федерации 2019 года в области науки и техники.

Вакансии


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

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

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


опрос

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




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