Все семинары

В 1975 году в Отделении информатики ВЦ СО АН СССР была создана лаборатория теории вычислительных процессов, которую возглавил В.Е. Котов. Проект МАРС (Модульные Асинхронные Развиваемые Системы) стал первой крупной работой нового коллектива. Концепция проекта была изложена в совместной работе Г.И. Марчука и В.Е. Котова в 1978 г. В ней обоснованы существенные принципы организации вычислительного процесса: параллелизм обработки, доступа к данным и управления; децентрализация потоков обработки; асинхронность взаимодействия устройств и процессов; иерархичность, модульность и специализация компонентов. Проведенный анализ базировался на новых по тому времени моделях взаимодействия асинхронных процессов, а архитектура виделась как естественная реализация модели вычислений.

В этом докладе будет представлена формальная модель графического конвейера GPU, реализованная на языке моделирования Promela, для возможной будущей верификации с помощью средства проверки моделей SPIN. Будет представлен анализ исторических графических архитектур. Модель осуществляет реальный 3D рендеринг в целочисленных координатах, абстрагирует ключевые этапы конвейера — выборку вершин, обработку шейдеров, растеризацию, текстурирование и пиксельные операции как параллельные процессы, синхронизированные через буферизованные каналы и семафоры. Модель может служить основой для сравнения графических архитектур, демонстрации в учебных целях и формальной проверки корректности конвейера.

У экономического неравенства несколько измерений. Более распространены оценки неравенства населения по денежным доходам, но не менее значимо неравенство по накопленному богатству, имуществу в собственности. Как за последнее три десятилетия в России менялись институциональные условия для формирования собственности домохозяйств? Из каких данных складывается наше представление об имущественном неравенстве в современной России? Какой разрыв между богатыми и бедными они показывают? Какова «географические» особенности распределения богатства и богатых россиян?

17:30-18:10 Лидия Васильевна Городняя: Эволюция знания в языках программирования (завершение доклада, начатого 24 февраля, 25 минут доклад + 5 минут на обсуждение)

18:10-18:30 Борис Леонидович Файфель: Предварительная трансляция макро в HomeLisp (25 минут доклад + 5 минут на обсуждение)

18:30-19:00 Дмитрий Александрович Кондратьев: Парадигмы задания спецификаций программ (25 минут доклад + 5 минут на обсуждение)

17:30-18:30 Лидия Васильевна Городняя: Эволюция знания в языках программирования (40 минут доклад + 20 минут на обсуждение)

18:30-19:00 Татьяна Анатольевна Андреева: Хронология возникновения основных парадигм программирования (25 минут доклад + 5 минут на обсуждение)

19:00-19:30 Андрей Валентинович Климов: Взгляд на эволюцию языков программирования (25 минут доклад + 5 минут на обсуждение)

P.S.

(1) По согласованию с участниками семинара докладам второго часа может быть добавлено дополнительное время на обсуждение.

(2) Так как поступили еще две заявки на выступление на семинаре, посвященном Л.В. Городней, то ожидается продолжение нашего мини-workshop на одном из ближайших заседаний семинара.

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

В докладе представлен практический подход к интеграции формальной верификации в процесс модельно-ориентированного проектирования. Показано, как осуществлять верификацию моделей конечных автоматов, разработанных в российской среде моделирования Engee. Основное внимание сосредоточено на разработанном решении для автоматической генерации кода на языке Promela, используемом в известной системе верификации Spin. Рассмотрены специфические аспекты и особенности данной трансформации, возникающие при конвертации графических моделей в формальное представление.

Нательные кресты как символ принадлежности к христианскому вероисповеданию – самая массовая категория артефактов, обнаруженных при исследовании многих археологических памятников. Эти находки также являются свидетельством освоения русскими территории Новосибирской области в период XVIII – XIX вв. Раскопки проведены на нескольких комплексах. Это некрополь и фундамент Никольской церкви села Кривощеково, некрополи и фундаменты Спасского собора в городе Каинские и укрепленного фортпоста – Умревинского острога.

Разнообразие форм, декора, символики оформления, материала изготовления позволяют определить конфессиональную принадлежность его владельцев, их социальный и профессиональный статус, проследить миграционные маршруты переселенцев, а также локализовать географические центры Центральной России – источники миграции.

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

Это обзорный доклад, фокусирующийся на алгоритмах сортировки и поиска ближайших соседей в многомерных векторных пространствах — ключевых операциях векторных СУБД. Дается краткое описание роли векторных СУБД как важных компонентов автономных больших языковых моделей (agentic LLMs). Анализируется проблема “проклятия размерности”, которая является непреодолимым препятствием на пути к точному решению задачи поиска ближайших соседей. Классифицируются основные подходы к решению приближенного варианта данной задачи и методы их сравнения друг с другом. Также рассматривается роль современных аппаратных средств в ускорении работы с многомерными векторными данными на примере некоторых конкретных подходов. Доклад завершается формулировкой острых проблем, стоящих перед разработчиками и пользователями прикладных векторных СУБД, а также кратким обзором оригинальных подходов к решению этих проблем.

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

Большое пространство состояний реальных программ затрудняет или делает невозможной их непосредственную верификацию методом проверки модели (model checking). Наличие симметрии в программе достаточно часто позволяет упростить модель и сократить её пространство состояний, что приводит к резкому снижению времени верификации. Классический подход состоит в обнаружении группы симметрии и построении на её основе упрощенной модели для верификации. Однако не все инструменты имеют поддержку симметрии, а инструменты с такой поддержкой не всегда справляются с поставленной задачей.

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

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

Подход продемонстрирован на примере разработки и верификации арбитра ресурсов марсохода. Арбитр координирует доступ n процессов к m ресурсам, где n и m -- натуральные числа. Используются язык программирования C/C++ и инструмент проверки модели Spin. Модель поведения ядра автоматически извлекается верификатором Spin из C-кода. Проверке подлежат темпоральные свойства, выраженные в логике LTL.

Становление Новосибирской экономико-социологической школы тесно связано с именами академика Татьяны Ивановны Заславской и д.э.н. Розалины Владимировны Рывкиной. Визитной карточкой школы стали сельские/аграрные исследования, старт которым в середине 1960-х дал запрос новосибирских партийных органов о причинах массовой миграции сельского населения в города и способах сохранения трудового потенциала колхозов и совхозов. Чтобы ответить на поставленные вопросы, новосибирские социологи в кооперации с центральным статистическим управлением России (ЦСУ РСФСР) в 1967 г. опросили более 5000 сельских семей и собрали отсутствующую в ту пору информацию о социальной и производственной инфраструктуре сельских поселений Новосибирской области.

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

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

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