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

Три основных исторически сложившихся «провинции» страны Формальной Семантики Программ – это Операционная Семантика, Денотационная Семантика и Аксиоматическая Семантика. Приглашаю студентов, кто только начинает путешествие по этой стране, познакомиться с общедоступным путеводителем…

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