Студенческая смена по математике и компьютерным наукам от факультета МКН СПбГУ в Сириусе
Проектная студенческая смена по математике и компьютерным наукам от факультета МКН СПбГУ состоится в Университете Сириус в Сочи с 24 марта по 03 апреля!
Приглашаем заинтересованных студентов третьего и четвёртого курса бакалавриата поработать над фундаментальными и прикладными проектами вместе с преподавателями факультета математики и компьютерных наук СПбГУ. Таких проектов будет шесть:
Машинное обучение
Минимальные бивогнутые функции
Поиск булевых схем
Верификация
Теория узлов и кос
Алгоритмы и структуры данных в операционных системах
Отбор организован через курс на Stepik-е.
Машинное обучение
Мы живём в период расцвета машинного обучения, являясь свидетелями ежегодных прорывов в этой области. Как же познакомиться с ней, чтобы на приличном уровне понимать происходящее? С одной стороны в сети полно видеолекций и публикаций на любой вкус, с другой — как невозможно научиться плавать по книгам, так и машинное обучение нельзя освоить без практической реализации моделей. При этом тестирование и проверка работ студентов всегда является «узким» местом любого учебного курса.
В предлагаемом проекте мы сначала познакомимся с избранными методами машинного обучения (см. например, курс на МКН СПбГУ), после чего будем разрабатывать и реализовывать удобную расширяемую систему автоматически проверяемых заданий на практическую реализацию пройденных методов на Python.
Верификация
Формальная верификация программ — это набор парадигм, техник и инструментов, гарантирующих с той или иной степенью надёжности корректность программ. Думаю, многие согласятся, что есть области ИТ, в которых корректность заслуживает самого пристального внимания: прошивки бортовых компьютеров самолетов, автомобилей, кардиостимуляторов, софт атомных электростанций и др.
Формальная верификация — это большая область, которую невозможно покрыть в одном курсе сколько-нибудь глубоко, поэтому нашей целью будет система интерактивного доказательства теорем Coq, теория типов, лежащей в ее основе, метапрограммирование в Coq и применение Coq к верификации (простых) компиляторов.
Алгоритмы и структуры данных в операционных системах
Операционные системы являются одним из важнейших потребителей эффективных по времени и памяти алгоритмов и структур данных, поскольку нужно, чтобы компоненты операционных систем работали быстро, потребляя при этом минимум ресурсов. В этом курсе мы посмотрим на принципы реализации самых важных компонентов современных операционных систем, таких как управление памятью и процессами, организация ввод-вывода, файловые системы, виртуализация, а затем в рамках проектов реализуем их прототипы и сравним разные подходы между собой.
Поиск булевых схем
Булева схема — это одна из простейших моделей вычисления для булевых функций. В этой модели булева функция задаётся ориентированным ациклическим графом с одним стоком, истоки которого помечены входными переменными, а остальных вершины — битовыми операциями. Схемная сложность булевой функции — это размер самой маленькой схемы, которая её вычисляет. Доказательство верхних и нижних оценок на схемную сложность булевых функций является одним из классических направлений теории сложности вычисления. Поиск минимальных схем для конкретных функций от небольшого числа переменных можно автоматизировать. Один из самых простых и эффективных подходов — это использование SAT-решателей, специальных программ для решения задачи выполнимости формулы в КНФ
Теория узлов и кос
Теория узлов и кос — один из интереснейших разделов алгебраической и комбинаторной топологии, имеющий применения во многих областях математики, в криптографии, физике, химии, биологии и т.д. К примеру, с помощью узлов можно описать любое трехмерное многообразие или изучать квантовую теорию поля, а заузленность молекулы полимера может влиять на ее свойства.
В курсе мы охватим, практически «с нуля», базовые и наиболее яркие элементы теории узлов и кос, связи с теорией групп и полугрупп, теорией трехмерных многообразий, теорией гомотопий, гиперболической геометрией, теорией случайных процессов. Мы планируем предложить к обсуждению задачи, ведущие к глубинным закономерностям теории, но допускающие наглядные понятные формулировки и имеющие элементарные подходы к возможным путям к решению.
Минимальные бивогнутые функции
В курсе будет расскано о методе функции Беллмана на примере одной вполне конкретной задачи. Метод функции Беллмана — это техника доказательства неравенств, обладающих определенным самоподобием, такие неравенства часто встречаются в теории вероятностей и гармоническом анализе; иногда этот и родственные методы называют «индукцией по шкалам». Прелесть техники состоит в том, что она неимоверно точна, и позволяет не только доказывать трудные неравенства, но и находить в них точные константы, а также иногда и оптимальные конфигурации, на которых достигаются равенства.
Пример, который мы будем рассматривать — описание функции распределения мартингального преобразования события при помощи минимальных бивогнутых функций на полосе. Эта задача, с одной стороны, позволяет прикоснуться к основным идеям метода функции Беллмана, а с другой — имеет очень наглядный геометрический смысл, который, в частности, дает простор для компьютерных экспериментов.
Формат программы
Программа не является соревновательной. Хорошо выполненный проект превратится в репозиторий с кодом или публикацию, ссылка на которые в резюме поможет вам при поступлении в магистратуру МКН или другие места. Вы сможете пообщаться с преподавателями не только по проектам, но и обо всём, что вам интересно, а также завести новые знакомства с другими мотивированными студентами.
На каждый проект будет отобрано до девяти человек среди тех, кто решил как можно больше задач по этому проекту до 13 февраля. Порядок отбора приведён на странице смены.
