Курс посвящен изложению актуального раздела математики и информационных технологий — применению методов искусственного интеллекта в задачах анализа данных и верификации программ.
В курсе будут излагаться логические формализмы, связанные с проведением интеллектуальных рассуждений о правильности программ, и будут даны различные иллюстрации проведения интеллектуальных рассуждений для различных классов программ и протоколов, в том числе для параллельных и распределенных программ и криптографических протоколов. Анализ моделей программ (model checking) связан с другими подходами — построением диаграмм переходов программ (моделей Крипке), которые представляют собой большие графы и во многих случаях требуют для своего анализа с приемлемой сложности упрощения до компактных вероятностных автоматных моделей. В курсе будет дано введение в вероятностные автоматные модели, основанное на работах автора по вероятностным автоматам. Важное место в теории дедуктивной верификации занимает область моделирования и верификации криптографических протоколов. В курсе будет изложено введение в разработанные автором новые методы интеллектуального анализа криптографических протоколов. Также в курсе будут изложены разделы, относящиеся к интеллектуальным методам прогнозирования. Будут представлены алгоритмы экспоненциального смешивания экспертных прогнозов (как детерминированные, так и вероятностные), агрегирующий алгоритм В.Г.Вовка, алгоритм усиления классификаторов (бустинг). В последнее время в области интеллектуальных методов прогнозирования развивается применение теоретико-игровых методов, в курсе будет дано введение и в эти методы, в том числе будет изложено построение игр на рандомизированные калибруемые предсказания.
В результате освоения курса студенты получат знания в области применения методов искусственного интеллекта для решения задач верификации программ и анализа данных.
Для прохождения курса студентам необходимы знания математической логики, линейной алгебры, дискретной математики.
Темы, изучаемые в рамках курса
1. Обзор основных направлений искусственного интеллекта. Интеллектуальные методы автоматизации логических рассуждений. Интеллектуальные методы спецификации и верификации программ. Интеллектуальный анализ данных. Основные задачи теории машинного обучения и прогнозирования.
2. Основные проблемы верификации программ. Модели последовательных программ. Блок-схемы программ. Дедуктивная верификация программ на основе метода Флойда.
3. Процессные модели параллельных программ. Дедуктивная верификация параллельных программ.
4. Дедуктивная верификация протоколов передачи данных.
5. Дедуктивная верификация криптографических протоколов.
6. Верификация программ на основе метода model checking.
7. Основные подходы к решению задач классификации данных.
8. Метод опорных векторов.
9. Прогнозирование временных рядов на основе алгоритма взвешенного большинства.
10. Алгоритм оптимального распределения потерь.
11. Алгоритм прогнозирования временных рядов на основе следования за возмущенным лидером (Follow the Perturbed Leader).
12. Метод бустинга для усиления слабых классификаторов.
13. Алгоримы экспоненциального смешивания экспертных прогнозов.
14. Агрегирующий алгоритм В.Г.Вовка.
15. Введение в теорию игр. Построение игр с рандомизированными калибруемыми предсказаниями.
Список литературы
Основная литература
1.1. Миронов А.М., Математические модели и методы верификации процессов, ООО МАКС Пресс (Москва) , ISBN 978-5-317-06893-6, 104 с., 2022
1.2. Миронов А.М. Верификация программ: Часть 1: нерекурсивные программы, МАКС Пресс Москва, ISBN 978-5-317-05721-3, 76 с., 2017
1.3. Миронов А.М. Теория функциональных программ. Издательство ИПИ РАН, Москва, ISBN 978-5-91993-024-2, 160 с., 2013
1.4. Вьюгин В. В. Математические основы машинного обучения и прогнозирования, М.: МЦНМО, 384 с., 2018.
Дополнительная литература
2.1. Миронов А.М. Верификация программ методом model checking, ООО МАКС Пресс (Москва), ISBN 978-5-317-06514-0, 74 с., 2020
2.2. Миронов А.М., Машинное обучение, часть 1, ООО МАКС Пресс (Москва), ISBN 978-5-317-06012-1, 90 с., 2018
Занятия проводятся в Главном Здании МГУ им. М. В. Ломоносова
В программе курса 25 занятий: 13 лекций и 12 практических занятий
Старт курса: с 15 февраля 2023
Лекции проходят по средам с 17:00 до 18:30 в ауд. 14-08, семинары - по четвергам с 18:30 по 20:00 в ауд. 13-03
Студентам будут предлагаться домашние задания после каждого занятия.
Запись на курс на сайте: https://lk.msu.ru/course
Telegram
Набор на курс 2023 года закрыт
Занятия проводятся в Главном Здании МГУ им. М. В. Ломоносова
В программе курса 25 занятий: 13 лекций и 12 практических занятий
Старт курса: с 15 февраля 2023
Лекции проходят по средам с 17:00 до 18:30 в ауд. 14-08, семинары - по четвергам с 18:30 по 20:00 в ауд. 13-03
Студентам будут предлагаться домашние задания после каждого занятия.
Запись на курс на сайте: https://lk.msu.ru/course
Telegram
Набор на курс 2023 года закрыт