Проекты
Начиная со второго курса студенты могут выбрать в качестве учебной практики теоретическую курсовую или практический проект. Практиками руководят сильнейшие ученые или ведущие сотрудники IT-компаний. Проекты могут быть самыми разными: браузерная игра, которая знакомит с машиной Тьюринга, сервис для изучения генома человека, предсказание цены продажи недвижимости, сервис для удалённого интервью, прототип датчика, который подсчитывает проехавшие мимо машины и другие.
С их помощью студенты:
С их помощью студенты:
- Знакомятся с самыми разными технологиями
- Понимают, какое направление или технология увлекают больше других
- Пробуют решить реальные рабочие задачи: проекты очень близки к ним
Примеры проектов
End2End моделирование голоса
Синтез речи (или text-to-speech) — это задача формирования сигнала, похожего на человеческую речь, по тексту. Обычно решение этой задачи разделяется на три части (модели):
1. G2P — эта часть переводит исходный текст в фонемы, в дальнейшем с ними работать удобнее.
2. Акустическая модель — эта часть описывает то, как связаны лингвистические признаки (текст) и акустические признаки целевого сигнала. Обычно это модель, строящая по фонемам мел-спектрограмму сигнала, который мы хотим в итоге предсказывать.
3. Вокодер — это модель, которая генерирует итоговый речевой сигнал по акустическим признакам (чаще всего по спектрограмме).
Основная проблема подхода в том, что эти три модели обучаются независимо друг от друга. Именно поэтому в последнее время распространяется использование end2end обучения, которое использует единую модель для решения всей задачи, без разбиения на несколько независимых моделей. Глобальная задача этого проекта — построить end2end модель для синтеза речи.
1. G2P — эта часть переводит исходный текст в фонемы, в дальнейшем с ними работать удобнее.
2. Акустическая модель — эта часть описывает то, как связаны лингвистические признаки (текст) и акустические признаки целевого сигнала. Обычно это модель, строящая по фонемам мел-спектрограмму сигнала, который мы хотим в итоге предсказывать.
3. Вокодер — это модель, которая генерирует итоговый речевой сигнал по акустическим признакам (чаще всего по спектрограмме).
Основная проблема подхода в том, что эти три модели обучаются независимо друг от друга. Именно поэтому в последнее время распространяется использование end2end обучения, которое использует единую модель для решения всей задачи, без разбиения на несколько независимых моделей. Глобальная задача этого проекта — построить end2end модель для синтеза речи.
PCB routing
Цель проекта — создать алгоритм (и имплементировать достаточно быстро работающий прототип), который решит автоматически задачу прокладки проводов, соединяющих компоненты на печатной плате.
Размеры компонент и их расположение на верхнем и нижнем слое уже дано, нужно только соединить их так, чтобы провода удовлетворяли определенным ограничительным условиям.
Проект выполнен совместно с лабораторией Huawei.
Размеры компонент и их расположение на верхнем и нижнем слое уже дано, нужно только соединить их так, чтобы провода удовлетворяли определенным ограничительным условиям.
Проект выполнен совместно с лабораторией Huawei.
| Смотреть проект |
Создание численного алгоритма по оптимизации обратной закачки газа с учетом технологических ограничений
Создание численного алгоритма по оптимизации обратной закачки газа с учетом технологических ограничений.
Необходимо разработать эффективный численный алгоритм оптимизации, который помогал бы выбрать оптимальную последовательность скважин, в которые будет закачиваться газ (такой метод помогает увеличивать нефтеотдачу). Целевая функция – экономическая эффективность проекта по итогам 20 лет.
Исходные данные. Для скважин-кандидатов даны численные характеристики эффективности: «закачано газа vs добыто нефти (драйвер экономической эффективности)» и «закачано газа vs добыто газа (отягчающий фактор)».
Образ результата: либо адаптация «классического» численного алгоритм для black-box оптимизации со штрафной функцией, либо разработка алгоритма, напрямую учитывающего упомянутые особенности задачи.
Необходимо разработать эффективный численный алгоритм оптимизации, который помогал бы выбрать оптимальную последовательность скважин, в которые будет закачиваться газ (такой метод помогает увеличивать нефтеотдачу). Целевая функция – экономическая эффективность проекта по итогам 20 лет.
Исходные данные. Для скважин-кандидатов даны численные характеристики эффективности: «закачано газа vs добыто нефти (драйвер экономической эффективности)» и «закачано газа vs добыто газа (отягчающий фактор)».
Образ результата: либо адаптация «классического» численного алгоритм для black-box оптимизации со штрафной функцией, либо разработка алгоритма, напрямую учитывающего упомянутые особенности задачи.
Verification of Truly Stateless model checker algorithm in Coq
Довольно часто в многопоточных программах случаются нестабильные баги. Чтобы ловить такие баги, можно использовать модел-чекеры (далее MC). Что они делают? Это специальные программы, которые на вход берут ваш многопоточный код и стараются некоторым способом обойти все возможные сцены его исполнения (может быть по модулю некоторой эквивалентности). Студент как раз работал над одним из таких MC.
Одной из задач на этот было завершение формального доказательства корректности на Coq алгоритма Truly Stateless concurrency model (TruSt), представленного в статье на POPL'22. Так же в планах реализовать пару модификаций этого алгоритма и сделать инстансы для конкретных моделей памяти на которых он работает.
Суть алгоритма TruSt, как и всех подобных MC, заключается в том, что он по данной на вход конкурентной программе (на любом языке поддерживающим компиляцию в LLVM) должен перебрать все возможные ее вычисления и для каждого из них проверить.
Однако запуская один и тот же код на разных языках или на разных процессорах, мы можем наблюдать разные поведения.
Одной из задач на этот было завершение формального доказательства корректности на Coq алгоритма Truly Stateless concurrency model (TruSt), представленного в статье на POPL'22. Так же в планах реализовать пару модификаций этого алгоритма и сделать инстансы для конкретных моделей памяти на которых он работает.
Суть алгоритма TruSt, как и всех подобных MC, заключается в том, что он по данной на вход конкурентной программе (на любом языке поддерживающим компиляцию в LLVM) должен перебрать все возможные ее вычисления и для каждого из них проверить.
Однако запуская один и тот же код на разных языках или на разных процессорах, мы можем наблюдать разные поведения.
| Смотреть проект |
Пески под спидами
Артур Саакян – студент третьего курса программы «Науки о данных» (до 2021 года МААД). Проект «Пески под спидами» он выполнил в осеннем семестре под руководством доцента МКН Никиты Калинина.
На примере моделирования песка Артур рассказывает, как «из воздуха» ускорить работу алгоритма и сэкономить математикам 400 лет жизни.
На примере моделирования песка Артур рассказывает, как «из воздуха» ускорить работу алгоритма и сэкономить математикам 400 лет жизни.
| Смотреть проект |