Computer Science Summer in Russia (CSSR)

June 24 - July 5, 2019

Список курсов школы
Введение в формальную семантику программ
Описание
Содержание
Требования
Преподаватель
Язык
Прошло почти полвека с того времени, когда Роберт Флойд опубликовал первую работу о том, как придать программам математически-корректную («формальную») семантику. Минуло двадцать лет с тех пор, как Давид Шмидт опубликовал статью "О необходимости популярной формальной семантики". За эти годы было разработано множество индивидуальных формальных семантик, но (как отмечал Д. Шмидт) научных экспертов по формальной семантике пока значительно больше, чем инженеров-программистов, которые ее используют. В то же время мы видим значительную активность в исследованиях по формальной семантике и ее приложениях.

Этот курс для тех, кто хочет понять, что такое «формальная семантика языков программирования». Поэтому он начинается со знакомством с типами формальной семантики на примере эзотерического языка программирования, продолжается построением формальных семантик для игрушечного (но уже не эзотерического) языка программирования, а заканчивается знакомством с современными вопросами, например – формальной семантикой указателей (в терминах исчисления алиасов Бертрана Мейера).

В этом курсе Вы сможете:

  • узнать зачем нужна формальная семантика программ
  • понять принципы операционной, денотационной и аксиоматической семантики
  • познакомиться с операционной, денотационной и аксиоматической семантикой игрушечного языка программирования
  • почувствовать, где возникают трудности при формализации семантики реальных языков программирования
  • познакомиться с примером проблемно-ориентированной формальной семантики (для указателей)
  • узнать об использовании разных формальных семантик в верификации программ
  • обсудить место формальной семантики программ в реальной программной инженерии, в том числе в разработке ПО для космических аппаратов
1. Введение во «Введение в формальную семантику…»

1.1. Что такое «семантика»?

1.2. Почему «формальная семантика»?

1.3. Операционная, денотационная и аксиоматическая семантика для эзотерического языка

2. Формальная семантика для игрушечного языка программирования

2.1. Типы данных и их семантика

2.2. Основной ингредиент – реализационная семантика

2.3. Структурная операционная семантика

2.4. Реляционная денотационная семантика

2.5. Аксиоматическая семантика

3. Семантика второго порядка

3.1. Что такое «логики высших порядков»?

3.2. Семантика второго порядка для эзотерического языка

3.3. Семантика слабейшего предусловия для игрушечного языка программирования

4. λ-исчисление и классическая денотационная семантика

4.1. Синтаксис, семантика и основные теоремы λ-исчисления (без типов)

4.2. Семантика игрушечного языка программирования с использованием λ-исчисления

5. Заключение: формальной семантики – основа математически-обоснованной верификации программ

5.1. Как формализовать «фичи», которых нет в игрушечном языке: исчисление алиасов для указателей

5.2. Формальная семантика в космосе – верификация в проекте Curiosity

6. Темы домашних лабораторных работ (опционально). Работа с эзотерическим языком программирования:

6.1. Реализация и визуализация операционной семантики языка.

6.2. Реализация и визуализация денотационной семантики.

6.3. Реализация и визуализация семантики второго порядка.

6.4. Реализация аксиоматической семантики.

6.5 Визуализация аксиоматической семантики.
Базовые навыки программирования,
основы теории множеств,
пропозициональной логики (синтаксис и таблицы истинности)
и первопорядковой логики (синтаксис и понятие модели)
Николай Шилов
Кандидат физико-математических наук, доцент АНО ВО «Университет Иннополис». Специалист в области теории программирования и прикладной логики.

Работал в Sydney University of Technology (Австралия), Nazarbayev University (Казахстан), University of Canterbury, Christchurch (Новая Зеландия), Korea Advanced Institute of Science and Technology, Chung-Ang University и Samsung Advanced Technology Training Institute (Южная Корея).

В настоящее время исследовательские интересы связаны с математическими основаниями формальных методов и их приложениями для анализа программных, информационных, распределенных и мультиагентных систем. Текущая работа связана с исследованиями по проекту «Платформенно-независимый подход к формальной спецификации и верификации стандартных математических функций».
Русский или английский, в зависимости от предпочтений слушателей
Введение в теорию языков программирования
Описание
Содержание
Требования
Преподаватель
Язык
Цель этого курса - познакомить слушателей с теорией языков программирования - одним из активно разрабатываемых разделов информатики. Мы начнём с элементарного введения в основные идеи, понятия, факты и инструменты теории, после чего разберем примеры актуальных исследований, связанных с языком программирования Haskell, результаты которых регулярно освещаются на важнейших конференциях в этой области: POPL (Principles of Programming Languages, Принципы языков программирования) и ICFP (International Conference on Functional Programming, Международная конференция по функциональному программированию).

Темы второй части курса будут излагаться в виде обзора, из которого слушатели получат базовое представление о применяемых методах исследований в теории языков программирования. Всем слушателям будет предоставлен подробный электронный конспект лекций и список литературы для более глубокого изучения.
  • Лямбда-исчисление как язык теории языков программирования. Правила вычисления. Программирование в лямбда-исчислении.

  • Простое типизированное лямбда-исчисление. Отношение и правила типизации. Классическая и конструктивная логика, соответствие Карри—Ховарда. Расширение простого типизированного лямбда-исчисления вдоль осей лямбда-куба Хенка Барендрегта.

  • Система интерактивного доказательства теорем Coq как инструмент исследований в теории языков программирования: быстрое введение.

  • Пример, часть 1: язык программирования Haskell и System FC (System F Жирара с алгебраическими типами данных и приведением типов).

  • Пример, часть 2: расширение языка Haskell (а) линейными стрелками и (б) зависимыми типами - как пример современных исследований в теории языков программирования.
Знания в области теории языков программирования не требуются, однако требуется владение инструментами дискретной математики (множества, отношения, доказательства методом индукции, булева алгебра, логические предикаты).

Знакомство с любым функциональным языком программирования (Haskell, OCaml, F#, Clojure) желательно, но не обязательно.
Виталий Брагилевский
Старший преподаватель кафедры информатики и вычислительного эксперимента Института математики, механики и компьютерных наук имени И.И. Воровича Южного федерального университета (Ростов-на-Дону), разработчик в JetBrains. Преподает лекции по функциональному программированию, теории вычислений и теории языков программирования.

Член комитета по стандартизации языка Haskell и член наблюдательного комитета компилятора GHC языка Haskell.

Перевёл на русский язык и редактировал переводы нескольких книг по языку Haskell и теории языков программирования. Автор книги "Haskell in Depth" (доступна в рамках программы раннего доступа издательства Manning Publications).
Русский
Cовременные технологии тестирования и верификации
Описание
Содержание
Требования
Lecturer
Язык
В этом курсе Вы познакомитесь с некоторыми современными промышленными и академическими инструментами тестирования и формальной верификации. Курс охватывает следующие методы в сфере тестирования:

  • разработка через тестирование (TDD),
  • разработка на основе поведенческой спецификации (BDD),
  • автоматическое создание модульных тестов с помощью MS Spec Explorer,
  • подход MS Code Contracts,

а также следующие методы верификации:

  • верификация методом проверки моделей с помощью Spin в среде iSpin;
  • написание контрактов для C-программ с помощью метода слабейшего предусловия (Weakest Precondition),
  • верификация кибер-физических систем и обзор примеров в системе автоматического доказательства KeYmaera.
Современные методы тестирования.

  • Triple-V : модель тестирования и верификации;
  • Разработка примера системы на основе подхода TDD;
  • Разработка примера системы на основе подхода BDD;
  • Spec Explorer в действии: генерация модульных тестов заданным автоматом поведения.

2. Формальная верификация в действии

  • Цель формальной верификации;
  • Проверка акторных систем и протоколов с помощью Spin;
  • Решение поисковых задач в Spin на примере: Ханойские башни;
  • Контрактное программирование MS Code Contracts.

3. Формальная верификация в действии (2)

  • Подход Weakest Precondition и проверка программ на C в Frama-C;
  • Кибер-физические системы (СPS): определение и вопросы верификации;
  • Введение в верификацию CPS: верификация систем из разных доменов.

  • Основы программирования на языке C и Java
  • Основы теории автоматов
  • Понимание метода модульного тестирования

Сергей Старолетов
Доцент АлтГТУ им. Ползунова, кандидат физико-математических наук, специалист в области моделирования и тестирования распределенных программных систем на основе автоматных мультиагентных моделей.

Имеет богатый опыт работы в программной индустрии. Автор книги "Основы тестирования и верификации программного обеспечения", изд-во Лань, 2018 г.
Русский
Введение в Проверку Моделей (Model Checking)
Описание
Содержание
Требования
Преподаватель
Язык
Проверка моделей — это метод для автоматической верификации соответствия модели системы и ее формальной спецификации. Он используется для проверки корректности программного обеспечения, оборудования и других параллельных и распределенных систем в отношении таких свойств, как свобода от блокировок, выполнение инвариантов и ответов на запросы и т. п. В методе проверки моделей обычно сравнивается конечная модель системы с ее спецификацией, выраженной в каком-либо формализме. Зачастую в качестве такого формализма выступает темпоральная логика.

В этом курсе мы рассмотрим базовые логики и алгоритмы проверки моделей, а также варианты метода для вероятностных моделей и моделей реального времени. Метод будет иллюстрироваться различными примерами. Будет предоставлен обзор программных инструментов проверки моделей, включая SPIN и PRISM.
  • Надежность и корректность программ и систем. Основы метода проверки модели. Моделирование систем: структура Крипке, логическое представление параллельных систем.

  • Временная логика CTLи LTL для спецификации систем. Типичные свойства систем и их спецификация.

  • Алгоритмы проверки модели для темпоральных логик CTL и LTL. Справедливость. Проверка вероятностных моделей. Системы реального времени.

  • Примеры задач проверки модели: анализ бизнес-процессов, планирование, коммуникационные и криптографические протоколы.

  • Обзор инструментов проверки моделей. SPIN и PRISM.
Базовые знания алгоритмов и структур данных,
а также математической логики на уровне бакалавра.
Наталья Гаранина
Старший научный сотрудник Института систем информатики им. А.П. Ершова, специалист в области логики и ее приложений для верификации мультиагентных систем, распределенных алгоритмов.

Работала в Университете Чун ан, Сеул, Южная Корея, участвовала в проекте Computal Европейского Союза по вычислимому анализу. Преподает курсы по формальным методам программной инженерии, в том числе методам верификации, в Новосибирском Государственном Университете.

Русский
Метод конечных контрмоделей (FCM) для верификации параметризованных систем и систем с бесконечным числом состояний
Описание
Содержание
Требования
Преподаватель
Язык
В этом курсе мы представим введение в концептуально простой, но в тоже время мощный и эффективный метод верификации систем с бесконечным числом состояний и параметризованных систем. Метод использует моделирование понятия достижимости между состояниями системы посредством выводимости (доказуемости) в классической логике первого порядка.

При таком моделировании чтобы продемонстрировать безопасное поведение системы, т.е. недостижимость опасных состояний, достаточно показать, что конкретная формула логики первого порядка не выводима. В описываемом методе решение задачи невыводимости поручается автоматической процедуре поиска контрмодели.

Мы изложим теоретические основания метода и обсудим многочисленные применения к задачам верификации, относящимся к

  • системам с ненадежными каналами связи,
  • протоколам для поддержки когерентности кэшей,
  • параметризованным массивам конечных автоматов,
  • слабым моделям памяти,
  • системам переписывания термов и задачам из популярной математики.

Далее мы покажем относительную полноту метода по отношению к любому другому методу, использующему регулярные инварианты. То есть, при достаточно общих предположениях, если безопасность системы/протокола может быть показана при помощи регулярных инвариантов, то она может быть показана и FCM-методом. Мы заметим, что с практической точки зрения FCМ-метод почти всегда оказывается быстрее известных альтернатив.
- Введение

  • Решение задач из занимательной математики методом FCM: задача о словах Фибоначчи и MU-головоломка.
  • Происхождение метода и ранние работы по верификации криптопротоколов.
  • Общие требования для кодирований в логике первого порядка, используемые в FCM-методе.

- FCM для решения различных классов верификационных проблем:

  • безопасность систем с ненадежными каналами;
  • параметризованные протоколы для поддержки когерентности кэшей;
  • системы переписывания термов и строк;
  • линейные системы автоматов и протоколы для взаимного исключения.


- Относительная полнота:
для доказательств свойств безопасности FCM-метод как минимум не хуже методов, основанных на регулярных инвариантах:

  • регулярная проверка моделей;
  • регулярная проверка древесных моделей;
  • пополнение древесных автоматов.

- Ограничения метода. Вопросы и задачи для будущих исследований.

  • Ограничения, связанные с регулярностью инвариантов;
  • Простые задачи, для которых метод не работает в принципе;
  • Задачи, для которых метод работает в теории, но очень медленно на практике;
  • Как улучшить метод? Открытые вопросы и задачи.
  • Основы классической логики первого порядка: формулы, интерпретации и модели.
  • Основы теории формальных языков: регулярные языки.
Алексей Лисица
Руководитель исследовательской группы по верификации департамента компьютерных наук университета г. Ливерпуль. Его исследования относятся к трем взаимосвязанным областям: методы автоматической верификации (в особенности для параметризованных систем и систем с бесконечным числом состояний); методы машинных рассуждений с приложениями к верификации и математике; методы компьютерной безопасности.

Автор более 100 научных работ. Алексей Лисица является председателем-учредителем и членом руководящего комитета серии семинаров VPT (Verification and Program Transformation), шесть выпусков которых проводились eжегодно в ассоциации с ключевыми конференциями CAV или ETAPS.

Алексей был приглашенным экспертом в проекте SC ^ 2, Horizon 2020 по проверке выполнимости (SAT solving) и символьным вычислениям. В настоящее время является руководителем совместного научно-индустриального проекта KTP (Партнерство по передаче знаний) по безопасной обработке данных и технологиям, основанным на блокчейне.

Русский или английский, в зависимости от предпочтений слушателей
Поддержка верификации систем автоматического управления на основе предметно-ориентированных языков
Описание
Содержание
Требования
Преподаватели
Язык
Во многих прикладных областях до сих пор отмечается нехватка логических средств верификации программного обеспечения. Например, разработка программ управления с использованием приложения Matlab-Simulink(R) использует симуляцию как основной метод тестирования. Но до сих пор нет общепринятых методов, которые могли бы гарантировать корректное поведение систем автоматического управления во всех состояниях.


С другой стороны, в последние 20 лет мы наблюдаем существенный прогресс в разработке специализированных формализмов, в том числе модальных логик, связанных с прикладными предметными областями. Методы машинного доказательства становятся все более эффективными и доступными даже для нестандартных логических формализмов. Однако решение задачи формализации предметной области в рамках той или иной логики по-прежнему остается ключевым этапом, который не допускает автоматизации и должен быть сделан «вручную».


В этом курсе Вы познакомитесь со средствами, которые призваны облегчить данный этап, и основаны на предметно-ориентированных языках (Domain-specific Languages, DSLs). DSLs представляют собой формализмы, достаточно выразительные для описания входов в широко распространенных форматах, используемыми инженерными средствами, такими как, например, Matlab-Simulink(R). Кроме того, их гибкость позволяет формулировать доказательства в рамках различных логических формализмов.


Данный курс основан на примере из области автоматического управления. Для начала мы попробуем описать корректную систему автоматического управления с помощью средства Matlab-Simulink(R), а затем перейдем к уточнению при помощи предметно-ориентированных языков. В качестве средства верификации системы управления будет использоваться системой автоматического доказательства KeYmaera.
- Основы логики

  • пропозициональная логика
  • логика первого порядка
  • динамическая логика

- Теория управления на примерах

  • производственная модель
  • контроллер
  • формализация средствами Matlab-Simulink(R)



- Современные средства обеспечения качества систем управления

  • симуляция

- Гибридные автоматы и реализация с помощью машины доказательства KeYmaera.

  • компактные примеры,
  • правила вывода (в том числе, для работы с обыкновенными дифференциальными уравнениями)

- Использование предметно-ориентированных языков для связи Matlab-Simulink(R) и гибридных автоматов

  • задание синтаксиса предметно-ориентированного языка с помощью XText
  • реализация генератора доказательств
  • визуализация результатов

- Модель резервуара как иллюстративный пример

  • базовые знания логики (пропорциональной, логики первого порядка или модальной логики)

  • знакомство с основными терминами из области парсинга (Lexer, Token, Abstract Syntax Tree, пр.)

  • знаний в теории управления не требуется

Томас Баар и Хайде Брандтштедтер
Томас Баар - выпускник Берлинского университета им. Гумбольдта, получил степень PhD в университете Карлсруэ (ныне Технологический институт Карлсруэ), Германия. С 2011 работает в должности профессора по специализации в инженерии ПО и баз данных в Университете прикладных технических и экономических наук, г. Берлин.

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

Хайде Брандтштедтер - выпускница Берлинского технического университета, получила степень PhD в Мюнхенском техническом университете. В 2008 присоединилась к лаборатории Сименс в Берлине, где занималась роторной динамикой крупноразмерных электрических агрегатов и торсионным анализом трансмиссии. С апреля 2018 г. работает в должности профессора в Университете прикладных технических и экономических наук, г. Берлин.

Научные интересы связаны с математическим моделированием динамических систем и теорией управления, в частности, управлением в скользящем режиме.
Английский
Современные принципы построения промышленных компиляторов
Описание
Содержание
Требования
Преподаватель
Язык
Построение компиляторов — одна из самых старых и зрелых областей информатики. Несмотря на долгую историю, начавшуюся в 1950-е годы, эта область постоянно изменяется и развивается. Классические учебники устаревают и не справляются с вопросом подготовки студентов и практикующих специалистов к решению научно-исследовательских и промышленных задач.

Данный краткий курс углублённого изучения компиляторов дополняет традиционные бакалаврские или магистерские лекции по компиляции и эволюции программного обеспечения примерами задач в области компиляции языков четвёртого поколения и предметно-ориентированных языков, модернизации устаревших систем, обратной разработки и т. п. Лекции данного курса основаны на опыте преподавания в ведущих европейских вузах, научном руководстве магистрантами и работе в компании Raincode Labs - крупнейшем в мире независимом производителе промышленных компиляторов.

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

На первой лекции мы поищем примеры окружающих нас программных языков и компиляторов, сместив акцент с традиционного системного программного обеспечения на предметно-ориентированные пакеты и «языковые верстаки». Также мы кратко обсудим конкретные инструменты, облегчающие жизнь несистемным программистам, желающим просто автоматизировать рутинные и хрупкие задачи обработки конфигурационных файлов или манипуляции данных в XML, JSON и подобных форматах.

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

На последней лекции будут рассмотрены несколько недостаточно проработанных вопросов, которые будут интересны студентам и аспирантам, ищущим тему для исследований.
• Будущее компиляторов и грамматическое обеспечение

• Языковые «верстаки» и прочий мощный инструментарий

• Предметно-ориентированные языки и четвёртое поколение

• Проектирование программных языков как новая область

• Умышленная разработка языков

• Современные алгоритмы разбора: GLL, ALL(*), SGLR, Packrat

• Полуразбор, восстановление от ошибок, изящная деградация

• Разбор в широком смысле

• Извлечение и восстановление грамматик

• Качество грамматик и грамматики с душком

• Эквивалентность и сходимость грамматик

• Кодогенерация с помощью соответствующих библиотек

• Двунаправленные и связанные преобразования

• Семантики и интерпретация

• Метапрограммирование, анализ и понимание

• Между интерпретацией и компиляцией

• Тестирование компиляторов и техника размытия

• Языковая документация

• Внедрение и интеграция компиляторов

• Место машинного обучения в построении компиляторов

• Нерешённые проблемы будущего

Наличие степени бакалавра по информатике,
либо знание основ построения компиляторов/формальных языков на уровне отдельного пройденного курса.
Вадим Зайцев
Заместитель директора по науке в бельгийской компании Raincode Labs, занимающейся предоставлением услуг по разработке и поддержке компиляторов, а также консультациями по связанными с этим вопросам.

Защитил кандидатскую диссертацию в Свободном университете Амстердама по направлению языковой инжинерии и грамматических технологий. Над этой темой он также работал в немецком Университете Кобленца-Ландау, нидерландском Центре математики и информатики и в Университете Амстердама, где также был активно вовлечён в учебный процесс, осуществлял научное руководство, поддерживал и расширял связи университета с индустрией.

Интересы и научная активность сосредоточены вокруг таких тем, как оценка качества программного обеспечения, анализ и трансформации программного кода, моделирование, метамоделирование и мегамоделирование, парадигмы программирования, декларативное и функциональное программирование, поддержка и обновление устаревших систем.
Русский или английский, в зависимости от предпочтений слушателей
Лекция компании Uma.Tech: Data Science и продуктовая разработка
Описание
Содержание
Требования
Преподаватель
Язык
Во время лекции мы расскажем вам о самом интересном и актуальном, а именно:


- О компании Uma.Tech;

- Раскроем тему продуктовой разработки и того, как Data Science помогает в создании новых продуктов;

- Рассмотрим популярную методологию CRISP-DM;

- Решим реальную задачу прогнозирования оттока пользователей на основе предложенной схемы процесса;

- Предложим к выполнению "домашнее задание".


- О компании Uma.Tech;

- Раскроем тему продуктовой разработки и того, как Data Science помогает в создании новых продуктов;

- Рассмотрим популярную методологию CRISP-DM;

- Решим реальную задачу прогнозирования оттока пользователей на основе предложенной схемы процесса;

- Предложим к выполнению "домашнее задание".

нет специальных требований
Станислав Гафаров
Руководитель Отдела анализа данных компании Uma.Tech. Станислав занимается анализом данных и внедрением методов машинного обучения более 3,5 лет. На данный момент управляет группой специалистов в компании Uma.Tech, которая внедряет модели машинного обучения, разрабатывает рекомендательные системы и занимается вопросами Computer Vision.
Русский
Логические методы инженерии онтологий
Описание
Содержание
Требования
Преподаватель
Язык
Практически каждая предметная область характерна богатыми системами терминов, которые используются специалистами в формальном и неформальном виде для документирования полученных знаний. В этой связи возникает и необходимость документирования терминов. Так, например, были развиты классификации в биологии и химии, своды специализированных терминологических систем в виде глоссариев, тезаурусов, таксономий и онтологий, представляющие определения терминов и взаимосвязей между ними.


Как правило, специализированные технические тексты, например, документация или спецификация технических узлов и агрегатов, опирается на богатую терминологию, которая включается в документацию в виде глоссария. Некоторые своды терминов являются стандартами на государственном или высшем профессиональном уровне, например, Общероссийский Классификатор Видов Экономической Деятельности, Международная Классификация Болезней и многие другие.


Формализованные терминологии применяются в информационных системах для решения задач аннотирования, поиска, интеграции информации, анализа текстов на естественном языке. На сегодняшний день в сети Интернет доступны сотни математически формализованных терминологических систем, которые используются для решения информационных задач, в естественнонаучных и технических предметных областях.


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

- Моделирование терминологических систем на основе логических методов
  • Обоснование применения логики для формализации онтологий.
  • Основания дескрипционных логик. Синтаксис и семантика логик EL и ALC.
  • Базовые проблемы логического следования: проблема непротиворечивости терминологической системы, невырожденности термина, дизъюнктности терминов.
  • Задача классификации терминов. Терминологии и развертывание терминологических определений.

- Методы машинных рассуждений в дескрипционных логиках
  • Сложность логического вывода в логике EL, сложность проверки невырожденности термина в логике ALC относительно пустой/непустой онтологии.
  • Взаимосвязь выразительных средств логик со сложностью вывода.
  • Метод прямого вывода для логики EL. Табличный метод для ALC.

- Объяснение свойств терминологических систем с помощью машинных рассуждений.
  • Проблема объяснения противоречий. Минимальные причины логических следствий и максимальные опровержения.
  • Число минимальных причин для следствия терминологической системы в логике EL, сложность проблемы поиска причины заданной мощности.
  • Glass-box подход к поиску причин на основе модификации алгоритма вывода. Вычисление минимальных причин для следствий в логике EL с помощью решения задачи SAT (выполнимости булевых формул).
  • Поиск минимальных причин с помощью модификации метода табло для логики ALC.
  • Black-box подход к поиску причин без модификации алгоритма вывода.

- Вычисление определений терминов в онтологиях
  • Явные и неявные определения термина.
  • Оценка числа и длины попарно несравнимых, кратчайших определений термина в логиках EL и ALC. Связь явных определений с минимальными причинами.
  • Построение явных определений терминов из машинных доказательств.
  • Вычисление явных определений терминов на основе модификации метода прямого вывода для логики EL.
  • Переписывание терминологической системы с помощью явных определений.
Базовые знания любой формальной логики (синтаксис и семантика)
Денис Пономарев
Старший научный сотрудник Института Систем Информатики им. А.П. Ершова и старший преподаватель Новосибиирского государственного университета. Работал в качестве приглашенного профессора и старшего научного сотрудника на факультете информатики Университета Райерсона, Торонто, и в Институте Искусственного Интеллекта при Университете г. Ульм, Германия.

Рецензент журнала ACM «Transactions on Computational Logic» и член программных комитетов ведущих конференций по тематике Искусственного Интеллекта, включая AAAI и IJCAI, а также международного воркшопа по дескрипционным логикам и других конференций близкой тематики.

Основные научные интересы: методы представления знаний, машинных рассуждений и доказательств, инженерия онтологий, методы рассуждения о действиях.
Русский или английский, в зависимости от предпочтений слушателей
Доступ к данным на основе онтологий
Описание
Содержание
Требования
Преподаватель
Язык
Доступ к данным на основе онтологий (ДДОО) считается ключевым ингредиентом информационных систем нового поколения.

В парадигме ДДОО онтология задает глобальную схему высокого уровня над уже существующими источниками данных и предоставляет словарь для пользовательских запросов. Система ДДОО переписывает такие запросы с учетом онтологии в словарь
источников данных, а затем делегирует вычисление ответа на запрос к реляционной СУБД.

В этом курсе Вы познакомитесь с идеями и технологиями, которые лежат в основе ДДОО: RDF-графы, SPARQL-запросы, связанные данные, логики для представления и описания знаний.

Мы сосредоточимся на ДДОО на основе языка OWL 2 QL - одного из трех профилей стандарта описания Веб-онтологий и реляционных баз данных. В заключение мы проведем практическое занятие с системой OnTop, которая реализует доступ к данным на основе онтологий.
  • RDF-графы и SPARQL-запросы.
  • Языки для Веб-онтологий, базы знаний
  • Реляционные базы данных как виртуальные RDF-графы
  • Онтологический доступ к данным через переформулировку запросов в OWL 2 QL
  • Двухмерная классификация онтологических запросов
  • Сложность ответов на конъюнктивные запросы относительно онтологий
  • Размер переписываний конъюнктивных запросов в OWL 2 QL
  • Онтологический доступ к данным с помощью OnTop
Для курса нет жестких требований. Однако студенты, знакомые с формальной логикой и принципами работы реляционных баз данных будут чувствовать себя более комфортно.

Базовые навыки работы с SQL и редактором онтологий Protege поможет в практической части курса.
Станислав Кикоть
Специалист в области логики и ее приложений в инженерии данных и знаний.

После окончания мехмата МГУ защитил диссертацию по теории соответствия в модальной логике. Затем после стажировки в Яндексе работал в должности научного сотрудника в Лондонском университете над фундаментальными проблемами доступа к данным на основе онтологий.

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


Реализация логических методов, в частности методов машинных рассуждений, исторически идет от самого начала компьютерной эры. Так, например, один из первых языков программирования высокого уровня - Lisp - можно считать компьютерной реализацией лямбда-исчисления.


В дальнейшем применение логики в информационных технологиях претерпевало взлеты и падения, но сейчас это направление - использование дедуктивного вывода в информационных технологиях - находится на новом витке подьема, связанном с применением в верификации программ, протоколов и систем, представлении и анализе знаний и обработке данных. В последние годы разработано множество систем, реализующие машинные рассуждения для решения этих задач.
  • Дедуктивные исчисления на примере логики предикатов: синтаксис и семантика. Проблема алгоритмического поиска логического вывода.

  • Применение машинных рассуждений на примере верификации программ.

  • Методы поиска доказательств: сведение к более простому языку, метод резолюций, табличный метод.

  • Применение теории типов для автоматизации поиска доказательств.

  • Перспективы: применение машинного обучения для поиска доказательств.
Основы дискретной математики: множества, отношения, доказательства методом индукции, булева алгебра, логические предикаты.

Также требуется понимание того, что такое императивная программа.
Дмитрий Власов
Старший преподаватель кафедр общей информатики и систем информатики Новосибирского государственного университета. Читает лекции по дискретной математике, математической логике и теории языков программирования.

Автор языка и программной реализации Russell - системы, предназначенной для представления формальных дедуктивных систем и машинных рассуждений в них.
Русский, слайды лекций на английском
Описание
Содержание
Требования
Преподаватель
Язык
В данном курсе Вы познакомитесь с рядом интересных приложений методов машинных рассуждений (МР).

Будут представлены недавние продвижения и результаты в таких приложениях как автоматическое доказательство и опровержение теорем и методы решения задач выполнимости (SAT solving), в экспериментальной математике.

В частности, мы рассмотрим приложения МР в вычислительной топологии (теории узлов), комбинаторной теории чисел и комбинаторной теории групп.
- В первой части курса будут представлены недавние приложения АР к классической задаче вычислительной топологии по распознаванию узлов.

  • Мы покажем, что такая задача может быть сведена к задаче доказательства/опровержения формулы логики первого порядка, которая описывает свойства алгебраической структуры (quandle), связанной c диаграммой узла.

  • Далее мы используем существующие методы автоматического доказательства теорем, чтобы продемонстрировать тривиальность узла, и методы автоматического опровержения через построение контрмоделей, чтобы показать нетривальность узла.

  • Мы далее покажем, что метод может быть улучшен с использованием вычисленных заранее алгебраических структур. В этом случае, задача распознавания нетривиальных узлов может быть сведена к задаче выполнимости пропозициональных формул (SATsolving), которая в свою очередь может быть быстро решена существующими решателями (SAT solvers). Этот подход представляет собой наиболее практически эффективный метод распознавания узлов.

  • Затем мы обсудим использование других алгебраических структур (например, полугрупп и групп) и топологических объектов (tangles) в машинных рассуждениях об узлах. Одни из этих структур приводят к более быстрым, а другие - к более прозрачным рассуждениям.

- Во второй части курса мы сделаем обзор результатов, относящихся к проблеме несоответствия Эрдёша ( Erdos Discrepancy Problem, EDP).

  • В 1930s Пол Эрдёш предположил, что для любого положительного целого числа C в любой бесконечной последовательности (x_n), состоящей из чисел 1 и -1 найдется подпоследовательность x_d, x_{2d}, x_{3d}, …, x_{kd} для некоторых чисел k и d, такая, что абсолютная величина суммы всех элементов этой подпоследовательности превосходит C. Это гипотеза со временем стала одной из главных открытых проблем в комбинаторной теории чисел.

  • Случай С=1 легко доказать методом перебора. Случай C=2 оставался открытым до марта 2014. Мы покажем, что, используя кодирование этой задачи как задачи булевской выполнимости и используя решатель выполнимости (SAT solver) можно доказать EDP для случая C=2. Эти результаты были опубликованы в 2014-2015. После этого осенью 2015 Теренс Тао доказал общий случай EDP, не используя ни методы машинных рассуждений, ни какие-либо другие вычислительные методы.

- В третьей части курса мы предстaвим приложения методов автоматического доказательств теорем для исследования открытой гипотезы Эдрюса-Куртиса из комбинаторной теории групп.

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


Менее классические понятия (quandles, tangles, т.д.) будут определены по ходу курса и должны быть доступны для людей с математическими интересами
Alexei Lisitsa
Руководитель исследовательской группы по верификации департамента компьютерных наук университета г. Ливерпуль. Его исследования относятся к трем взаимосвязанным областям: методы автоматической верификации (в особенности для параметризованных систем и систем с бесконечным числом состояний); методы машинных рассуждений с приложениями к верификации и математике; методы компьютерной безопасности.

Автор более 100 научных работ. Алексей Лисица является председателем-учредителем и членом руководящего комитета серии семинаров VPT (Verification and Program Transformation), шесть выпусков которых проводились eжегодно в ассоциации с ключевыми конференциями CAV или ETAPS.

Алексей был приглашенным экспертом в проекте SC ^ 2, Horizon 2020 по проверке выполнимости (SAT solving) и символьным вычислениям. В настоящее время является руководителем совместного научно-индустриального проекта KTP (Партнерство по передаче знаний) по безопасной обработке данных и технологиям, основанным на блокчейне.
Русский или английский, в зависимости от предпочтений слушателей
Описание
Содержание
Требования
Преподаватель
Язык
Данный курс представляет краткий обзор истории развития и текущие достижения в области машинного обучения. Практическая часть курса содержит работу с популярными инструментами, средами и рабочими процессами глубокого обучения для создания и развертывания моделей нейронных сетей на полностью сконфигурированной рабочей станции с ускорением на GPU в облаке.

После быстрого знакомства с основами глубокого обучения мы перейдем к приложению для классификации изображений и обнаружения объектов. Затем мы перейдем к модификации нейронных сетей, чтобы повысить их точность и производительность, и завершим созданием прототипа рабочего процесса / проекта, интегрирующего машинное обучение и классическое программирование. По окончании семинара у Вас будет доступ к дополнительным ресурсам для самостоятельного создания новых приложений с использованием GPU.


После успешного завершения этого курса Вы получите сертификат NVIDIA DLI о прохождении.

  • Организация процессов глубокого обучения, таких как классификация изображений и обнаружение объектов.

  • Эксперименты с данными, параметрами обучения, структурой сети и другими стратегиями для увеличения производительности и возможностей нейронных сетей

  • Интеграция и развертывание нейронных сетей в реальных приложениях
Знакомство с основами программирования, такими как функции и переменные.
Николай Толстокулаков
Специалист в области высоконагруженных распределенных систем и глубокого обучения. Преподает курсы по данным направлениям в Новосибирском Государственном Университете и является представителем NVIDIA Deep Learning Institute в НГУ.

Имеет богатый опыт работы в промышленных проектах с использованием данных технологий. Примером одного их проектов является система умного паркинга http://green-pay.ru
Русский или английский, в зависимости от предпочтений слушателей
Описание
Содержание
Требования
Преподаватель
Язык
В курсе будет рассказано про уникальный метод машинного обучения, который был разработан в Новосибирском Академгородке и зарекомендовал себя при решении множества практических задач.

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

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


В заключительной части курса будут рассмотрена проблематика управления гиперизбыточными робототехническими системами и модульными роботами.
  • Знакомство с логико-вероятностным методом извлечения знаний из данных.

  • Практическое применение метода для извлечения знаний и прогнозирования в различных областях.

  • Иерархические системы управления на основе современных нейрофизиологических теорий работы мозга.

  • Управление гиперизбыточными системами и модульными роботами.

Знакомство с основными понятиями математической логики и статистики, такие как предикат, конъюнкция, булевы операции, вероятность.
Александр Демин
Специалист в области анализа данных и адаптивного управления. Работает в Институте систем информатики им. А.П. Ершова в тесном сотрудничестве с Лабораторией теории вычислимости и прикладной логики Института математики С.Л. Соболева.


Имеет практический опыт разработки систем извлечения знаний и прогнозирования в различных областях, включая медицину, финансы и биоинформатику. Занимается исследованиями в области создания интеллектуальных самообучающихся робототехнических систем.
Русский