• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта
Контакты

Адрес: 123458, Москва, ул. Таллинская, д.34
Телефон: 8(495)916-88-29
Факс: 8(495)916-88-29
Эл. почта: miem@hse.ru

     
Руководство
и.о. директора, научный руководитель Крук Евгений Аврамович
Заместитель директора Абрамешин Андрей Евгеньевич
Заместитель директора Романов Виктор Владимирович
Заместитель директора Костинский Александр Юльевич
Заместитель директора Прохорова Вероника Борисовна
Заместитель директора по учебной работе Тумковский Сергей Ростиславович
Заместитель директора по научной работе Аксенов Сергей Алексеевич
Образовательные программы
Бакалаврская программа

Инфокоммуникационные технологии и системы связи

4 года
Очная форма обучения
50/10/5
50 бюджетных мест
10 платных мест
5 платных мест для иностранцев
RUS
Обучение ведётся на русском языке
Бакалаврская программа

Информатика и вычислительная техника

4 года
Очная форма обучения
100/50/15
100 бюджетных мест
50 платных мест
15 платных мест для иностранцев
RUS
Обучение ведётся на русском языке
Бакалаврская программа

Информационная безопасность

4 года
Очная форма обучения
30/20
30 бюджетных мест
20 платных мест
RUS
Обучение ведётся на русском языке
Программа специалитета

Компьютерная безопасность

5,5 лет
Очная форма обучения
30/45/1
30 бюджетных мест
45 платных мест
1 платное место для иностранцев
RUS
Обучение ведётся на русском языке
Бакалаврская программа

Прикладная математика

4 года
Очная форма обучения
80/40/6
80 бюджетных мест
40 платных мест
6 платных мест для иностранцев
RUS
Обучение ведётся на русском языке
Магистерская программа

Инжиниринг в электронике

2 года
Очная форма обучения
30/5/2
30 бюджетных мест
5 платных мест
2 платных места для иностранцев
RUS
Обучение ведётся на русском языке
Магистерская программа

Интернет вещей и киберфизические системы

2 года
Очная форма обучения
20/5/2
20 бюджетных мест
5 платных мест
2 платных места для иностранцев
RUS
Обучение ведётся на русском языке
Магистерская программа

Компьютерные системы и сети

2 года
Очная форма обучения
50/15/2
50 бюджетных мест
15 платных мест
2 платных места для иностранцев
RUS
Обучение ведётся на русском языке
Магистерская программа

Математические методы моделирования и компьютерные технологии

2 года
Очная форма обучения
20/5/3
20 бюджетных мест
5 платных мест
3 платных места для иностранцев
RUS
Обучение ведётся на русском языке
Магистерская программа

Материалы. Приборы. Нанотехнологии

2 года
Очная форма обучения
20/10/2
20 бюджетных мест
10 платных мест
2 платных места для иностранцев
RUS
Обучение ведётся на русском языке
Магистерская программа

Системы управления и обработки информации в инженерии

2 года
Очная форма обучения
25/5/2
25 бюджетных мест
5 платных мест
2 платных места для иностранцев
RUS
Обучение ведётся на русском языке
Магистерская программа

Суперкомпьютерное моделирование в науке и инженерии

2 года
Очная форма обучения
20/5/4
20 бюджетных мест
5 платных мест
4 платных места для иностранцев
RUS/ENG
Обучение ведётся на русском и английском языках

Курс лекций–семинаров на тему «Модальные логики и многоагентные системы»

Уважаемые преподаватели и студенты!
Каждый вторник начиная с 10.09.2019 с 16:40 до 19:30, в аудитории 506, Таллинская, д 34. известный специалист в области верификации и логики Юрий Глебович Карпов прочтет в МИЭМ НИУ ВШЭ курс лекций – семинаров на тему «Модальные логики и многоагентные системы». Аналоги этого курса также читаются в Стенфорде,  MIT, МФТИ.

"Каковы те базовые понятия и умения в области логики,
которым нужно обучать всех начинающих студентов,
и которые могли бы остаться в их будущей жизни
как постоянно востребованный культурный багаж,
даже если эти студенты в своем подавляющем большинстве
не станут профессиональными логиками?"

Johan van Benthem

Эта цитата из введения в курс "Логика в действии", читаемый в нескольких ведущих университетах мира. В нем авторы расширяют изложение классической логики представлением модальных логик и демонстрацией их применения к проблемам ИИ. Данный курс имеет подобную цель: представление основных концепций модальных логик не только как теории рассуждений с модальностями, но и как «строительных лесов» окружающего мира с его новой реальностью - многоагентными системами искусственного интеллекта.

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

Человечество находится на грани перемен, которые сравнимы с появлением разумного человека на Земле” - Vernor Vinge.

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

"Развитие ИИ чревато появлением нового риска для человечества — страшнее атомной войны и экологической катастрофы" -Дм. Волков.
 "Мы еще никогда не оказывались в настолько опасной ситуации" - Т.Черниговская. 

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

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

План курса "Модальные логики и многоагентные системы"

1. Мотивация

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

2. Примеры

"Сильные" и "слабые" характеризации истины. Модальности. Примеры задач, формулировка и решение которых использует разнообразные модальности.

3. Модальная логика

Синтаксис и семантика модальной логики. Модели и шкалы Крипке. 
Теория корреспонденции. Аксиоматические системы модальных логик.

4. Конкретные модальные логики и их приложения

4.1. Модальная эпистемическая логика - логика знаний MEL

а) формализация проблем с помощью эпистемических моделей;
б) рассуждения 'с точки зрения другого' и социальное взаимодействие;
в) знания в группе агентов, "групповое" и "общее" знание;
г) "общее" знание и социальная координация.

4.2. Темпоральные логики - логики времени

а) линейное и ветвящееся время, темпоральные логики LTL, CTL*, CTL.
б) формализация требований к поведению программных и аппаратных систем;
в) верификация программных и аппаратных систем;
г) синтез супервизорного управления координированным поведением систем.

4.3. Деонтические логики - логики законов и норм

а) деонтическая логика: формализация 'нормативных' рассуждений;
б) проблемы и парадоксы деонтической логики SDL;
в) электронные контракты;
г) нормативная темпоральная логика NTL; анализ и синтез коллективов агентов с нормативным поведением.

5. Философская составляющая

Даже поверхностное изложение модальных логик не может не касаться глубоких философских проблем. Определяются ли все свойства знания аксиомами логики MEL? Что такое время? Почему логика столь необычайно эффективна в компьютерных науках? Что такое этика и мораль? Все эти вопросы так или иначе затрагиваются в курсе.

6. Курсовые (самостоятельные) работы

1) Принятие решений в карточных играх. Игра "тузы и восьмерки". MEL.
2) Спецификация требований и верификация аппаратных систем с памятью. LTL.
3) Верификация программных управляющих систем. CTL.
4) Синтез многоагентных систем с координированным поведением агентов. NTL.