자동 추론이란?
자동 추론은 시스템 또는 프로그램이 수행할 작업 또는 절대 수행하지 않을 작업을 보장하려고 시도하는 컴퓨터 과학의 한 분야입니다. 이러한 보장은 수학적 증명을 기반으로 합니다. 사람들은 정리 및 추론과 같은 논리적 전략을 사용하여 많은 수학, 과학 및 컴퓨팅 분야의 논리적 문제를 해결합니다. 자동 추론은 동일한 도구를 사용하는 컴퓨터를 사용하여 복잡한 문제를 해결합니다. 자동 추론 도구는 알려진 수학 기법을 사용하여 프로그램(또는 논리 공식)에 대한 질문에 답하려고 시도합니다. 이 도구는 진술 또는 표현에서 참인 부분을 확인하는 데 도움을 줍니다.
자동 추론으로 어떤 문제를 해결할 수 있나요?
과학자와 소프트웨어 개발자는 자동 추론을 사용하여 두 가지를 증명합니다. 첫째, 시스템 설계 또는 구현이 사양을 준수한다는 것을 증명합니다. 둘째, 시스템이 의도한 대로 작동한다는 것을 증명합니다.
자동 추론은 수학적 정리 또는 알려진 진리에 의해 뒷받침되는 형식 논리로 증명을 생성하여 이를 수행합니다. 자동 추론은 수학적 논리 기반 알고리즘 검증 방법을 사용하여 가능한 모든 행동의 보안 또는 정확성을 입증합니다.
또한 자동 추론을 사용하여 시스템이 네트워크를 구성하고, 네트워크 액세스를 허용하거나 권한을 부여하고, 의도한 대로 데이터를 비공개로 안전하게 유지하는 데 사용되었음을 증명할 수 있습니다.
자동 추론을 사용할 때, 먼저 사용자가 시스템에 문제 진술을 제시합니다. 그러면 자동 추론 시스템이 문제 진술을 사용하여 전제를 계산하고 검증합니다. 소프트웨어는 모든 옵션을 대상으로 이 작업을 수행합니다.
자동 추론 문제 예시
자동 추론을 보다 정확하게 이해하려면 고양이는 육지에 사나요?라는 문제 진술과 다음 주장을 생각해 보세요.
- 고양이는 포유류이다.
- 포유류는 육지에 산다.
자동 추론 시스템은 문제 진술이 참인지 평가합니다. 특히 논리적 추론을 사용합니다. 고양이는 포유류이고 포유류는 육지에 산다는 것이 이 예시의 문제 진술입니다. 따라서 자동 추론 시스템은 고양이가 육지에 사는지 확인합니다.
자동 추론의 한계
자동 추론은 예측이나 일반화를 수행하지 않습니다. 예를 들어 자동 추론을 사용하여 다음과 같이 주장할 수 있습니다.
- 고양이는 털이 있다.
- 플러피는 고양이다.
- 따라서 플러피는 털이 있다.
자동 추론을 사용하여 다음과 같은 주장을 할 수 없습니다.
- 고양이는 포유류이다.
- 고양이는 육지에 산다.
- 따라서 모든 포유류는 육지에 산다.
이러한 응용은 연역적 추론 작업을 수행할 때 사람의 지도가 필요한 정리 증명자에서 흔히 볼 수 있습니다.
자동 추론 사용 사례로 어떤 것이 있나요?
단계별 논리적 추론이 가능한 자동 추론 기능은 여러 영역에서 도움이 됩니다. 자동 추론을 사용하면 대규모 아키텍처의 보안, 규정 준수, 가용성, 내구성 및 안전 특성을 입증할 수 있습니다.
다음은 자동 추론의 다른 사용 사례입니다.
수학적 모델링
과학자, 엔지니어 및 수학자는 과학 응용 분야에서 대수 공식을 적용하여 문제를 해결하고 수학적 증명을 검증합니다. 이러한 작업에서는 이들은 여러 변수를 사용하는 수학적 모델을 사용하여 가능성 있는 문제 해결책을 추론합니다.
하드웨어 검증
자동 추론은 하드웨어 엔지니어가 신뢰할 수 있는 제품을 만드는 데 도움이 됩니다. 하드웨어 엔지니어는 자동 추론을 통해 기존 테스트 방법에서 놓친 잠재적 결함을 발견할 수 있습니다.
예를 들어 전자제품 설계 엔지니어는 엄격한 수학적 자동 추론 분석을 사용하여 특정 하드웨어 설계가 시스템 동작 또는 실행과 같은 사양을 충족한다는 결정적인 증거를 얻습니다.
검증은 시스템의 가능한 모든 동작이 사양을 구성하는 시간적 속성을 충족한다는 것을 보여줍니다. 구현하는 시스템에서 가능한 각 동작이 상위 사양의 일부 동작과 일치한다는 것을 보여줄 수도 있습니다.
소프트웨어 검증
소프트웨어 개발자는 자동 추론을 사용하여 애플리케이션이 원치 않는 보안 문제의 영향을 받지 않고 견고하게 작동하고 소프트웨어가 의도한 대로 또는 설계한 대로 작동하게 만들 수 있습니다. 하드웨어 검증과 마찬가지로 개발자는 자동 추론을 통해 다양한 정책을 대상으로 소프트웨어 보안 조치를 확인할 수 있습니다.
예를 들어 Amazon Web Services(AWS)의 엔지니어들은 자동 추론을 통해 모든 부팅 구성에서 부팅 코드가 안전하다는 것을 증명합니다. 또 다른 예로 Amazon Simple Storage Service(S3)에서 저장 및 처리되는 데이터가 보호된다는 것을 증명합니다. 다음 예에서는 복제, 일관성, Auto Scaling, 로드 밸런싱 및 기타 조정 작업에 자동 추론을 사용합니다.
인간 추론 모델링
컴퓨터 과학자는 자동 추론 기술을 사용하여 액세스를 구성합니다. 이를 위해 컴퓨터 과학자는 사용자의 리소스 액세스 요청을 언제 허용하고 언제 거부하는지 설명하는 정책을 작성합니다. 이렇게 하면 의도한 사용자만 리소스에 액세스할 수 있게 되며, 이는 리소스의 보안 및 개인 정보 보호에 중요합니다.
예를 들어 컴퓨터 과학자는 만족도 모듈로 이론(SMT) 공식과 SMT 솔버를 사용하여 보안 특성을 증명합니다.
자동 추론 도구와 기법으로 어떤 것이 있나요?
다음으로, 아마존은 컴퓨팅 시스템이 사람의 추론을 수행할 수 있게 해주는 여러 가지 자동 추론 방법을 공유합니다.
고전 논리
고전 논리는 자동 논리적 추론 프로그램을 위한 기본 추론 모델을 제공하는 수학적 철학입니다. 이 논리는 각 명제가 진리값으로 참 또는 거짓 중 하나만 가질 수 있고 둘 다 가질 수는 없다는 원칙을 기반으로 합니다.
주로 수학자들이 존재한다와 같은 정량자를 문장에 사용하여 x와 같은 미지의 변수를 표현할 수 있는 1차 논리에 초점을 맞춥니다. 예를 들어 과학자들은 논리 프로그래밍에 고전 논리를 적용하여 x가 존재한다. x는 육지에 사는 포유류이다라는 문장에서 x를 찾습니다.
명제 논리
명제 논리는 참일 수도 있고 거짓일 수도 있는 명제와 그 명제 간의 관계를 구성하는 논리 체계이며, 이를 논거라고 합니다.
명제 논리의 고전적인 논거 표현은 P이면 Q입니다. 예를 들어 토요일이면 주말입니다.
자동 추론은 SAT 풀이라는 기법을 사용합니다. 자동 추론은 SAT 솔버라는 도구를 사용하여 명제 논리의 논거를 만족하는 값입니다. 다시 말해서 논거를 참으로 만드는 변수를 찾습니다.
자동 추론과 인공 지능의 차이는 무엇일까요?
자동 추론은 컴퓨터 시스템에 논리적 추론을 적용하는 인공 지능(AI) 분야입니다.
AI는 컴퓨터가 문제를 해결할 때 사람처럼 생각하도록 가르치는 과학입니다. 최근 AI가 발전하면서 딥 러닝, 데이터 분석 및 기계 학습을 비롯한 다양한 하위 분야도 함께 발전했습니다.
자동 추론은 자연어 처리(NLP)와 같은 다른 AI 기술과 다릅니다. 자연어 처리(NLP)는 컴퓨터가 서면 또는 구두 음성을 이해하도록 훈련하는 데 중점을 둡니다. 반면 자동 추론은 논리적 모델과 증명을 사용하여 시스템 또는 프로그램이 도달할 수 있거나 절대 도달할 수 없는 상태를 포함하여 가능한 동작을 추론합니다.
자동 추론과 딥 러닝의 차이는 무엇일까요?
자동 추론은 프로그램 또는 시스템의 속성을 증명합니다. 프로그램 또는 시스템 자체뿐만 아니라 시스템의 모델 또는 사양을 형식 논리에 사용합니다.
딥 러닝은 대규모 데이터 세트에 통계 모델을 적용하여 예측을 수행합니다.
딥 러닝은 인간 두뇌의 작동 방식을 모방하는 고급 기계 학습 기술입니다. 관련 정보를 추출, 비교 및 분석하는 여러 신경망 계층으로 구성된 다양한 신경망 모델을 사용합니다. 데이터 과학자는 자율 주행 자동차의 카메라 및 센서 데이터 처리와 같은 복잡한 애플리케이션에 딥 러닝을 사용합니다.
자동 추론은 기계 학습인가요?
자동 추론과 기계 학습은 같은 것이 아닙니다. 간단히 말해, 기계 학습은 예측과 추론을 수행합니다. 자동 추론은 증거를 제공합니다.
기계 학습은 대규모 데이터 샘플을 사용하여 의사 결정을 내리도록 컴퓨터를 학습시키는 AI입니다. 예를 들어 데이터 과학자는 기계 학습을 사용하여 사기 행위를 판별할 수 있도록 뱅킹 소프트웨어를 학습시킵니다. 대량의 재무 데이터 샘플을 사용하여 소프트웨어가 이전에 학습한 결과를 기반으로 비정상적인 패턴을 쉽게 식별할 수 있게 학습시킵니다.
모델을 데이터로 학습시키는 대신 자동 추론을 사용하면 모델이 수학적 진리와 증명을 기반으로 결과를 추론할 수 있습니다.
AWS는 자동 추론을 사용하여 서비스 상품을 어떻게 개선하나요?
AWS는 자동 추론을 사용하여 여러 서비스 상품을 개선합니다. 다음은 몇 가지 예입니다.
- Amazon CodeGuru Reviewer는 자동 추론과 기계 학습을 사용하여 개발자가 소프트웨어 취약성을 찾을 수 있도록 도와줍니다.
- Amazon Inspector Classic에는 네트워크 연결성이라는 기능이 있는데, 이 기능은 EC2 인스턴스를 자동으로 분석하여 잠재적 보안 취약성과 구성 오류를 찾아냅니다.
- AWS Identity and Access Management(IAM) Access Analyzer는 자동 추론을 사용하여 계정 권한을 관리합니다.
- Amazon Virtual Private Cloud(VPC) Reachability Analyzer는 자동 추론을 적용하여 AWS 네트워크를 이해하고 시각화하는 데 도움을 줍니다.
AWS 서비스 전반의 자동 추론에 대한 자세한 내용은 입증할 수 있는 보안을 참조하세요. 아마존은 수학적 추론을 사용하여 고객의 보안 워크로드를 철저하게 보호합니다.
지금 바로 계정을 생성하여 AWS에서 보안을 강화하세요.
