Кондратьев Дмитрий Александрович, к.ф.-м.н., Институт систем информатики им. А. П. Ершова СО РАН (научный сотрудник), Новосибирский Государственный Университет (ассистент)
Дедуктивная верификация нейронных сетей (продолжение).
Архив семинара
Кондратьев Дмитрий Александрович, к.ф.-м.н., Институт систем информатики им. А. П. Ершова СО РАН (научный сотрудник), Новосибирский Государственный Университет (ассистент)
Дедуктивная верификация нейронных сетей (продолжение).
Аннотация
В настоящее время искусственный интеллект, основанный на нейронных сетях, стал активно применяться в программном обеспечении систем, к надежности и корректности которых предъявляются повышенные требования. В качестве примера таких систем можно привести беспилотные авиационные системы, беспилотные транспортные системы, роботизированные системы, экспертные системы в банковской сфере и т.д. Традиционно для проверки корректности и надежности программного обеспечения применяется тестирование. Но известно, что тестирование не может гарантировать корректность программ. Это может сделать только формальная верификация, которая позволяет формально доказать, что программа корректна относительно своих спецификаций. Для проверки корректности программы относительно формальных спецификаций, описывающих результат ее исполнения, применяется такой вид формальной верификации, как дедуктивная верификация. Дедуктивную верификацию можно применить и к нейронным сетям, чтобы сделать основанный на них искусственный интеллект доверенным. В отличие от тематики дедуктивной верификации программного обеспечения общего назначения, тематика дедуктивной верификации нейронных сетей начала активно развиваться относительно недавно. Итого, проблема дедуктивной верификации систем искусственного интеллекта, основанных на нейронных сетях, является актуальной. В данном докладе будет дан обзор новейших зарубежных исследований в области дедуктивной верификации нейронных сетей. Также в данном докладе будет рассмотрен наш проект исследования по созданию комплексного подхода к формальной верификации систем искусственного интеллекта, основанных на нейронных сетях, преимущества нашего проекта перед новейшими зарубежными исследованиями и перспективы данного проекта.Кондратьев Дмитрий Александрович, к.ф.-м.н., Институт систем информатики им. А. П. Ершова СО РАН (научный сотрудник), Новосибирский Государственный Университет (ассистент)
Дедуктивная верификация нейронных сетей.
Аннотация
В настоящее время искусственный интеллект, основанный на нейронных сетях, стал активно применяться в программном обеспечении систем, к надежности и корректности которых предъявляются повышенные требования. В качестве примера таких систем можно привести беспилотные авиационные системы, беспилотные транспортные системы, роботизированные системы, экспертные системы в банковской сфере и т.д. Традиционно для проверки корректности и надежности программного обеспечения применяется тестирование. Но известно, что тестирование не может гарантировать корректность программ. Это может сделать только формальная верификация, которая позволяет формально доказать, что программа корректна относительно своих спецификаций. Для проверки корректности программы относительно формальных спецификаций, описывающих результат ее исполнения, применяется такой вид формальной верификации, как дедуктивная верификация. Дедуктивную верификацию можно применить и к нейронным сетям, чтобы сделать основанный на них искусственный интеллект доверенным. В отличие от тематики дедуктивной верификации программного обеспечения общего назначения, тематика дедуктивной верификации нейронных сетей начала активно развиваться относительно недавно. Итого, проблема дедуктивной верификации систем искусственного интеллекта, основанных на нейронных сетях, является актуальной. В данном докладе будет дан обзор новейших зарубежных исследований в области дедуктивной верификации нейронных сетей. Также в данном докладе будет рассмотрен наш проект исследования по созданию комплексного подхода к формальной верификации систем искусственного интеллекта, основанных на нейронных сетях, преимущества нашего проекта перед новейшими зарубежными исследованиями и перспективы данного проекта.Новиков Сергей, 4 курс ММФ (научный руководитель Нечесов А. В.)
AlphaGeometry: как ИИ-система от DeepMind побеждает на международных олимпиадах.
Аннотация
Поговорим о нашумевшей AI-системе AlphaGeometry от Google DeepMind. Будет частично прореферирована статья: DeepMind AI solved geometry problems at star-student level. (David Castelvecchi).
P.S.: После планируется живая дискуссия и анализ применимости наших методов в решении таких задач.
Бурдуков Александр Николаевич (независимый исследователь, математик, программист)
Метамоделирование как общий подход разработки и генерации моделей в любых предметных областях. AGI как приложение метамодельного подхода.
Аннотация
Моя цель описать в общем виде круг идей и подход в основе которого положено метамоделирование.
Задачи:
- заинтересовать профильных специалистов в развитии концепции и перспективе направления.
- показать, что данный универсальный подход позволяет системно отвечать и решать все проблемы связанные с AGI.
Роман Потемин, DS в Сбер, студент 4 курса ММФ НГУ, н.р. И. Ю. Бондаренко
Named Entity Recognition: прикладные задачи и исследования (продолжение).
Аннотация
Распознавание именованных сущностей (NER). Постановка задачи: плоские и вложенные сущности, мультиязычные задачи, задачи с «грубым» и «подробным» уровнем сущностей. Описаны прикладные задачи и их решения, последние результаты исследований (SOTA). Приведены результаты решения задачи в разных постановках с помощью больших языковых моделей (LLM, gpt-like модели) + исследование докладчика.
Дополнительно (по необходимости в ходе доклада)
Теоретический минимум по трансформерам, задачи оптимизации, LoRA.
Роман Потемин, DS в Сбер, студент 4 курса ММФ НГУ, н.р. И. Ю. Бондаренко
Named Entity Recognition: прикладные задачи и исследования.
Аннотация
Распознавание именованных сущностей (NER). Постановка задачи: плоские и вложенные сущности, мультиязычные задачи, задачи с «грубым» и «подробным» уровнем сущностей. Описаны прикладные задачи и их решения, последние результаты исследований (SOTA). Приведены результаты решения задачи в разных постановках с помощью больших языковых моделей (LLM, gpt-like модели) + исследование докладчика.
Дополнительно (по необходимости в ходе доклада)
Теоретический минимум по трансформерам, задачи оптимизации, LoRA.
Информация о семинаре
Руководители:
акад. С. С. Гончаров, к.ф.-м.н А. В. Нечесов
Время и место проведения:
Среда, 18.10 ч., ауд. 5273, новый корпус НГУ
