Лаборатория алгоритмики

Механико-математический факультет

Новосибирский государственный университет

Расписание семинара

Семинар лаборатории проходит по средам в 16:20. Расписание может меняться. Эта страница соответственно обновляется.

На сайте лаборатории в Контакте мы информируем о предстоящих докладах, изменениях расписания и других новостях лаборатории.

Дата Время Место Докладчик Тема
16.11.2016 16:20 4110 НГУ Д. Ю. Власов Машинное обучение в автоматическом доказательстве теорем
30.11.2016 16:20 4110 НГУ П. Г. Емельянов Декомпозиция булевых полиномов
07.12.2016 16:20 4110 НГУ А. И. Ерзин Задачи вычислительной геометрии и комбинаторной оптимизации в контексте оптимизации беспроводных сенсорных сетей
14.12.2016 16:20 4110 НГУ Н. Н. Токарева Алгоритмические задачи в области криптографии
21.12.2016 16:20 4110 НГУ В. Б. Бериков Оптимальные композиции алгоритмов кластерного анализа
08.02.2017 16:20 4117 НГУ Ю. Кочетов, В. Чулков Игры Штакельберга в размещении производства
15.02.2017 16:20 4117 НГУ М. А. Бульонков Автоматизация научных исследований в области математической экономики
22.02.2017 16:20 4117 НГУ Д. Ю. Власов Полонота и корректность алгоритма поиска вывода в языке Russell
15.03.2017 16:20 4117 НГУ А. В. Кононов Различные подходы к анализу структурных свойств оптимальных расписаний
22.03.2017 16:20 4117 НГУ Д. К. Пономарёв Логика и машинное доказательство в инженерии терминологических систем
29.03.2017 16:20 4117 НГУ Д. К. Пономарёв Логика и машинное доказательство в инженерии терминологических систем (продолжение)
Р. ван Беверн Параметризованные алгоритмы для оптимизаций маршрутов и расписаний
П. Г. Емельянов Системы поддержки принятия решений

Аннотации докладов

В. Б. Бериков. Оптимальные композиции алгоритмов кластерного анализа

Кластерный анализ имеет многочисленные приложения: сегментация изображений, построение филогенетических деревьев в биологии, тематическое моделирование коллекций текстовых документов, демографическая статистика и т.д. Существует большое число алгоритмов кластерного анализа, различающихся по способам понимания сходства, алгоритмам поиска оптимального решения и особенностям предметной области. Коллективный (ансамблевый) кластерный анализ позволяет повысить устойчивость решений, снизить зависимость результатов от неудачного выбора алгоритмов или их параметров. При использовании данного подхода генерируется набор базовых вариантов, а затем формируется итоговое консенсусное решение. Вес каждого алгоритма в коллективе может быть разным; под оптимальной композицией понимается такое сочетание, которое обеспечивает наилучшее качество.

В докладе будет сделан короткий обзор различных подходов к ансамблевому кластерному анализу, описаны критерии качества ансамбля. Особое внимание будет уделено подходу, основанному на взвешенных коассоциативных матрицах. Будет рассмотрена модель кластерного ансамбля с латентными классами, в рамках которой исследовано его поведение и найдены оптимальные веса алгоритмов.

М. А. Бульонков: Автоматизация научных исследований в области математической экономики

В докладе будут представлены средства поддержки экспериментов в области решения экономических задач, для которых характерны, во-первых, большие объёмы входных и выходных данных, во-вторых, сложность взаимовлияния внутренних и внешних факторов, а, следовательно, ограниченные возможности для формального описания и машинного моделирования, и, в-третьих, неоднозначность трактовки полученных результатов, что требует привлечения экспертного знания.

Система МИКС поддерживает весь цикл моделирования: от создания, верификации и хранения входных данных, до визуализации полученных результатов с картографической привязкой. Так МИКС-ПРОСТОР позволяет сравнивать загруженность транспортной сети в зависимости от её конфигурации и тарифов; МИКС-ОМММ поддерживает анализ и прогнозирование межрегионального взаимодействия с учетом экономических и социальных условий, а также динамики развития отдельных регионов; МИКС-АТПК реализует экономические игры развития территориально-производственного комплекса для разных стратегий заинтересованных сторон.

Д. Ю. Власов: Машинное обучение в автоматическом доказательстве теорем

Идея автоматизации процесса доказательства теорем (automated theorem proving, ATP) имеет длинную историю. Как самостоятельное направление исследований ATP появилось в 60-х годах 20 века, тогда, когда появился наиболее распространенный метод ATP — метод резолюций. С начала 70-х годов 20 века различные разновидности теории типов (на основе лямбда-исчисления) также активно используется в качестве основы для ATP. Фактически сейчас эти два подхода являются доминирующими в ATP. На сегодняшний день существует много систем ATP, использующих оба подхода, но пока применение ATP на практике является скорее исключением, чем практикой. Причина этого заключается в чрезвычайной комбинаторной сложности поиска доказательств. Даже мощнейшие суперкомпьютеры не могут в лоб доказать достаточно простые для человека утверждения.

Естественным решением проблемы сложности задачи является привлечение методов машинного обучения для сокращения перебора вариантов доказательства. За последние 10 лет совершен прорыв в области искусственных нейронных сетей, позволяющий эффективно обучать многослойные сети, и, используя такие сети, сейчас достигаются ранее недостижимые цели, такие как, например, победа машины над человеком в игре "го".

Несмотря на перспективность применения машинного обучения в ATP на этом пути в случае классического подхода — метода резолюций — есть большие проблемы. Дело в том, что доказательство, полученное методом резолюции очень не похоже на доказательство, которое обычно делает человек. Причина достаточно проста: метод резолюции "перерабатывает" формулы, понятные человеку в формулы специального вида, после чего включается механизм вывода, и, при достижении положительного результата (получения доказательства) очень трудно восстановить доказательство в привычном для человека виде. По той же причине сложно использовать для обучения полученные человеком доказательства, т.к. для использования в обучении их нужно превратить в доказательства, полученные методом резолюции. Метод, основанный на теории типов также подвержен подобной проблеме: привычные доказательства из книг и статей требуют серьезной переделки (на концептуальном уровне) для того, чтобы их можно было использовать.

Поэтому предлагается нетрадиционный подход: не использовать резолюцию или теорию типов, а вместо этого изначально оперировать доказательствами в той форме, в которой это делает человек. Это сразу очень сильно ухудшает ситуацию с комбинаторной сложностью (при том, что она и так очень большая), но зато появляется возможность брать "человеческие" доказательства для обучения. Очевидным плюса такого подхода является то, что доказательства всегда будут в читаемом виде, и подобная система имеет смысл даже если не получится достичь высоких результатов в ATP.

Д. Ю. Власов: Полонота и корректность алгоритма поиска вывода в языке Russell

Будет рассматриваться общий алгоритм поиска доказательств в произвольной дедуктивной системе в языке Russell с доказательством корректности и полноты этого алгоритма. Среди известных методов автоматического поиска доказательств теорем наиболее близким к этому алгоритму является обратный метод Маслова.

П. Г. Емельянов: Декомпозиция булевых полиномов

Декомпозиция сложных объектов в меньшие или проще устроенные — это важнейший методологический прием анализа в различных областях. Декомпозиция булевых формул является важным направлением исследований, имеющим длинную историю и широкий спектр приложений. Помимо комбинаторной оптимизации, теории игр и теории (гипер)графов, следует отметить синтез логических схем, в области которого данная задача привлекла внимание большого числа исследователей и получила наибольшее развитие. Возможность декомпозиции булевых формул, как одного из этапов их оптимизации, связана с такими ключевыми параметрами электронных схем, как размер, скорость срабатывания и потребление энергии. Сейчас у методов декомпозиции появились новые области применения, связанные с анализом данных с целью выявления знания о их внутренней структуре.

Под конъюнктивной декомпозицией (AND-декомпозиция) понимают отыскание двух или более формул, компонент декомпозиции, конъюнкция которых эквивалентна исходной формуле. В докладе рассматривается задачи AND-декомпозиции в нескольких классах булевых формул. Мультипликативный характер конъюнкции в этих классах формул приводит к тому, что в большинстве случаев компоненты декомпозиции имеют меньший размер, что и является обычно целью декомпозиции.

Декомпозиция называется дизъюнктной, если множество переменных у компонент не пересекается. Проблема существования дизъюнктной конъюнктивной декомпозиции является трудной для булевых формул в КНФ/ДНФ. Однако для позитивных ДНФ, СДНФ и АНФ установлен полиномиальный алгоритм для нахождения компонент дизъюнктной декомпозиции. Данный результат следует из эффективной факторизации полилинейных полиномов над конечным полем порядка 2, основанной на тестировании равенства нулю частных производных некоторого полинома, сконструированного из исходного. Комбинация дизъюнктных AND/OR декомпозиций дает конструктивный способ построения бесповторных формул (read-once), хотя и не является настолько же эффективным, как специализированный метод.

К сожалению, дизъюнктная декомпозиция, являющаяся привлекательной по характеристикам компонент, возможна в редких случаях. Можно привести довольно простую оценку, которая демонстрирует, что доля таких функций довольно быстро убывает. Поэтому возникает интерес к отысканию недизъюнктных видов декомпозиции, которые бы позволяли, быть может не всегда, достигать удовлетворительных результатов. Одним из таких видов является декомпозиция, которая, если это возможно, позволяет отыскать компоненты, разделяющие заранее предписанное подмножество переменных. Существуют функции, которые не являются дизъюнктно декомпозируемы, но декомпозируются, если допустить, например, наличие одной общей переменной для компонент разложения.

А. И. Ерзин: Задачи вычислительной геометрии и комбинаторной оптимизации в контексте оптимизации беспроводных сенсорных сетей

Беспроводные сенсорные сети (БСС) используют в труднодоступных или опасных для жизни и здоровья людей местах, либо по соображениям целесообразности. Часто беспроводные сети являются эффективнее проводных как по стоимости, так и по эффективности. Большинство БСС функционируют автономно. Важным критерием эффективности сети является время жизни – отрезок времени, в течение которого сенсоры собирают информацию о территории или/и объектах и передают её в базовую станцию (БС). Каждый сенсор собирает информацию в пределах некоторой области, которую называют его зоной покрытия. Время жизни БСС зависит от эффективности использования энергии сенсоров. Известно, что потери энергии сенсора пропорциональны площади покрытия и дальности передачи. Продлить жизнь БСС можно, решив последовательно три основные задачи:

  1. Построение наименее плотных покрытий территорий различными фигурами (кругами, эллипсами, секторами,...).
  2. Синтез энергоэффективной коммуникационной сети (КС).
  3. Построение в КС остовного дерева с корнем в БС и поиск расписания бесконфликтной агрегации данных по ребрам этого дерева минимальной длины.

На семинаре предполагается рассказать об этих трёх задачах, об их сложности и о подходах построения решений.

А. В. Кононов: Различные подходы к анализу структурных свойств оптимальных расписаний

Рассматриваются два подхода в исследовании фундаментальных свойств оптимальных решений в задачах теории расписаний. Первый подход связан с нахождением интервалов локализации оптимумов для задач с многопроцессорными работами и предполагает применение компьютера для установления теоретических результатов. Второй подход связан с проведением много-параметрического анализа для цеховых (многостадийных) задач теории расписания. Основные идеи обоих методов были разработаны в ИМ СО РАН профессором Севастьяновым и его учениками.

Ю. Кочетов, В. Чулков: Игры Штакельберга в размещении производства

В играх Штакельберга, как правило, рассматриваются два неравноправных игрока, которых будем называть лидер и ведомый. При размещении предприятий они конкурируют между собой за обслуживание клиентов на рынке. Игроки действуют следующим образом. Сначала на рынок выходит лидер. Он открывает свои предприятия, понимая, что вслед за ним на рынок придет его конкурент. Ведомый знает решение лидера и открывает собственные предприятия для обслуживания клиентов. Предполагается, что каждый клиент имеет свои предпочтения на множестве предприятий, которые зависят от расстояний до предприятий и качества обслуживания, предоставляемого игроками. Рассматриваются различные модели таких предпочтений, например, бинарные предпочтения, когда каждый клиент выбирает только одно предприятие в качестве своего поставщика, или так называемые гравитационные модели, когда клиент использует все открытые предприятия для получения продукции. Каждый клиент имеет определенную покупательную способность или вес. Предполагается, что эта характеристика клиента не зависит от расстояний до предприятий и запросы клиентов удовлетворяются полностью. Каждый игрок стремится максимизировать свою долю рынка. Задача состоит в том, чтобы найти решение лидера, гарантирующее ему максимальную долю рынка после ответного хода ведомого.

В докладе будут представлены точные математические формулировки таких игр Штакельберга в терминах двухуровневого частично целочисленного программирования. Вычислительная сложность, минимаксные формулировки, эвристические и точные методы для этих игр будут подробно обсуждаться. Наконец, приложениям игр Штакельберга в телекоммуникационных сетях также будет уделено внимание.

Д. К. Пономарёв: Логика и машинное доказательство в инженерии терминологических систем

Лептоны, эукариоты, меланома — специализированные термины возникают во многих естественнонаучных предметных областях для именования и систематизации изучаемых объектов и явлений. Некоторые системы терминов являются стандартом на государственном и высшем профессиональном уровне, например, Общероссийский классификатор видов экономической деятельности (ОКВЭД), Международная классификация болезней (МКБ-10). Вопрос математической формализации определений терминов приобрел особую актуальность с развитием компьютерных методов работы с объемными данными. Стало понятно, что описание и выборку данных удобно производить, используя термины, которые привычны исследователям. А значит, должны существовать инструменты для формального компьютерного представления терминологических систем.

Новая история методов формализации систем терминов — это история успеха математической логики и ее приложений. Международные стандарты - компьютерные языки для описания терминологий - основаны на дескрипционных логиках, которые имеют тесную связь с логикой первого порядка и модальными логиками. С использованием этих стандартов в Интернет опубликованы сотни формализованных терминологий, которые применяются для аннотирования, интеграции, поиска данных в предметных областях физики, химии, биологии, медицины. Стандартные проблемы обнаружения дефектов и анализа терминологических систем сводятся к проблемам логического следования и могут быть решены методами автоматического доказательства. Например, проверка, является ли одно понятие более общим, чем другое, на основе присвоенных им определений, сводится к проверке (не)противоречивости множества формул. Прикладные задачи анализа терминологий оказываются связанными с фундаментальными свойствами, изучаемыми в математической логике, и позволяют по-новому взглянуть на классические разделы математики.

В докладе рассматривается метод логической формализации систем терминов и проблемы их анализа: проверка непротиворечивости терминологии, невырожденности термина, построение явных определений терминов, декомпозиция/комбинирование терминологических систем.

Н. Н. Токарева: Алгоритмические задачи в области криптографии

Научные исследования в области криптографии и защиты информации активно ведутся во всём мире, при этом особую роль в этом направлении играют математические исследования. Именно математические методы позволяют моделировать надёжные шифрсистемы и получать строгие оценки их стойкости.

Алгоритмические задачи криптографии всё чаще выходят на первый план. Среди них и проблемы поиска алгоритмов шифрования с оптимальными характеристиками, и вопросы существования односторонних функций и псевдослучайных генераторов, и создание новых криптографических протоколов, являющихся по своему определению ни чем иным как описанием распределённых алгоритмов, в выполнении которых участвуют хотя бы два игрока.

Более того, по оценке некоторых известных криптографов, прошлый, XX-й, век был веком развития алгоритмов, а нынешний станет веком развития вопросов сложности алгоритмов. Интересно.

Обо всём этом пойдёт речь в данном докладе.