Курс лекций–семинаров на тему «Модальные логики и многоагентные системы»
Каждый вторник начиная с 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.