Artificial intelligence methods in data analysis and program verification tasks

ABOUT THE COURSE
ACADEMIC STAFF
  • ABOUT THE COURSE
  • ACADEMIC STAFF

The course focuses on a current area of mathematics and information technology: the application of artificial intelligence methods to data analysis and program verification tasks.

 

The course will cover logical formalisms related to conducting intelligent reasoning about the correctness of programs, and will provide various illustrations of such reasoning for different classes of programs and protocols — including parallel and distributed programs and cryptographic protocols. Model checking of program models is linked to other approaches, such as constructing program transition diagrams (Kripke models), which represent large graphs and often require simplification to compact probabilistic automaton models to achieve acceptable analysis complexity. The course will include an introduction to probabilistic automaton models based on the author’s work on probabilistic automata. An important part of deductive verification theory is the area of modeling and verifying cryptographic protocols; the course will present an introduction to the author’s new methods for the intelligent analysis of cryptographic protocols. The course will also cover sections related to intelligent forecasting methods. Algorithms for exponential mixing of expert forecasts (both deterministic and probabilistic), V. G. Vovk’s aggregating algorithm, and the classifier boosting algorithm will be presented. Recently, game‑theoretic methods have been developing in the field of intelligent forecasting techniques; the course will provide an introduction to these methods as well, including the construction of games for randomized calibrated predictions.

 

Upon completing the course, students will gain knowledge in applying artificial intelligence methods to solve program verification and data analysis tasks.

 

To take the course, students must have knowledge of mathematical logic, linear algebra, and discrete mathematics.

 

Topics covered in the course

1. Overview of the main areas of artificial intelligence. Intelligent methods for automating logical reasoning. Intelligent methods for program specification and verification. Intelligent data analysis. Main problems in machine learning and forecasting theory.

2. Main challenges in program verification. Models of sequential programs. Program flowcharts. Deductive verification of programs based on Floyd’s method.

3. Process models of parallel programs. Deductive verification of parallel programs.

4. Deductive verification of data transmission protocols.

5. Deductive verification of cryptographic protocols.

6. Program verification using the model checking method.

7. Main approaches to solving data classification tasks.

8. Support vector method.

9. Time series forecasting using the weighted majority algorithm.

10. Algorithm for optimal loss distribution.

11. Time series forecasting algorithm based on the Follow the Perturbed Leader approach.

12. Boosting method for strengthening weak classifiers.

13. Algorithms for exponential mixing of expert forecasts.

14. V. G. Vovk’s aggregating algorithm.

15. Introduction to game theory. Construction of games with randomized calibrated predictions.

 

Reading list

Core literature

1.1. Mironov A. M. Mathematical Models and Methods for Process Verification. MAX Press, Moscow, ISBN 978‑5‑317‑06893‑6, 104 pp., 2022.

1.2. Mironov A. M. Program Verification: Part 1: Non‑recursive Programs. MAX Press, Moscow, ISBN 978‑5‑317‑05721‑3, 76 pp., 2017.

1.3. Mironov A. M. Theory of Functional Programs. IPI RAS Publishing, Moscow, ISBN 978‑5‑91993‑024‑2, 160 pp., 2013.

1.4. Vyugin V. V. Mathematical Foundations of Machine Learning and Forecasting. MCCME, Moscow, 384 pp., 2018.

Additional literature

2.1. Mironov A. M. Program Verification Using the Model Checking Method. MAX Press, Moscow, ISBN 978‑5‑317‑06514‑0, 74 pp., 2020.

2.2. Mironov A. M. Machine Learning, Part 1. MAX Press, Moscow, ISBN 978‑5‑317‑06012‑1, 90 pp., 2018.

 

Classes are held at the Main Building of Lomonosov Moscow State University

The course program includes 25 sessions: 13 lectures and 12 practical sessions

 

Telegram

Teachers:

  • Andrey A. Mironov

    • Education

      PhD Candidate of Physico-mathematical Sciences
      MSU

    • Занятия проводятся в Главном Здании МГУ им. М. В. Ломоносова

    В программе курса 25 занятий: 13 лекций и 12 практических занятий

    Старт курса: с 15 февраля 2023

    Лекции проходят по средам с 17:00 до 18:30 в ауд. 14-08, семинары - по четвергам с 18:30 по 20:00 в ауд. 13-03

     

    Студентам будут предлагаться домашние задания после каждого занятия.

     

    Запись на курс на сайте: https://lk.msu.ru/course

    Telegram

    Набор на курс 2023 года закрыт 

    ABOUT THE COURSE
    ACADEMIC STAFF
    Group НС201

    FRIDAYS

    09:00–10:30 — period 1

    10:40–12:10 — period 2

    12:10–13.00 — break

    13:00–14:30 — period 3

    14:40–16:10 — period 4

    Instructor: A. Ganichev

    Group НС202

    THURSDAYS

    09:00–10:30 — period 1

    10:40–12:10 — period 2

    12:10–13.00 — break

    13:00–14:30 — period 3

    14:40–16:10 — period 4

    Instructor: A. Marakulin

    Group НС203

    MONDAYS

    09:00–10:30 — period 1

    10:40–12:10 — period 2

    12:10–13.00 — break

    13:00–14:30 — period 3

    14:40–16:10 — period 4

    Instructor: D. Penzar

    Group НС204

    SATURDAYS

    09:00–10:30 — period 1

    10:40–12:10 — period 2

    12:10–13.00 — break

    13:00–14:30 — period 3

    14:40–16:10 — period 4

    Instructor: I. Konyushok