“AI 에이전트에게 신용카드를 맡기는 건 10대에게 신용카드를 주는 것과 같다. 많은 일을 해낼 수도 있지만, 창고 가득 사탕을 주문하거나 조랑말을 사올 수도 있다.”

바이런 쿡(Byron Cook) 아마존웹서비스(AWS) 부사장 겸 특임 과학자는 3일(현지시간) 미국 라스베이거스에서 열린 ‘AWS 리인벤트 2025’ 기조연설에서 현재 AI 에이전트의 신뢰성 문제를 이렇게 비유했다. 자동화된 추론 분야 최고 권위자인 그는 “에이전트는 대형언어모델(LLM)을 기반으로 하는데, LLM은 할루시네이션(환각)을 일으킨다”며 “복잡한 규칙이나 논리 앞에서 실수하고, 추론 과정에 논리적 오류가 포함된다”고 지적했다.

그가 제시한 해법은 2000년 전 고대 그리스로 거슬러 올라간다. 유클리드가 기하학 정리를 증명하던 방식, 즉 수학적 논리를 AI에 적용하는 것이다. 쿡 부사장은 “자동화된 추론(Automated Reasoning)은 수학적 논리에서 증명을 찾고 매우 세밀하게 검증하는 기술”이라며 “유클리드가 고대 그리스 시대에 수행했던 것과 같은 유형의 추론”이라고 설명했다.

AWS는 이를 ‘뉴로-심볼릭 AI(Neuro-Symbolic AI)’라고 부른다. LLM의 통계적 방법을 나타내는 ‘뉴로(neuro)’와 수학적 논리를 뜻하는 ‘심볼릭(symbolic)’의 합성어다.

◇ 베드록 가드레일에 자동 추론 검사 추가

AWS는 이날 ‘아마존 베드록 가드레일(Amazon Bedrock Guardrails)’에 자동화된 추론 검사 서비스를 추가한다고 발표했다. 베드록 가드레일은 LLM 애플리케이션에 안전장치를 제공하는 서비스로, 유해 콘텐츠 필터링이나 개인정보 보호 등의 기능을 제공해 왔다.

이번에 추가된 자동 추론 검사는 LLM의 응답이 수학적으로 증명 가능한 규칙을 위반하지 않는지 실시간으로 검증한다. 예를 들어 환불 정책을 해석하는 에이전트가 논리적 오류를 범하면, 자동 추론 검사가 이를 즉시 차단하고 수정을 요구한다.

쿡 부사장은 “지금까지 대부분의 에이전틱 시스템은 ‘LLM을 심판으로’(LLM as a judge) 같은 통계적 방법을 사용해 가이드라인을 적용했다”며 “하지만 신뢰, 돈, 인명이 걸린 민감한 상황에서는 이런 방식이 절대 통하지 않는다”고 강조했다.

자동화된 추론은 컴퓨터 프로그램의 모든 가능한 실행 경로를 수학적으로 검증한다. 쿡 부사장은 “유클리드가 모든 가능한 직각삼각형에 대해 피타고라스 정리를 증명했던 것처럼, 우리도 컴퓨터 프로그램의 모든 가능한 실행에 대해 추론할 수 있다”고 말했다.

일례로 데이터가 저장되기 전에 암호화되는지 확인하고 싶다면, 이 속성을 논리 공식으로 인코딩한 뒤 수학적 논리 기법을 사용해 실제로 항상 참인지 증명한다. 쿡 부사장은 “기호 논리(symbolic logic)를 사용하기 때문에 시스템에 대한 모든 가능한 입력과 실행 중 도달할 수 있는 모든 가능한 구성에 대해 추론하고 있다는 것을 알 수 있다”고 강조했다.

◇ 10년간 내부 검증… 이제 고객에게 개방

AWS는 이 기술을 10년 넘게 내부 시스템에 적용해 왔다. 가상화 스택, 암호화 시스템, 신원 관리, 네트워크 등 AWS의 핵심 인프라가 자동화된 추론으로 검증됐다. 고객들도 IAM 액세스 분석기(IAM Access Analyzer), VPC 도달 가능성 분석기(VPC Reachability Analyzer), S3 퍼블릭 액세스 블록(S3 Public Access Block) 등을 통해 이 기술을 직접 사용하고 있다.

쿡 부사장은 “항공우주, 철도 전환, 산업 제어 시스템 등 실패가 용납되지 않는 미션 크리티컬 시스템에서 이 기술이 사용되고 있다”며 “이제 이와 동일한 기술을 에이전틱 AI 세계에 적용하고 있다”고 밝혔다.

AWS는 자동화된 추론을 AI 에이전트에 세 가지 방식으로 적용한다. 먼저 LLM의 출력물을 검증하는 방식이다. 출력물이 프로그램이든 에이전트 지시사항이든 Q&A 응답이든, 자동화된 추론 도구가 답변을 검증한다. 문제가 발견되면 LLM에 다시 시도하도록 요청하는 피드백 루프가 생성된다. 베드록 가드레일의 자동 추론 검사가 바로 이 방식이다.

다음은 자동화된 추론 도구의 출력물로 LLM을 훈련시키는 것이다. 쿡 부사장은 “많은 모델 제공업체가 ‘린 정리 증명기(Lean theorem prover)’를 사용해 잘 추론되고 정확한 무제한의 훈련 데이터를 만든다”며 “딥시크(DeepSeek)가 린을 사용해 훈련하는 대표적 사례”라고 설명했다.

마지막은 LLM 추론 인프라 내부에 검증기를 심는 ‘제약 디코딩(constrained decoding)’ 방식이다. 예를 들어 LLM이 “프랑스의 수도는?”이라는 질문에 “베를린”이라는 틀린 답을 말하려고 하면, ‘B’ 토큰을 출력하기 전에 형식적 추론 모델이 개입해 ‘P’(파리의 첫 글자)로 유도한다. 쿡 부사장은 “추론을 추론 인프라로 왼쪽으로 이동시키는 것”이라고 표현했다.

◇ 큐 디벨로퍼·에이전트 정책에도 적용

지난해 5월 출시된 아마존의 에이전틱 통합개발환경(IDE) ‘큐 디벨로퍼(Q Developer)’에도 이 기술이 적용됐다. 큐 디벨로퍼는 설계 단계에서 애플리케이션을 분석해 검수 기준(acceptance criteria)을 식별한다. 예를 들어 계산기 앱을 만들 때 ‘오류가 발생하면 앱은 결국 명확한 오류 메시지를 표시해야 한다’는 기준을 세운 뒤, 이를 명세(specification)로 변환한다.

쿡 부사장은 “이 명세를 사용해 LLM이 코드를 찾도록 안내할 수 있고, 명세 구조를 활용해 테스트를 생성할 수도 있다”며 “자동화된 추론을 사용해 명세에 대한 프로그램의 정확성을 증명할 수도 있다”고 말했다.

큐 디벨로퍼는 API가 빠르게 변화하는 문제도 해결한다. 쿡 부사장은 “AWS는 모델 제공업체들이 모델을 업데이트하는 것보다 빠르게 진화한다”며 “API의 형식적 모델을 개발하고 유지 관리한 뒤, 에이전틱 도구가 합성하는 프로그램이 API를 존중하는지 추론할 수 있다”고 설명했다.

자동화된 추론은 에이전트 정책 관리에도 활용된다. 전날 기조연설에서 맷 가먼 AWS CEO가 발표한 ‘에이전트 정책(Policy in Agent)’이 대표적이다. 쿡 부사장은 “정책을 통해 에이전트가 외부 도구나 데이터와 상호작용하는 방식을 실시간으로 결정론적이고 감사 가능하게 제어할 수 있다”며 “자연어로 허용하려는 작업을 설명하면 우리가 ‘시더(Cedar)’라는 형식적 표현으로 번역한다”고 설명했다.

시더는 AWS가 2년 전 출시한 오픈소스 권한 부여 언어다. 최근에는 자동화된 추론 기반 분석이 추가됐다. 일례로 프로덕션 환경의 문제를 해결하기 위한 에이전트를 만든다고 가정할 때 ‘프로덕션 데이터에 접근하고 진단을 실행해 문제 해결 방법을 파악하되, 합의하기 전까지 프로덕션에서 변경하지 못하게 하고 싶다’는 요구사항을 자연어로 작성하면, AWS 프로덕션 환경의 리소스에 대한 업데이트 작업을 수행하지 못하도록 차단하는 시더 정책으로 자동 변환된다. 이 정책은 주권, 프라이버시, 가용성, 내구성, 보안 등 다양한 요구사항과 일치하는지 자동화된 추론을 통해 검증된다.

쿡 부사장은 “건전한 형식적 추론 기능과 생성형 AI의 결합은 신뢰할 수 있는 에이전트를 만드는 게임 체인저”라며 “강력할 뿐만 아니라 어떤 규모에서도 신뢰할 수 있고 안전한 에이전틱 시스템을 구축하는 데 도움이 될 것”이라고 강조했다.