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

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

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

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