Prove It, Part 2: Formal logic, Cedar policies, and the economics of verification

자동 추론은 비즈니스 정책을 형식 로직으로 변환하고, 해당 규칙과 대조하여 LLM 결과에 더해 검증을 추가합니다. 수동 QA 비용보다 훨씬 적은 비용으로 할루시네이션을 감지하고 규정 준수 제약 조건을 적용하며 전체 적용 범위에 걸쳐 에이전트 작업을 제어합니다.

Part 1('Probably Correct' Is Not Good Enough")에서는 AI를 기반으로 비즈니스를 구축하는 Startup에 결정론적 검증이 필요한 이유를 살펴보았습니다. 이 게시물에서는 내부 작동 방식을 살펴보도록 하겠습니다. AI Startup의 기술 공동 창업자, 엔지니어링 책임자 또는 선임 개발자라면, 자동 추론이 실제로 어떻게 작동하는지, LLM이 응답을 생성하고 공식 로직이 이를 검사할 때 어떻게 되는지, 경제성 측면에서 QA 팀을 고용하는 것과 비교할 때 이 서비스를 사용하는 것이 왜 타당한지 알 수 있습니다.

이 게시물에는 API 코드가 없습니다. 코드는 3부에 나와 있습니다. 여기서는 무엇을 구축하는지 알기 쉽도록 개념, 형식 로직, 검증 파이프라인에 초점을 맞춥니다.

확률론적 vs. 결정론적: 근본적인 차이점

메커니즘을 자세히 살펴보기 전에, 모든 아키텍처 결정에 영향을 미치는 만큼 핵심 개념을 명확하게 구분하는 것이 좋습니다.

LLM은 확률론적입니다.

훈련 데이터에서 학습한 확률 분포를 기반으로, 다음 토큰을 예측합니다. 온도, top-k, top-p 샘플링 파라미터는 의도적인 무작위성을 유발합니다. 동일한 프롬프트를 두 번 실행하면 결과가 달라질 수 있습니다. 이는 버그가 아니라 의도적인 기능입니다. LLM을 유연하고 창의적이며 다양한 자연어 입력을 처리할 수 있게 해줍니다. 하지만 이는 모든 단일 결과가 확률 분포의 샘플이지 입증된 사실이 아니라는 의미이기도 합니다.

자동 추론(AR)은 정확합니다.

규칙 세트와 입력이 주어졌을 때, 결과는 단순한 추측이 아니라 증명입니다. 명제는 주어진 규칙에 대해 증명 가능하고 유효하거나, 증명 가능하고 무효이며, 또는 시스템이 어떤 정보가 부족 또는 모호한지를 정확히 알려줍니다. 답변이 틀렸다면, AR은 단순히 오류를 표시하는 데 그치지 않고 왜 잘못되었는지 정확히 보여주는 반례를 제공합니다. 결과는 확률에 기반한 것이 아니라 수학적으로 검증 가능합니다. 여기에는 온도 설정도 없습니다. 샘플링도 없습니다. 대신, 직접 검토할 수 있는 증명이 존재합니다.

이는 어느 한 접근 방식이 ‘더 우수하다’는 문제가 아닙니다. LLM은 자연어를 이해하고 인간과 유사한 답변을 생성하는 데 더 뛰어납니다. 반면, AR은 그러한 답변이 논리적으로 올바른지를 검증하는 데 더 뛰어납니다. 이 둘이 결합되면 완전한 스택이 만들어집니다. 즉, LLM이 대화를 담당하고 AR이 정확성을 담당합니다. 신경망과 형식 로직이 결합된 이러한 형태를 연구자들은 신경기호 AI라고 부릅니다.

첫 100명의 고객에게 제품을 제공하는 5인 규모 Startup에게 이러한 차이는 매우 실질적인 의미를 가집니다. 별도의 QA 팀을 둘 인력도 없고, 규정 준수 인시던트로 인한 비용을 감당할 여유도 없습니다. 형식 검증은 이러한 상황에서 강력한 레버리지가 되고, 소규모 팀이 훨씬 더 큰 조직처럼 리스크 없이 제품을 출시할 수 있도록 해줍니다.

Amazon Bedrock의 두 가지 보호 계층은 무엇인가요?

AWS는 AR을 두 계층에서 제공하며, 이는 대부분의 AI Startup이 거치는 성장 단계와 일치합니다. 초기 단계에서는 제품이 대개 챗봇이나 어시스턴트 형태입니다. 즉, LLM이 고객의 질문에 답하거나, 추천을 제공하거나, 가이드를 제시하는 구조입니다. 이 단계에서 Amazon Bedrock Guardrails의 자동 추론 기능은 정의된 비즈니스 규칙에 따라 모델 출력의 내용을 검증합니다.

비즈니스가 성장함에 따라 단순한 챗봇을 넘어 에이전트 기반 워크플로를 구축하게 됩니다. AI가 예약을 잡고, 환불을 처리하고, 데이터베이스를 조회하고, 외부 API를 직접 호출하게 됩니다. 이 단계에서는 Policy in Amazon Bedrock AgentCore가 도구가 실행되기 전에 게이트웨이에서 적용되는 Cedar 정책을 사용하여 에이전트가 수행하도록 허용되는 행동을 제어합니다.

Cedar 정책은 에이전트가 수행할 수 있는 작업을 결정합니다. 하지만 AR 검사 API를 에이전트 툴킷의 도구로 제공하여, 에이전트가 조치를 취하기 전에 스스로 중간 결론을 검증하도록 할 수도 있습니다. 에이전트는 정책에 따라 ApplyGuardRail을 직접 호출하고 조사 결과를 검사한 후 사용자의 개입 없이 자체 수정합니다. 다단계 워크플로를 계획하는 에이전트는 제안된 순서가 제약 조건에 위배되는지 확인하거나, 가정상의 모순을 찾아내거나, 입력에서 파생된 값이 실제로 반영되었는지 확인할 수 있습니다. 이를 통해 AR은 단순한 경계 검사를 넘어 추론 파트너의 역할을 하게 됩니다. 즉, 에이전트는 게이트에서 차단당하는 것이 아니라, 애초에 그 게이트로 향하는 잘못된 경로 자체를 피하게 됩니다.

두 가지를 비교하면 다음과 같습니다.

AR 검사와 Policy in Amazon Bedrock AgentCore는 애플리케이션의 여러 계층을 보호합니다.

• AR 검사는 AI가 말하는 내용을 검증합니다(예: 이 모기지 자격 답변이 대출 기준에 맞는가?).
• Policy in Amazon Bedrock AgentCore는 AI가 수행하는 작업을 제어합니다(예: 이 에이전트는 환불을 시작하거나 고객 계정을 쿼리할 권한이 있는가?).

현재 무엇을 구축하고 있는지에 따라 둘 중 하나부터 시작하거나 둘 모두로 시작할 수 있습니다.

• MVP가 정책 관련 질문에 답하는 챗봇이라면, AR 검사가 첫 번째로 통합되어야 합니다.
• 예약을 잡거나 자금을 이체하는 에이전트를 운영하는 경우, Policy는 첫날부터 반드시 갖춰야 하는 필수 요소입니다.

대부분의 Startup은 결국 두 가지를 함께 운영하게 됩니다.

AR 검사의 작동 방식: 비즈니스 규칙을 형식 로직으로 인코딩

AR의 입력은 정책이며, 정책은 이미 가지고 있는 문서로 시작됩니다.

핀테크 Startup이라면 대출 기준 문서일 수 있습니다. 의료 분야에서는 임상 프로토콜 또는 HIPAA 처리 절차일 수 있으며, 보험 분야라면 보험 인수 심사 지침이 있을 것입니다. 이 문서는 AI가 무엇을 말해야 하고 무엇을 말하지 말아야 하는지를 정의합니다. 또한 법무팀의 검토를 거쳤으며, 투자자들이 실사 과정에서 관련 내용을 확인했을 수도 있습니다. AR은 이러한 기존 아티팩트를 시행 가능한 규칙으로 바꿉니다. 처음부터 새로운 것을 만드는 것이 아닙니다. 이미 가지고 있는 것을 활성화하는 것입니다.

정책 문서(PDF, Markdown 또는 일반 텍스트)를 Amazon Bedrock에 업로드하면 시스템이 변수와 규칙이라는 두 가지 항목을 추출합니다.

변수는 해당 도메인의 개념을 나타냅니다. 각 변수에는 이름, 유형 및 설명이 있습니다. 모기지 자격 정책을 예로 들자면, 다음과 같습니다.

변수 설명은 정확도에 가장 큰 영향을 미치는 요소입니다. 설명이 모호하면 LLM은 해당 변수가 무엇을 의미하는지 추측하게 됩니다. 반면, 개념의 의미와 사용자가 이를 어떻게 표현하는지, 정책 문서에서 어떻게 등장하는지를 자세히 설명하면, LLM은 자연어를 올바른 형식 변수에 매핑하기에 충분한 컨텍스트를 얻을 수 있습니다. 바로 여기에서 Startup 창업자이자 도메인 전문가로서의 지식이 가장 큰 가치를 발휘합니다.

규칙은 변수 간의 관계를 캡처하는 형식 로직 표현식입니다. SMT-LIB 구문의 하위 집합을 사용하며 대부분은 if-then(암시적) 형식을 따릅니다.

이는 모기지 정책 문서를 업로드했을 때 Bedrock이 내부적으로 생성하는 내용입니다. 콘솔에서 이러한 규칙을 검토하여 시스템이 의도를 올바르게 반영했는지 확인할 수 있지만, 직접 SMT-LIB를 작성할 필요는 없습니다. 사용자는 정책을 자연어로 작성하고 시스템은 이를 형식 로직으로 변환합니다.

2단계 검증 프로세스

AR 정책을 설정하고 가드레일에 연결한 후에는(3부에서 다룸), 애플리케이션이 ApplyGuardRail로 보내는 모든 LLM의 답변이 2단계 검증 프로세스를 거칩니다. 이러한 분할을 이해하면 어디에 작업 시간을 할애해야 할지 알 수 있으므로, 이는 매우 중요합니다.

1단계: 변환

시스템은 사용자 질문과 LLM 답변 모두의 자연어를 정책에 선언된 변수를 사용하여, 단순 할당이 아닌 ‘>= 180 & earning <= 220’과 같은 형식 로직 조건자로 변환합니다. 여기서 변수에 대한 설명이 사용됩니다.

예를 들어 “35만 USD짜리 주택에 3만 USD를 투자한 고객은 일반 모기지를 이용할 수 있습니다”라는 답변이 있다면, 변환 단계에서는 다음과 같이 출력됩니다. downPaymentAmount = 30000, purchasePrice = 350000, mortgageType = CONVENTIONAL.

입력된 자연어를 로직으로 변환하는 데 LLM을 사용하는 것이 바로 이 시스템이 최대 99%의 검증 정확도를 주장하는 이유입니다. 변환의 정확성을 보장하기 위해, 단일 LLM에만 의존하지 않습니다. 대신 온도 설정이 서로 다른 여러 LLM을 병렬로 사용하여 동일한 변환 작업을 수행합니다. 이러한 중복 번역 결과들이 의미적으로 동일할 때에만 검증 결과를 생성합니다. 변환 결과들 사이에 불일치가 발생하면, 시스템은 대신 입력에 대한 두 가지 가능한 해석을 포함하는 AMBIGUOUS 결과를 반환합니다. 이후 LLM은 이 피드백을 활용해 자신의 답변을 명확히 하거나 사용자에게 추가 질문을 할 수 있습니다. 또한 시스템을 Carnegie Mellon University의 조건부 QA 데이터 세트로 벤치마킹한 결과, 시스템이 VALID로 판정한 사례 중 99% 이상에서 해당 판정이 정확한 것으로 확인되었습니다. 자세한 방법론은 이 문서에서 참조할 수 있습니다.

2단계: 검증

만족도 모듈로 이론(SMT) 솔버는 변환된 할당값이 모든 정책 규칙을 만족하는지 여부를 평가합니다. 이 단계는 정의상 수학적으로 타당합니다. 변환이 정확하면, 검증 결과는 증명 가능한 정확성을 갖게 됩니다..

모기지 예에서, 이 솔버는 먼저 계약금 비율을 (30000 / 350000) × 100 = 8.57%로 계산합니다. 그런 다음 이를 (=> (< downPaymentPercentage 20.0) (not (= mortgageType CONVENTIONAL))) 규칙과 비교합니다. 그 결과 8.57%는 20%보다 작기 때문에, mortgageType = CONVENTIONAL라는 결론은 논리적으로 유효하지 않습니다. 시스템은 어떤 규칙에 위배되는지와 그 이유를 정확히 보여주는 전체 트레이스와 함께 유효하지 않은 조사 결과를 반환합니다.

이는 Startup 개발자에게 실질적으로 무엇을 시사할까요? 변환 품질은 더 나은 변수 설명을 작성함으로써 사용자가 직접 개선할 수 있는 영역입니다. 검증을 위한 수학적 계산은 걱정할 필요가 없습니다. 도메인을 명확하게 설명하는 데 집중하면 되고, 나머지 검증 작업은 솔버가 처리합니다.

조사 결과는 무엇을 의미하나요?

AR 검사는 단순히 ‘통과’ 또는 ‘실패’를 반환하지 않습니다. 정확히 무슨 일이 있었는지, 다음에 무엇을 해야 하는지 알려주는 구조화된 결과를 반환합니다. 각 조사 결과는 다음 유형 중 하나입니다.

이 점은 중요합니다. AR 검사는 탐지 모드로 작동합니다. 즉, 결과와 피드백을 반환하지만 답변 자체를 차단하지는 않습니다. 애플리케이션은 반환된 결과를 검토한 후 답변을 그대로 제공할지, 다시 작성할지, 추가 설명을 요청할지, 아니면 안전한 기본 답변으로 대체할지 결정합니다. 이를 통해 모든 응답에 대해 수학적 검증을 수행하면서도 사용자 경험에 대한 완전한 제어권을 유지할 수 있습니다. 이러한 패턴의 실제 구현 예는 오픈 소스 재작성 챗봇 구현에서 참조할 수 있습니다. 이 예는 AR 조사 결과를 LLM에 다시 전달하여 자동으로 답변을 수정하는 방법을 보여줍니다.

AgentCore Policy: AI 에이전트의 결정론적 경계

AI가 다단계 워크플로를 조정하고, 도구를 직접 호출하고, 사용자를 대신하여 작업을 수행하는 에이전트 애플리케이션을 구축하는 Startup에게는 또 다른 신뢰 문제가 발생합니다. 즉, AI가 말하는 내용만 중요한 것이 아니라 AI가 무엇을 수행하느냐도 중요합니다.

의료, 핀테크 또는 법률 분야 Startup의 경우, 규정 준수 또는 규제 관점에서 ‘에이전트가 예상치 못한 작업을 수행했다’는 것은 용납되지 않습니다. 에이전트 행동에 대한 입증 가능한 경계가 필요하며, 에이전트가 프롬프트 인젝션으로 조작되거나 추론 오류를 범하는 경우에도 이러한 경계가 유지되어야 합니다.

Policy in Amazon Bedrock AgentCore는 게이트웨이 경계에서 모든 에이전트-도구 상호 작용에 적용되는 권한 부여 계층을 활용하여 이 문제를 해결합니다. 정책은 AR로 검증할 수 있도록 AWS가 구축한 인증 언어인 Cedar로 작성됩니다. Cedar 정책은 누가(위탁자) 어떤 조건에서 어떤 리소스에 대해 무엇(작업)을 할 수 있는지를 정의합니다. 일치하는 권한 없이는 도구 간접 호출이 게이트웨이를 통과하지 못합니다. Cedar에서 직접 정책을 작성하거나, 자연어로 규칙을 설명하고 시스템이 Cedar를 생성하도록 할 수 있습니다.

정책을 배포하기 전에 자동 추론은 시맨틱 검증을 실행하여 다음과 같은 문제를 찾아냅니다.

• 특정 주체/작업/리소스 조합에 대한 모든 요청을 허용하는 지나치게 관대한 정책
• 모든 것을 거부하는 지나치게 제한적인 정책
• 권한이 아무것도 허용하지 않거나 금지 조항이 아무것도 금지하지 않는 효과 없는 정책

이러한 정책의 시행은 규제 대상 산업의 Startup에 특히 중요한 두 가지 원칙을 따릅니다.

1. 기본적으로 거부: 어떤 정책도 특정 작업을 명시적으로 허용하지 않는 경우 해당 작업은 차단됩니다. 에이전트는 사용자가 승인하지 않은 어떤 작업도 수행할 수 없습니다.
2. 금지 규칙 우선: 다른 정책에서 해당 작업을 허용하더라도, 절대 무시할 수 없는 강제 차단 규칙을 설정할 수 있습니다.

한 의료 Startup이 일정 예약 에이전트를 만들고 있다고 가정해 보겠습니다. AgentCore Policy를 사용하면 환자가 자신의 기록에만 액세스하도록 하고, 예약을 업무 시간 내로 제한하고, 환불 금액 상한선을 정책으로 제한할 수 있습니다. 이러한 규칙은 에이전트에 메시지를 보내는 방식, 코드에 존재하는 버그 또는 사용자가 요청을 얼마나 창의적으로 처리했는지에 관계없이 적용됩니다. 정책 적용은 전적으로 에이전트 외부의 게이트웨이 경계에서 이루어집니다.

자동 추론은 수동 QA와 비교해 비용이 얼마나 드나요?

자동 추론의 경제성을 이해하려면 현재 대부분의 팀에서 사용하는 모델 출력의 수동 QA 검토 방식을 기준으로 비교해 보는 것이 좋습니다.

기존 방식: 수동 QA

AI 출력을 검토하는 한 검토자가 시간당 약 50건의 상호 작용을 처리할 수 있으며, 인건비를 포함한 비용은 시간당 약 40 USD 수준입니다. 월 10만 건의 고객 상호 작용을 처리하는 Startup이 모든 상호 작용을 검토하려면 월 8만 USD의 비용이 발생합니다. 10%만 샘플링하더라도 월 8,000 USD가 소요되며, 나머지 90%는 여전히 검증되지 않은 상태로 남습니다. 검토자 1인당 연간 비용이 8만~15만 USD라고 가정하면, 5~10명 규모의 검토 팀을 운영하는 데 연간 40만~150만 USD가 소요됩니다. 대부분의 Startup에게 이는 AI의 작동을 확인하는 데 사용하기에는 상당히 큰 비용입니다.

새로운 방식: 자동 추론

AR 검사는 검증 요청에 따라 가격이 책정됩니다(요율이 다를 수 있으므로 정확한 요금은 Bedrock 요금 페이지에서 확인해야 함). 수동 검토와 달리, 샘플링하지 않은 상태로 모든 상호 작용을 검증할 수 있습니다. Amazon Bedrock Guardrails는 텍스트 단위를 검증 단위로 사용하며, 각 텍스트 단위는 1,000자입니다. 일반적인 Startup에서는 다음과 같이 실행됩니다.

가정

계산

앞선 예처럼 월 10만 건의 상호 작용을 처리하는 Startup에서 각 상호 작용의 출력이 약 200 토큰이라고 가정해 보겠습니다. 이 경우 AR 검사를 검증에 사용하는 비용을 쉽게 추정할 수 있습니다. Amazon Bedrock Guardrails는 사용량을 텍스트 단위로 측정하며, 텍스트 단위 하나는 1,000자에 해당합니다. 토큰당 평균 4자를 기준으로 계산하면, 각 상호 작용은 약 800자이며 따라서 0.8 텍스트 단위에 해당합니다.

각각 0.8 텍스트 단위로 구성된 10만 건의 상호 작용을 검증할 경우, 월 총 8만 텍스트 단위가 됩니다. AR 검사 요금이 텍스트 단위 1,000개당 0.17 USD라면 단일 정책의 월 총 비용은 13.60 USD가 됩니다. 여러 정책을 적용할 경우 비용이 선형적으로 확대됩니다. 정책이 여러 개 있더라도 총 비용은 수동 검토보다 훨씬 저렴합니다.

규정 준수 관점에서 계산해 보면 그 가치는 더욱 분명해집니다. HIPAA 위반 범주 하나만으로도 현재 물가 기준 연간 최대 2,067,813 USD의 벌금이 부과될 수 있습니다. 매일 수천 건의 환자 상호 작용을 처리하는 의료 분야 Startup의 경우, 검증되지 않은 AI 출력으로 인한 규제 리스크는 기업의 존속 자체를 위협할 수 있습니다. 이러한 맥락에서 AR은 단순한 소프트웨어 비용 항목이라기보다 리스크 관리 통제 수단에 가깝다고 볼 수 있습니다.

개발자에게 가장 가까운 비유는 Rust의 borrow checker입니다. Rust는 코드가 프로덕션 환경에 배포되기 전에 컴파일 단계에서 메모리 손상 문제를 찾아냅니다. AR은 정책 위반이 고객에게 영향을 미치기 전에 검증 단계에서 포착합니다. 어떤 경우든, 문제가 피해를 일으키기 전에 잡아내면 사후에 수습하는 것보다 비용이 적게 듭니다.

물론 대가도 있습니다. AR 검증은 답변마다 지연 시간을 가중시키고, 재작성할 경우 문제가 발견된 답변에 대해 LLM이 두 번 실행됩니다. 하지만 대부분의 애플리케이션에서 이 비용은 잘못된 출력으로 인한 운영상, 법적 또는 평판상의 피해에 비하면 미미한 수준입니다.

이러한 논리는 투자자들에게도 설득력이 있습니다. AI 출력이 형식화된 비즈니스 정책에 따라 체계적으로 검증될 것임을 확신할 수 있다는 것은 단순한 제품 기능 이상의 의미가 있습니다. 이는 리스크가 선제적으로 관리되고 있다는 증거입니다. 즉, Startup의 리스크 관리 역량을 보여주는 구체적이고 검증 가능한 증거입니다.

다음 단계는 무엇인가요?

3부: 단계별 구현 플레이북에서는 개념부터 코드까지 살펴봅니다. 기존 문서에서 AR 정책을 생성하고, 이를 가드레일에 배포하고, ApplyGuardRail API와 통합하고, 결과를 프로그래밍 방식으로 처리하고, AgentCore Gateway를 통해 AgentCore Policy를 설정하고, 감사 추적을 작성하는 방법을 배우게 됩니다. 수학적 검증에 관한 내용을 읽는 것부터 프로덕션 환경에 배포하는 것까지, 필요한 모든 정보를 제공합니다.