2020 год, том 24, выпуск 1 (PDF)
Рассматривается алгоритм верификации формализованных математических доказательств. Основная его часть формулируется в виде продукционной системы с метапеременными. Доказываются теоремы о его корректности и полноте.
Ключевые слова: автоматическое доказательство теорем, система автоматизации дедукции, верификация доказательств, язык первого порядка, исчисление предикатов, продукционная система, искусственный интеллект.
В статье вводятся графовые объекты, соответствующие функциональным программам, называемые диаграммами состояний. Показано, как можно использовать диаграммы состояний для решения задач верификации функциональных программ. Предлагаемый подход иллюстрируется примером верификации функциональной программы сортировки.
Ключевые слова: верификация программ, функциональные программы, диаграммы состояний.
Интерпретируемость решения, возможность обучения без учителя, масштабируемость сделали тематическое моделирование одним из наиболее популярных инструментов статистического анализа текстов. Тематические модели позволяют снизить размерность пространства данных, так как описывают каждый документ как вероятностную смесь абстрактных тем, каждую тему как распределение над словами словаря коллекции. Переход из пространства слов в пространство тем приводит к естественному решению проблем синонимии и полисемии терминов. Однако есть и ряд недостатков, вызванных зависимостью решения от инициализации. Неустойчивость тематических моделей являются общеизвестным фактом, однако связанная с ней проблема полноты до сих пор в литературе не изучалась. Для решения этой задачи в статье исследуется новый алгоритм нахождения полного набора тем, основанный на построении выпуклой оболочки. Экспериментально подтверждается эффективность данного алгоритма. На практике полный набор тем использовался в качестве инициализации модели ARTM (additive regularization for topic modeling). По сравнению с рандомизированным начальным приближением, базис тем позволяет повысить устойчивость, перплексию на более 10%, когерентность в разы.
Ключевые слова: вероятностное тематическое моделирование, устойчивость тематических моделей, полный набор тем тематических моделей, латентное размещение Дирихле, LDA, регуляризация, ARTM, BigARTM.
Определяется семантика арифметической реализуемости для формул языка теории множеств, основанная на гиперарифметических видах. Доказывается корректность конструктивной теории множеств без аксиомы объемности относительной этой семантики.
Ключевые слова: конструктивная семантика, реализуемость, арифметическая реализуемость, аксиоматическая теория множеств, гиперарифметические виды.
В работе рассматриваются одномерные сверточные схемы в базисе Маккалока-Питтса. Показано, что рассматриваемые схемы могут быть реализованы схемой из априорной и динамической части, в которой вычисления в априорной части не зависят от входных данных. При этом априорная и динамическая части имеют нелинейную глубину, равную 2.
Ключевые слова: сверточная нейронная сеть, нейронная схема, нелинейная сложность, модель Маккалока-Питтса.
В работе рассматривается соответствие между правильными семействами булевых функций и реберными ориентациями с единственным стоком на булевых кубах. Данное соответствие позволяет перенести часть результатов, полученных для указанных ориентаций, на язык правильных семейств: получить оценки на число правильных семейств порядка n ≥ 5 и показать, что задача распознавания правильности семейства является coNP-полной.
Ключевые слова: правильные семейства булевых функций, реберные ориентации с единственным стоком.
Автомат прогнозирует следующий символ входного сверхслова, если он выдает этот символ на выходе в предыдущий момент времени. В работе исследуется вопрос сужения класса автоматов для задачи прогнозирования произвольного общерегулярного сверхсобытия в многозначном алфавите. Получен класс автоматов достаточный для задачи прогнозирования, а также с его помощью доказан переход от оценок простых сверхсобытий к оценкам составных.
Ключевые слова: прогнозирование автоматами, общерегулярное сверхсобытие, автоматное прогнозирование общерегулярных сверхсобытий.
Для коэффициентов полиномов функций над конечными полями Fq рассматривается задача отыскания нижней оценки на максимум минимума числа ненулевых коэффициентов в полиноме, где максимум берется по всем функциям, а минимум — по их преобразованиям, соответствующим различным заданиям поля. При этом возможно рассматривать различные типы таких преобразований. В работе получена оценка L(q) ≥ q − 2 на максимум минимума числа ненулевых коэффициентов в полиноме для определенного типа преобразований, оставляющих нулевой элемент поля на месте.
Ключевые слова: коэффициенты полиномов, булевы функции, полином булевой функции, таблица значений функции, sagemath.
Данная статья посвящена описанию изменения размерности периодических подмножеств натурального ряда при, казалось бы, таких незначительных операциях, как удаление/добавление к множеству одного числа. В работе исследуется случай, когда размерность исходного множества равна 1 или 2. Под размерностью множества понимается минимальное число непересекающихся арифметических прогрессий, дающих в объединениее это множество. Для множеств размерности 2 результат получен только в случаях пар прогрессий общего положения. В работе приводятся результаты о том, как именно меняется размерность в зависимости от того, откуда удаляется/куда добавляется число x.
Ключевые слова: арифметическая прогрессия, натуральный ряд, прогрессивное множество.
Доказано, что почти любую булеву функцию от n переменных можно реализовать неизбыточной двухполюсной контактной схемой, допускающей единичный диагностический тест длины 8 относительно обрывов и замыканий контактов.
Ключевые слова: контактная схема, булева функция, обрыв контакта, замыкание контакта, единичный диагностический тест.