Что такое автоматизация логических рассуждений?
Автоматизированное построение логических рассуждений — это область компьютерных наук, задача которой состоит в определении того, что система или программа сделает или не сделает. Уверенность в этом основана на математических доказательствах. Люди решают множество логических задач в математике, естественных науках и вычислениях, используя логические стратегии, такие как теоремы и дедукции. Автоматизированное построение логических рассуждений реализовано на компьютерах, которые используют те же инструменты для решения сложных задач. Инструменты автоматизированного построения логических рассуждений пытаются ответить на вопросы о программе (или логической формуле), используя известные математические методы. Эти инструменты помогают проверить истинность высказывания или выражения.
Какие проблемы может решить автоматизированное построение логических рассуждений?
Ученые и разработчики ПО используют автоматизированное построение логических рассуждений, чтобы доказать две вещи. Во-первых, они доказывают, что конструкция или реализация системы соответствует ее техническим характеристикам. Во-вторых, они доказывают, что все работает в соответствии с концепцией.
Автоматизированное построение логических рассуждений позволяет получить доказательства в формальной логике, подкрепленные математическими теоремами или известными истинами. Автоматизированное построение логических рассуждений использует математические алгоритмические методы проверки, основанные на логике, для подтверждения безопасности или правильности всех возможных вариантов поведения.
Автоматизированное построение логических рассуждений также может быть использовано для доказательства того, что системы используются для настройки сетей, предоставления доступа к сети или предоставления разрешений, а также для обеспечения конфиденциальности и безопасности работы данных по назначению.
При использовании автоматизированного построения логических рассуждений в первую очередь системе необходимо поставить задачу. Затем система автоматизированного построения логических рассуждений вычисляет и подтверждает предположения с помощью постановки задачи. Программа делает это до тех пор, пока не исчерпает все возможности.
Пример задачи для автоматизированного построения логических рассуждений
Чтобы лучше понять автоматизированное построение логических рассуждений, рассмотрим постановку задачи «Живут ли кошки на суше?» и следующие утверждения:
- кошки — млекопитающие;
- млекопитающие живут на суше.
Система автоматизированного построения логических рассуждений оценивает, истинна ли постановка задачи. В частности, используется логическая дедукция. В этом случае кошки — млекопитающие, а млекопитающие живут на суше. Таким образом, это подтверждает, что кошки живут на суше.
Ограничения автоматизированного построения логических рассуждений
Автоматизированное построение логических рассуждений не делает предсказаний или обобщений. Например, мы можем использовать автоматизированное построение логических рассуждений, чтобы привести следующий аргумент:
- у кошек есть шерсть;
- Пушок — это кот.
- Следовательно, у Пушка есть шерсть.
Мы не можем использовать автоматизированное построение логических рассуждений для такого аргумента:
- кошки — млекопитающие;
- кошки живут на суше.
- Следовательно, все млекопитающие живут на суше.
Такие приложения часто используются в доказательстве теорем, которое требует участия человека в выполнении задач при построении дедуктивных рассуждений.
Каковы некоторые варианты использования автоматизированного построения логических рассуждений?
Способность автоматизированного построения логических рассуждений шаг за шагом делать логические выводы полезна в нескольких областях. Используя автоматизированное построение логических рассуждений, можно доказать безопасность, соответствие требованиям, доступность, долговечность и защищенность крупномасштабных архитектур.
Вот еще несколько примеров использования автоматизированного построения логических рассуждений.
Математическое моделирование
Ученые, инженеры и математики решают задачи и проверяют математические доказательства, применяя алгебраические формулы в научных приложениях. При решении таких практических задач они используют математические модели, основанные на нескольких переменных для определения вероятных решений проблемы.
Проверка аппаратного обеспечения
Автоматизированное построение логических рассуждений помогает инженерам аппаратного обеспечения создавать надежные продукты. Это дает им возможность выявлять потенциальные недостатки, упущенные из виду при использовании обычных методов тестирования.
Например, инженеры-проектировщики электроники прибегают к тщательному математическому автоматизированному анализу, чтобы получить убедительные доказательства того, что конкретная конструкция оборудования соответствует заданным техническим характеристикам, таким как поведение или исполнение системы.
Проверка показывает, что все возможные варианты поведения системы удовлетворяют временным свойствам, составляющим технические характеристики. Это также может показать, что каждое возможное поведение реализации системы соответствует некоторому поведению ее высокоуровневой спецификации.
Проверка программного обеспечения
Разработчики ПО используют автоматизированное построение логических рассуждений, чтобы убедиться, что приложения защищены от нежелательных проблем безопасности и что программное обеспечение работает так, как предполагалось или было задумано. Аналогично проверке аппаратного обеспечения автоматизированное построение логических рассуждений позволяет разработчикам проверять меры безопасности программного обеспечения на соответствие различным политикам.
Например, инженеры Amazon Web Services (AWS) с помощью автоматизированного построения логических рассуждений подтверждают безопасность загрузочного кода для каждой конфигурации загрузки. Другой пример — они доказывают, что данные, хранящиеся и обрабатываемые в простом сервисе хранения данных Amazon (Amazon S3), защищены. В этом примере разработчики используют автоматизированное построение логических рассуждений для репликации, согласованности, автомасштабирования, балансировки нагрузки и других задач координации.
Моделирование человеческого мышления
Ученые-информатики используют технологии автоматизированного построения логических рассуждений для настройки доступа. Для этого они составляют политики, описывающие, когда разрешать и отклонять запросы пользователей на доступ к ресурсу. Это подтверждает, что доступ к ресурсу имеют только предполагаемые пользователи, что важно для безопасности и конфиденциальности ресурса.
Например, ученые-информатики используют формулы задач выполнимости формул в теориях (SMT) и SMT-решатели для доказательства свойств безопасности.
Какие существуют инструменты и методы автоматизированного построения логических рассуждений?
Далее мы расскажем о нескольких автоматизированных методах дедукции, которые позволяют вычислительным системам выполнять человеческую дедукцию.
Классическая логика
Классическая логика — это философия математики, которая предоставляет базовые модели построения логических рассуждений для программ автоматизированного построения логических рассуждений. В основе этой логики лежит такой принцип: каждое предложение имеет истинное значение либо истинно, либо ложно, но не оба значения одновременно.
Основное внимание уделяется логике первого порядка, которая позволяет математикам представлять неизвестные переменные, такие как x, с помощью кванторов типа существует в предложении. Например, ученые применяют классическую логику в логическом программировании, чтобы найти x в таком предложении: Существует x, при этом x живет на земле, и x — млекопитающее.
Логика высказываний
Логика высказываний — это логическая система, в которой существуют предложения, которые могут быть истинными или ложными, и построение отношений между ними, называемых аргументами.
Классическое выражение аргумента в логике высказываний выглядит так: Если P, тогда Q. Например, если сегодня суббота, тогда это выходной день.
В автоматизированном построении логических рассуждений используется метод, называемый решением SAT. Он использует инструменты, называемые SAT-решателями, для поиска удовлетворительных назначений аргументам в логике высказываний. Здесь следует понимать переменные, подтверждающие истинность аргумента.
В чем разница между автоматизированным построением логических рассуждений и искусственным интеллектом?
Автоматизированное построение логических рассуждений — это особая дисциплина искусственного интеллекта, которая применяет логическую дедукцию к компьютерным системам.
Искусственный интеллект — это область науки, которая обучает компьютеры думать как люди при решении проблем. Последние разработки в области искусственного интеллекта привели к развитию различных дисциплин, включая глубокое обучение, анализ данных и машинное обучение.
Автоматизированное построение логических рассуждений отличается от других технологий искусственного интеллекта, таких как обработка естественного языка (NLP), которая направлена на обучение компьютеров пониманию письменной или устной речи. Вместо этого автоматизированное построение логических рассуждений использует логические модели и доказательства для обоснования возможного поведения системы или программы, в том числе состояний, которых они могут достичь или никогда не достигнут.
В чем разница между автоматизированным построением логических рассуждений и глубоким обучением?
Автоматизированное построение логических рассуждений подтверждает свойства программы или системы. Оно использует саму программу или систему, а также модель или технические характеристики системы в формальной логике.
Глубокое обучение выполняет прогнозирование на основе применения статистических моделей к большим наборам данных.
Глубокое обучение — это передовая технология машинного обучения, имитирующая работу человеческого мозга. Оно использует различные модели нейронных сетей, состоящие из нескольких слоев нейронов, которые извлекают, сравнивают и анализируют соответствующую информацию. Специалисты по работе с данными используют глубокое обучение для сложных приложений, таких как обработка данных камер и датчиков в беспилотных автомобилях.
Является ли автоматизированное построение логических рассуждений машинным обучением?
Автоматизированное построение логических рассуждений и машинное обучение — это не одно и то же. Если говорить кратко, машинное обучение позволяет делать прогнозы и выводы. Автоматизированное построение логических рассуждений предоставляет доказательства.
Машинное обучение — это часть искусственного интеллекта, которая обучает компьютеры принимать решения на основе больших выборок данных. Например, специалисты по обработке данных используют машинное обучение для обучения банковского программного обеспечения выявлению мошеннических действий. Они используют большие выборки финансовых данных, чтобы программное обеспечение легко выявляло аномальные шаблоны на основе ранее полученных результатов.
Вместо обучения модели данным автоматизированное построение логических рассуждений позволяет модели выводить результат, основанный на математической истине и доказательствах.
Как AWS использует автоматизированное построение логических рассуждений для улучшения предлагаемых сервисов?
AWS использует автоматизированное построение логических рассуждений для улучшения нескольких сервисных предложений. Ниже представлены несколько примеров.
- Ответственный за проверку Amazon CodeGuru использует автоматизированное построение логических рассуждений и машинное обучение, чтобы помочь разработчикам выявлять уязвимости программного обеспечения.
- В Amazon Inspector Classic есть функция сетевой доступности, которая автоматически анализирует инстансы EC2 на предмет потенциальных уязвимостей безопасности и неправильных конфигураций.
- Анализатор доступа к управлению идентификацией и доступом AWS (IAM) управляет разрешениями учетных записей с помощью автоматизированного построения логических рассуждений.
- Анализатор достижимости виртуального частного облака Amazon (Amazon VPC) применяет автоматизированное построение логических рассуждений для упрощения понимания и визуализации сети AWS.
Посетите страницу Доказуемая безопасность для получения дополнительной информации об автоматизированном построении логических рассуждений в сервисах AWS. Мы используем математическое обоснование, чтобы обеспечить достоверные гарантии безопасности рабочих нагрузок.
Создайте учетную запись уже сегодня и начните работу с безопасностью в AWS.
AWS: дальнейшие шаги
Получите мгновенный доступ к уровню бесплатного пользования AWS.
