Название спецкурса на английском языке
Artificial Intelligence Methods in Data Analysis and Program Verification
Аннотация
Курс посвящен изложению актуального раздела математики и информационных технологий — применению методов искусственного интеллекта в задачах анализа данных и верификации программ.
Область верификации программ традиционно подразделяется на два направления: дедуктивную верификацию и анализ моделей программ (model checking). Дедуктивная верификация связана с построением математических доказательств теорем о том, что анализируемые программы обладают заданными свойствами. Задачи построения математических доказательств формальных утверждений относятся к классическим задачам искусственного интеллекта — автоматизации логических рассуждений. В курсе будут излагаться логические формализмы, связанные с проведением интеллектуальных рассуждений о правильности программ, и будут даны различные иллюстрации проведения интеллектуальных рассуждений для различных классов программ и протоколов, в том числе для параллельных и распределенных программ и криптографических протоколов.
Также в курсе будут изложены разделы, относящиеся к интеллектуальным методам прогнозирования. Будут представлены алгоритмы экспоненциального смешивания экспертных прогнозов (как детерминированные, так и вероятностные), агрегирующий алгоритм В.Г.Вовка, алгоритм усиления классификаторов (бустинг). В последнее время в области интеллектуальных методов прогнозирования развивается применение теоретико-игровых методов, в курсе будет дано введение и в эти методы, в том числе будет изложено построение игр на рандомизированные калибруемые предсказания.
Все необходимые понятия будут пояснены, специальных знаний от слушателей не требуется.
Область верификации программ традиционно подразделяется на два направления: дедуктивную верификацию и анализ моделей программ (model checking). Дедуктивная верификация связана с построением математических доказательств теорем о том, что анализируемые программы обладают заданными свойствами. Задачи построения математических доказательств формальных утверждений относятся к классическим задачам искусственного интеллекта — автоматизации логических рассуждений. В курсе будут излагаться логические формализмы, связанные с проведением интеллектуальных рассуждений о правильности программ, и будут даны различные иллюстрации проведения интеллектуальных рассуждений для различных классов программ и протоколов, в том числе для параллельных и распределенных программ и криптографических протоколов.
Также в курсе будут изложены разделы, относящиеся к интеллектуальным методам прогнозирования. Будут представлены алгоритмы экспоненциального смешивания экспертных прогнозов (как детерминированные, так и вероятностные), агрегирующий алгоритм В.Г.Вовка, алгоритм усиления классификаторов (бустинг). В последнее время в области интеллектуальных методов прогнозирования развивается применение теоретико-игровых методов, в курсе будет дано введение и в эти методы, в том числе будет изложено построение игр на рандомизированные калибруемые предсказания.
Все необходимые понятия будут пояснены, специальных знаний от слушателей не требуется.
Подразделение
[Кафедра МаТИС]
Семестр
Полгода (весна)
Тип курса
Спецкурс по выбору студента
Учебный год
2023/24
Целевая аудитория
1 курс
Дополнительная информация
Ауд 13-06. Первое занятие - 7 февраля.
День недели
среда
Время
15:00-16:35
Аудитория
1306