В прошедшем осеннем семестре сотрудники лабораторий JetBrains Research провели несколько открытых лекций в Computer Science Center. Тематика докладов разнообразная, как и области исследований лабораторий. Для удобства собрали ссылки на все выступления. Приятного просмотра!
Читать полностью »
Рубрика «jetbrains research»
Открытые лекции лабораторий JetBrains Research
2020-01-20 в 11:30, admin, рубрики: computer science, computer science center, jetbrains, jetbrains research, Блог компании Образовательные проекты JetBrainsВведение в контекстно-ориентированное программирование на Kotlin
2019-11-29 в 13:46, admin, рубрики: jetbrains research, kotlin, Блог компании Образовательные проекты JetBrains, ПрограммированиеЭто перевод статьи An introduction to context-oriented programming in Kotlin
В этой статье я постараюсь описать новое явление, которое возникло как побочный результат стремительного развития языка Kotlin. Речь идет о новом подходе к проектированию архитектуры приложений и библиотек, который я буду называть контекстно-ориентированным программированием.
Несколько слов о разрешении функций
Как хорошо известно, существует три основных парадигмы программирования (примечание Педанта: есть и другие парадигмы):
- Процедурное программирование
- Объектно-ориентированное программирование
- Функциональное программирование
Arend – язык с зависимыми типами, основанный на HoTT (часть 2)
2019-10-08 в 17:36, admin, рубрики: jetbrains research, Блог компании Образовательные проекты JetBrains, Программирование, языки программированияВ первой части статьи про язык Arend мы рассматривали простейшие индуктивные типы, рекурсивные функции, классы и множества.
2. Сортировка списков в Arend
2.1 Упорядоченные списки в Arend
Определим тип упорядоченных списков как пару, состоящую из списка и доказательства его упорядоченности. Как мы уже говорили, в Arend зависимые пары определяются при помощи ключевого слова Sigma
. Определение типа Sorted
дадим через сопоставление с образцом, вдохновившись определением из уже упомянутой статьи про упорядоченные списки.
func SortedList (O : LinearOrder.Dec) => Sigma (l : List O) (Sorted l)
data Sorted {A : LinearOrder.Dec} (xs : List A) : Prop elim xs
| nil => nilSorted
| :-: x nil => singletonSorted
| :-: x1 (:-: x2 xs) => consSorted ((x1 = x2) || (x1 < x2)) (Sorted (x2 :-: xs))
Обратите внимание: Arend сумел автоматически вывести, что тип Sorted
содержится во вселенной Prop
. Это произошло потому, что все три образца в определении Sorted
являются взаимно исключающими, а конструктор consSorted
имеет два параметра, оба из которых принадлежат Prop
.
Докажем какое-нибудь очевидное свойство предиката Sorted
, скажем, что хвост упорядоченного списка сам является упорядоченным списком (это свойство пригодится нам в дальнейшем).
Читать полностью »
Подход интенсивного обучения STEM
2019-09-14 в 9:59, admin, рубрики: jetbrains research, Блог компании Образовательные проекты JetBrains, образование, Учебный процесс в ITВ мире инженерного образования существует много отличных курсов, но зачастую программа обучения, построенная на них, обладает одним серьезным недостатком — отсутствием хорошей связности между различными темами. Можно возразить: как же так?
Когда формируется программа обучения, для каждого курса указываются пререквизиты и четкий порядок, в котором надо изучать дисциплины. К примеру, для того чтобы собрать и запрограммировать примитивного мобильного робота, нужно знать немного механики для создания его физической конструкции; основы электричества на уровне законов Ома/Кирхгофа, представления цифровых и аналоговых сигналов; операции с векторами и матрицами для того, чтобы описать системы координат и перемещения робота в пространстве; основы программирования на уровне представления данных, простейших алгоритмов и конструкций передачи управления и т.п. для описания поведения.
Есть ли все это в университетских курсах? Конечно есть. Однако к законам Ома/Кирхгофа мы получаем термодинамику и теорию поля; помимо операций с матрицами и векторами приходится разбираться с Жордановыми формами; в программировании изучать полиморфизм — темы, которые не всегда нужны для решения простой практической задачи.
Университетское обучение экстенсивно — учащийся идет широким фронтом и зачастую не видит смысла и практической значимости знаний, которые получает. Мы решили перевернуть парадигму университетского обучения STEM (от слов Science, Technology, Engineering, Math) и сделать такую программу, которая опирается на связность знаний, допуская наращивание полноты в будущем, то есть подразумевает интенсивное освоение предметов.
Читать полностью »
Как я научила робота бегать по видео с YouTube
2019-01-25 в 9:58, admin, рубрики: hse, jetbrains, jetbrains research, Алгоритмы, Блог компании Питерская Вышка, искусственный интеллект, машинное обучение, обучение с подкреплением, питерская вышка, Учебный процесс в ITМы продолжаем рассказывать о совместных научных проектах наших студентов и JetBrains Research. В этой статье поговорим об алгоритмах глубокого обучения с подкреплением, которые используются для моделирования двигательного аппарата человека.
Смоделировать все возможные движения человека и описать все сценарии поведения — достаточно сложная задача. Если мы научимся понимать, как человек двигается, и сможем воспроизводить его движения «по образу и подобию» — это сильно облегчит внедрение роботов во многие области. Как раз для того, чтобы роботы учились повторять и анализировать движения сами, и применяется машинное обучение.
Как учиться с помощью машинного обучения у экспертов в Dota 2
2019-01-10 в 13:00, admin, рубрики: hse, jetbrains, jetbrains research, Алгоритмы, Блог компании Питерская Вышка, демонстрации, искусственный интеллект, машинное обучение, обучение с подкреплением, питерская вышка, Учебный процесс в ITВ предыдущей статье от Питерской Вышки мы показывали, как при помощи машинного обучения можно искать баги в программном коде. В этом посте расскажем о том, как мы вместе с JetBrains Research пытаемся использовать один из самых интересных, современных и быстроразвивающихся разделов машинного обучения — обучение с подкреплением — как в реальных практических задачах, так и на модельных примерах.
Машинное обучение для поиска ошибок в коде: как я стажировался в JetBrains Research
2018-12-25 в 19:16, admin, рубрики: hse, jetbrains, jetbrains research, автоматический поиск багов, Блог компании Питерская Вышка, Карьера в IT-индустрии, машинное обучение, питерская вышка, Учебный процесс в ITНедавно мы рассказывали о том, как попасть на стажировку в Google. Помимо Google наши студенты пробуют свои силы в JetBrains, Яндекс, Acronis и других компаниях.
В этой статье я поделюсь своим опытом прохождения стажировки в JetBrains Research, расскажу о задачах, которые там решают, и подробнее остановлюсь на том, как при помощи машинного обучения можно искать баги в программном коде.