- Автоматические рассуждения в Temporal DL-Lite(arXiv)
Автор:Сабиха Тахрат, Герман Браун, Алессандро Артале, Марко Гарио, Ана Одзаки
Аннотация. В этом документе исследуется возможность автоматизированного анализа временных баз знаний (KB) DL-Lite (TDL-Lite). Мы тестируем использование готовых рассуждений LTL для проверки выполнимости баз знаний TDL-Lite. В частности, мы проверяем надежность и масштабируемость алгоритмов рассуждений при работе с TDL-Lite TBox в паре с темпоральным ABox. Мы проводим различные эксперименты, чтобы проанализировать производительность различных алгоритмов рассуждения, случайным образом генерируя базы знаний TDL-Lite, а затем измеряя время выполнения и размер переводов. Кроме того, чтобы сделать использование TDL-Lite KB реальностью, мы представляем полноценный инструмент с графическим интерфейсом для их разработки. Наш интерфейс основан на принципах концептуального моделирования и интегрирован с нашим инструментом перевода и темпоральной логикой.
2. Исследование задачи вывода на естественном языке с помощью автоматизированных инструментов рассуждений (arXiv)
Автор:Заид Марджи, Анимеш Нигхойкар, Джон Ликато
Аннотация : Задача вывода на естественном языке (NLI) является важной задачей современного НЛП, поскольку она задает широкий вопрос, к которому можно свести многие другие задачи: учитывая пару предложений, влечет ли первое за собой второй? Хотя современные наборы контрольных данных для NLI основаны на глубоком обучении, стоит использовать другие методы для изучения логической структуры задачи NLI. Мы делаем это, проверяя, насколько хорошо машинно-ориентированный контролируемый естественный язык (Attempto Controlled English) может использоваться для разбора предложений NLI и насколько хорошо автоматизированные средства доказательства теорем могут рассуждать над полученными формулами. Для повышения производительности мы разрабатываем набор правил синтаксического и семантического преобразования. Мы сообщаем об их эффективности и обсуждаем последствия для NLI и NLP на основе логики.
3. Сознание и автоматизированное мышление (arXiv)
Автор: Ульрике Бартелмесс, Ульрих Фурбах, Клаудия Шон
Аннотация: Целью этой статьи является демонстрация того, как система логического мышления первого порядка в сочетании с большой базой знаний может быть понята как система искусственного сознания. Для этого мы рассмотрим некоторые аспекты из области философии сознания и, в частности, теорию интеграции информации Тонони (IIT) и теорию глобального рабочего пространства Баарса. Они будут применяться к системе рассуждений Hyper с ConceptNet в качестве базы знаний в сценарии здравого смысла и когнитивных рассуждений. Наконец, мы демонстрируем, что такая система очень хорошо способна блуждать в сознании.
4. Инвариантное встраивание свойств для автоматизированного рассуждения (arXiv)
Автор:Мирослав Ольшак, Цезарий Калишик, Йозеф Урбан
Аннотация. Автоматизированные рассуждения и доказательства теорем в последнее время стали серьезной проблемой для машинного обучения. В других областях все более распространенными становятся представления, способные абстрагироваться от несущественных преобразований, таких как абстракция от переводов и поворотов в видении. Однако стандартные методы встраивания математических формул для обучения доказательству теорем еще не в состоянии справиться со многими важными преобразованиями. В частности, встраивание ранее невидимых меток, которые часто возникают в дефиниционных кодировках и при сколемизации, до сих пор было очень слабым. Аналогичные проблемы возникают при переносе знаний между известными символами. Мы предлагаем новую кодировку формул, которая расширяет существующие модели графовых нейронных сетей. Эта кодировка представляет символы только узлами в графе, не сообщая сети никаких сведений об исходных метках. Мы предоставляем дополнительные связи между такими узлами, которые позволяют сети восстанавливать значение и, следовательно, правильно встраивать такие узлы независимо от заданных меток. Мы тестируем предложенное кодирование в автоматическом средстве доказательства теорем, основанном на исчислении связности таблиц, и показываем, что оно улучшает лучшие характеристики, которые использовались до сих пор. Кодирование дополнительно оценивается в задаче выбора предпосылки и недавно введенной задаче угадывания символов, и показано, что она правильно предсказывает 65% имен символов.
