Войти
Математика 13 лекций
Методы искусственного интеллекта в задачах анализа данных и верификации программ
Лектор
Миронов Андрей Михайлович
#лекции #мфк
Механико-математический факультет
2024

Курс посвящен изложению актуального раздела математики и информационных технологий — применению методов искусственного интеллекта в задачах анализа данных и верификации программ.

Область верификации программ традиционно подразделяется на два направления: дедуктивную верификацию и анализ моделей программ (model checking). Дедуктивная верификация связана с построением математических доказательств теорем о том, что анализируемые программы обладают заданными свойствами. Задачи построения математических доказательств формальных утверждений относятся к классическим задачам искусственного интеллекта — автоматизации логических рассуждений. В курсе будут излагаться логические формализмы, связанные с проведением интеллектуальных рассуждений о правильности программ, и будут даны различные иллюстрации проведения интеллектуальных рассуждений для различных классов программ и протоколов, в том числе для параллельных и распределенных программ и криптографических протоколов.

Также в курсе будут изложены разделы, относящиеся к интеллектуальным методам прогнозирования. Будут представлены алгоритмы экспоненциального смешивания экспертных прогнозов (как детерминированные, так и вероятностные), агрегирующий алгоритм В.Г.Вовка, алгоритм усиления классификаторов (бустинг). В последнее время в области интеллектуальных методов прогнозирования развивается применение теоретико-игровых методов, в курсе будет дано введение и в эти методы, в том числе будет изложено построение игр на рандомизированные калибруемые предсказания.

Все необходимые понятия будут пояснены, специальных знаний от слушателей не требуется.

Страница курса: https://lk.msu.ru/course/view?...

Список всех тем лекций

Лекция 1. Верификация алгоритмов вычисления суммы, корня и возведения в степень.
Вступление Методы искусственного интеллекта Верификация алгоритма вычисления суммы Верификация алгоритма, который по целому числу вычисляет корень Верификация алгоритма возведения первого числа в степень второго

Лекция 2. Верификация алгоритмов возведения в степень и сортировки массива.
Зачем нужна верификация программ Верификация алгоритма возведения первого числа в степень второго Верификация алгоритма сортировки пузырьком массива

Лекция 3. Верификация алгоритма сортировки массива.
Верификация алгоритма сортировки массива пузырьком Лексикографический порядок

Лекция 4. Верификация функциональной программы сортировки строки.
Программа сортировки строки Верификация программы сортировки строки

Лекция 5. Теория процессов.
Общий формат описания процесса Параллельная композиция двух процессов Блокировка взаимодействия по внутренним каналам для параллельной композиции

Лекция 6. Теория процессов для конфиденциального обмена информацией.
Шифрование сообщений Задача аутентификации и ее верификация Задача голосования без посредника и её верификация

Лекция 7. Шифрование электронных платежей и model checking.
Система шифрования и атаки на неё Протоколы и схемы электронных платежей Model checking

Лекция 8. Прогнозирование в больших данных.
Анализ больших данных Weighted modelling algorithm

Лекция 9. Верификация алгоритмов с бинарными и численными потерями.
Верификация алгоритма предсказаний экспертов с бинарными ошибками Верификация алгоритма предсказаний экспертов с численными потерями

Лекция 10. Усиление алгоритмов машинного обучения.
Алгоритм boosting Доказательство алгоритма boosting

Лекция 11. Алгоритмы следования за лидером.
Алгоритм следования за лидером Алгоритм следования за возмущённым лидером и его верификация Принятие решений в условиях неопределённости

Лекция 12. Метод опорных векторов.
Задача построения классификатора Алгоритм Розенблатта

Лекция 13. Агрегирующий алгоритм и теоретико-игровые методы.
Агрегирующий алгоритм Вовка Матричная игра с чистыми стратегиями Матричная игра со смешанными стратегиями