기계 번역으로 제공되는 번역입니다. 제공된 번역과 원본 영어의 내용이 상충하는 경우에는 영어 버전이 우선합니다.

자동 추론 검사 개념

이 페이지에서는 자동 추론 검사의 구성 요소를 설명합니다. 이러한 개념을 이해하면 효과적인 정책을 생성하고, 테스트 결과를 해석하고, 문제를 디버깅하는 데 도움이 됩니다. 자동 추론 검사가 수행하는 작업과 이를 사용하는 시기에 대한 개략적인 개요는 섹션을 참조하세요규칙.

정책

자동 추론 정책은 공식 로직 규칙 세트, 변수 스키마 및 선택적 사용자 지정 유형을 포함하는 AWS 계정의 리소스입니다. 이 정책은 LLM 응답을 검증하려는 비즈니스 규칙, 규정 또는 지침을 인코딩합니다.

정책은 자연어로 규칙을 설명하는 HR 핸드북, 규정 준수 매뉴얼 또는 제품 사양과 같은 소스 문서에서 생성됩니다. 정책을 생성하면 자동 추론 검사는 문서에서 규칙과 변수를 추출하여 수학적으로 확인할 수 있는 공식 로직으로 변환합니다.

정책, 가드레일과 애플리케이션 간의 관계는 다음과 같습니다.

Source Document ──► Automated Reasoning Policy ──► Guardrail ──► Your Application
  (natural          (rules + variables +           (references     (calls guardrail
   language)         custom types)                  a policy        APIs to validate
                                                    version)        LLM responses)
    

정책의 주요 특성:

정책 생성에 대한 step-by-step 지침은 섹션을 참조하세요자동 추론 정책 생성.

Fidelity 보고서

충실도 보고서는 추출된 정책이 생성된 소스 문서를 얼마나 정확하게 나타내는지 측정합니다. 보고서는 소스 문서에서 정책을 생성할 때 자동으로 생성되며, 모든 규칙 및 변수를 소스 콘텐츠의 특정 문에 다시 연결하는 자세한 근거 정보와 함께 두 가지 주요 점수를 제공합니다.

충실도 보고서는 비기술 주제 전문가가 공식 로직을 이해할 필요 없이 정책을 탐색하고 검증할 수 있도록 설계되었습니다. 콘솔의 소스 문서 탭에는 충실도 보고서가 문서에서 추출된 번호가 매겨진 원자성 문 테이블로 표시되며, 각 문이 근거하는 규칙과 변수를 보여줍니다. 특정 규칙 또는 변수를 기준으로 필터링하고 문 내에서 콘텐츠를 검색할 수 있습니다.

충실도 보고서에는 각각 0.0~1.0 범위의 두 가지 점수가 포함됩니다.

충실도 보고서는 집계 점수 외에도 정책의 각 규칙 및 변수에 대한 자세한 근거를 제공합니다.

규칙

규칙은 자동 추론 정책의 핵심입니다. 각 규칙은 변수 간의 관계를 캡처하는 공식 로직 표현식입니다. 규칙은 자동 추론 검사가 수학적 검증에 사용하는 공식 로직의 표준 형식인 SMT-LIB 구문의 하위 집합을 사용하여 표현됩니다. 자동 추론 정책에 대한 KMS 권한 섹션을 참조하세요

대부분의 규칙은 if-then(가시적) 형식을 따라야 합니다. 즉, 규칙에 암시 연산자에 의해 연결된 조건("if" 부분)과 결론("then" 부분)이 있어야 합니다=>.

올바른 형식의 규칙(if-then 형식):

;; If the employee is full-time AND has worked for more than 12 months,
;; then they are eligible for parental leave.
(=> (and isFullTime (> tenureMonths 12)) eligibleForParentalLeave)

;; If the loan amount is greater than 500,000, then a co-signer is required.
(=> (> loanAmount 500000) requiresCosigner)

베어 어설션( if-then 구조가 없는 규칙)은 항상 true인 문인 axiom을 생성합니다. 이는 양수 값이 있는 계정 밸런스와 같은 경계 조건을 확인하는 데 유용하지만 특정 조건을 논리적으로 불가능하게 만들고 검증 중에 예상치 못한 IMPOSSIBLE 결과를 초래할 수도 있습니다. 예를 들어, 베어 어설션은 자동 추론 검사가 이를 사용자가 상위 휴가 자격이 있는 것으로 취급한다는 것을 (= eligibleForParentalLeave true) 의미합니다. 자격이 없다고 언급하는 모든 입력은이 어시옴과 모순IMPOSSIBLE되므로의 검증 결과를 생성합니다.

;; GOOD: Useful to check impossible conditions such as 
;; negative account balance
(>= accountBalance 0)

;; BAD: This asserts eligibility as always true, regardless of conditions.
eligibleForParentalLeave

규칙은 다음 로직 연산자를 지원합니다.

효과적인 규칙 작성에 대한 모범 사례는 섹션을 참조하세요자동 추론 정책 모범 사례.

변수

변수는 자동 추론 검사가 자연어를 공식 로직으로 변환하고 규칙을 평가하는 데 사용하는 도메인의 개념을 나타냅니다. 각 변수에는 이름, 유형 및 설명이 있습니다.

자동 추론 검사는 다음 변수 유형을 지원합니다.

변수 설명의 중요한 역할

변수 설명은 번역 정확도에서 가장 중요한 단일 요소입니다. 자동 추론 검사는 자연어를 공식 로직으로 변환할 때 변수 설명을 사용하여 텍스트에 언급된 개념에 해당하는 변수를 결정합니다. 모호하거나 불완전한 설명은 TRANSLATION_AMBIGUOUS 결과 또는 잘못된 변수 할당으로 이어집니다.

예: 설명이 번역에 미치는 영향

사용자가 다음과 같이 질문한다고 가정해 보겠습니다. "여기에서 2년 동안 일했습니다. 육아 휴가 자격이 있나요?"

모호한 설명에서 자동 추론 검사는 "2년"을 24개월로 변환할지 모르거나 변수를 전혀 할당하지 않을 수 있습니다. 자세한 설명과 함께 번역은 모호하지 않습니다.

좋은 변수 설명은 다음과 같아야 합니다.

사용자 지정 유형( 열거형)

사용자 지정 유형은 변수가 취할 수 있는 명명된 값 집합을 정의합니다. 프로그래밍 언어의 열거형( 열거형)과 동일합니다. 변수가 고정된 값 집합이 있는 범주를 나타내는 경우 사용자 지정 유형을 사용합니다.

예:

열거형과 부울을 사용하는 경우:

번역: 자연어에서 공식 로직으로

번역은 자동 추론 검사가 자연어(사용자 질문 및 LLM 응답)를 정책 규칙에 따라 수학적으로 확인할 수 있는 공식 로직 표현식으로 변환하는 프로세스입니다. 이 프로세스를 이해하는 것은 문제를 디버깅하고 효과적인 정책을 만드는 데 중요합니다.

자동 추론 검사는 다음 두 단계로 콘텐츠를 검증합니다.

예: 작업 중 번역

변수isFullTime(bool), (int), tenureMonths (eligibleForParentalLeavebool) 및 입력이 포함된 정책이 주어짐:

1단계(번역)는 다음을 생성합니다.

Premises: isFullTime = true, tenureMonths = 18
Claims: eligibleForParentalLeave = true

2단계(검증)는 이러한 할당을 정책 규칙(=> (and isFullTime (> tenureMonths 12)) eligibleForParentalLeave)과 비교하여 확인하고 클레임이 인지 확인합니다VALID.

번역 정확도를 높이려면:

결과 및 검증 결과

자동 추론 검사가 콘텐츠를 검증하면 결과 집합이 생성됩니다. 각 결과는 검증 결과, 사용된 변수 할당 및 결론을 지원하는 정책 규칙과 함께 입력에서 추출된 사실적 클레임을 나타냅니다. 전체(집계된) 결과는 심각도에 따라 결과를 정렬하고 최악의 결과를 선택하여 결정됩니다. 최악의 심각도부터 최상의 심각도 순서는 TRANSLATION_AMBIGUOUS, IMPOSSIBLE, INVALID, SATISFIABLE, 입니다VALID.

조사 결과의 구조

결과 유형에 따라 결과에 존재하는 필드가 결정됩니다. 각 결과 유형에 대한 자세한 설명은 검증 결과 참조 섹션을 참조하세요. 그러나 대부분의 결과 유형은 다음 구성 요소가 포함된 공통 translation 객체를 공유합니다.

검증 결과 참조

각 결과는 정확히 다음 유형 중 하나입니다. 유형에 따라 결과의 의미, 결과에서 사용할 수 있는 필드, 애플리케이션에 대한 권장 작업이 결정됩니다. translation 필드를 포함하는 모든 결과 유형에는 변환에 정책 규칙과 무관한 논리적 문제(예: 항상 true 또는 항상 false인 문)가 포함된 경우 존재하는 logicWarning 필드도 포함됩니다.

신뢰도 임계값

자동 추론 검사는 여러 파운데이션 모델을 사용하여 자연어를 공식 로직으로 변환합니다. 각 모델은 자체 번역을 독립적으로 생성합니다. 신뢰도 점수는 이러한 번역 간의 일치 수준, 특히 의미상 동등한 해석을 생성한 모델의 비율을 나타냅니다.

신뢰도 임계값은 변환이 검증하기에 충분히 신뢰할 수 있는 것으로 간주되는 데 필요한 최소 계약 수준을 결정하는 설정한 값(0.0~1.0)입니다. 적용 범위와 정확도 간의 균형을 제어합니다.

임계값 작동 방식: