Formal Semantics for Agentic Tool Protocols: A Process Calculus Approach

이 논문은 대규모 언어 모델 에이전트의 도구 호출 프로토콜인 SGD 와 MCP 를 프로세스 미적분으로 형식화하여 두 체계 간의 구조적 동형성을 증명하고, MCP 의 표현력 한계를 보완하는 새로운 형식적 기반 MCP+ 를 제시합니다.

핵심

이 논문은 **"거대 인공지능 (AI) 이 외부 도구를 사용할 때, 그 행동이 안전하고 정확한지 수학적으로 증명하는 방법"**을 제시합니다.

마치 새로운 도시에서 낯선 가게들을 찾아다니는 AI 여행 가이드가 있다고 상상해 보세요. 이 가이드는 가게의 메뉴판 (스키마) 을 보고 무엇을 시킬지 결정합니다. 하지만 메뉴판이 불완전하거나 모호하면, 가이드가 실수를 하거나 위험한 일을 저지를 수 있습니다.

이 논문은 바로 그 메뉴판의 표준과 안전 규칙을 수학적으로 다듬은 연구입니다. 핵심 내용을 쉬운 비유로 설명해 드리겠습니다.

---

1. 두 가지 다른 언어, 같은 목적

현재 AI 가 도구를 사용할 때 두 가지 주요 방식이 경쟁하고 있습니다.

• SGD (스키마 기반 대화): 연구실 출신의 '꼼꼼한 기획자' 스타일입니다. 모든 단계와 예외 상황을 미리 문서로 아주 자세히 적어둡니다. "돈을 이체할 때는 반드시 비밀번호를 확인해야 한다" 같은 규칙이 명확합니다.
• MCP (모델 컨텍스트 프로토콜): 업계 표준이 된 '실용적인 엔지니어' 스타일입니다. 다양한 도구와 연결되도록 빠르게 설계되었지만, 때로는 "이 도구가 위험한 작업인지, 승인 없이 해도 되는지" 같은 중요한 정보가 누락될 수 있습니다.

논문의 첫 번째 발견:
수학 (프로세스 계산) 을 이용해 분석해 보니, 이 두 방식은 기본 구조는 거의 비슷하지만, **MCP 는 중요한 정보가 빠져나가는 '불완전한 번역'**이라는 사실이 드러났습니다. 마치 고해상도 사진 (SGD) 을 저해상도缩略图 (MCP) 로 변환할 때 세부 묘사가 사라지는 것과 같습니다.

2. 왜 위험할까요? (정보 손실의 비유)

MCP 방식의 문제점을 은행 창구에 비유해 볼까요?

• SGD 방식: "이체하려면 먼저 잔고 확인을 하고, 고객 확인을 거쳐야 합니다."라고 명확한 절차가 적혀 있습니다.
• MCP 방식: "이체 도구 사용 가능"이라고만 적혀 있습니다.
  • 문제: AI 가 이 도구를 쓸 때, "아, 이거 승인 없이 해도 되나? 아니면 잔고 확인을 안 해도 되나?"라고 추측하게 됩니다.
  • 결과: 실수로 돈을 잘못 이체하거나, 보안 허점을 이용할 수 있습니다.

논문은 MCP 가 거래의 중요성 (승인 필요 여부), 오류 발생 시 대처법, 다른 도구와의 연결 관계 등을 명시적으로 적지 않아서 이런 위험이 생긴다고 지적합니다.

3. 해결책: 'MCP+' (다섯 가지 안전 규칙)

저자는 MCP 를 SGD 만큼 안전하고 완벽한 시스템으로 만들기 위해 **5 가지 새로운 규칙 (원칙)**을 추가한 **MCP+**를 제안합니다.

이를 **요리사 (AI) 와 레시피 (도구 설명)**에 비유하면 다음과 같습니다.

1. 의미의 완전성 (Semantic Completeness):

   • 비유: 레시피에 "소금"이라고만 쓰지 말고, "맛을 위해 소금 1 티스푼을 넣으세요"라고 이유와 맥락을 적어야 합니다.
   • 효과: AI 가 단순히 데이터가 아니라 '의미'를 이해하게 됩니다.

2. 명확한 행동 경계 (Explicit Action Boundaries):

   • 비유: "이 요리는 위험한 불을 사용하므로, 반드시 주방장 (사용자) 의 확인을 받으세요"라고 적어야 합니다.
   • 효과: AI 가 실수로 중요한 작업 (돈 이체, 데이터 삭제 등) 을 승인 없이 수행하는 것을 막습니다.

3. 실패 모드 문서화 (Failure Mode Documentation):

   • 비유: "만약 재료가 떨어지면 A 가게에서 구하거나, B 레시피로 대체하세요"라고 비상 계획을 적어야 합니다.
   • 효과: 시스템이 멈추지 않고 유연하게 대처할 수 있습니다.

4. 점진적 공개 (Progressive Disclosure):

   • 비유: 메뉴판에 모든 상세 설명을 다 적어두면 AI 가 읽느라 지쳐버립니다. 대신 **"간단한 요약"**을 먼저 보여주고, 필요할 때만 상세 설명을 보여주는 방식입니다.
   • 효과: AI 가 더 빠르고 효율적으로 도구를 선택할 수 있습니다.

5. 도구 간 관계 선언 (Inter-Tool Relationship):

   • 비유: "이 요리를 하려면 먼저 국물을 끓여야 합니다"라고 순서를 명시해야 합니다.
   • 효과: AI 가 순서를 잘못 섞어 실수하는 것을 방지합니다.

4. 결론: 수학적 보장이 있는 AI 시대

이 논문의 핵심 메시지는 **"AI 가 도구를 쓰는 방식을 임의의 규칙이 아니라, 수학적으로 검증 가능한 안전 시스템으로 바꿔야 한다"**는 것입니다.

• MCP+ 를 적용하면: AI 와 도구 사이의 소통이 완벽한 번역이 되어, 어떤 상황에서도 AI 가 안전하게 행동함을 수학적으로 증명할 수 있게 됩니다.
• 미래: 은행, 병원, 교통 시스템 등 중요한 분야에서 AI 가 일할 때, "이게 안전할까?"라고 걱정하지 않아도 되는 신뢰할 수 있는 AI 시스템의 기초를 닦은 것입니다.

한 줄 요약:

"AI 가 도구를 쓸 때 생길 수 있는 오해를 없애기 위해, 도구의 설명서에 안전 수칙, 비상 계획, 작동 순서를 수학적으로 완벽하게 적어주는 새로운 표준을 만들었습니다."

기술 요약

이 논문은 대규모 언어 모델 (LLM) 에이전트가 외부 도구를 호출하는 프로토콜의 형식적 검증 (Formal Verification) 에 대한 필요성을 제기하고, **프로세스 계산 (Process Calculus)**을 기반으로 한 **Schema-Guided Dialogue (SGD)**와 **Model Context Protocol (MCP)**의 형식적 의미론을 제시합니다.

저자 Andreas Schlapbach 은 두 프로토콜 간의 구조적 동등성을 증명하고, MCP 의 표현력 부족을 보완하기 위한 5 가지 원칙을 도출하여 확장된 프로토콜 **MCP+**를 제안합니다.

주요 내용은 다음과 같습니다.

---

1. 문제 제기 (Problem)

• 배경: LLM 에이전트가 복잡한 워크플로우를 위해 외부 도구를 동적으로 호출하는 환경이 급속히 확산되고 있습니다.
• 현황: 에이전트 - 도구 통합을 위한 두 가지 주요 패러다임이 존재합니다.
  1. SGD (Schema-Guided Dialogue): 연구 중심 프레임워크로, 런타임에 자연어 스키마를 통해 제로샷 (zero-shot) API 일반화를 가능하게 합니다.
  2. MCP (Model Context Protocol): Anthropic 이 제안한 산업 표준으로, 호스트와 서버 간의 표준화된 원시적 (primitives) 연결을 제공합니다.
• 결함: 두 패러다임은 개념적으로 유사하지만, 그 형식적 관계는 규명되지 않았습니다. 에이전트의 안전성, 정확성, 행동 속성을 수학적으로 검증할 수 있는 방법이 부재하며, 현재는 테스트나 프롬프트 엔지니어링에 의존하여 불완전한 커버리지와 취약성을 안고 있습니다.

2. 방법론 (Methodology)

• π-계산 (π-calculus) 적용: 동적이고 통신하는 시스템을 모델링하는 데 적합한 π-계산을 사용하여 SGD 와 MCP 를 형식화했습니다.
• 구문 및 운영 의미론 정의: 두 프로토콜에 대한 상태, 전이 규칙 (transition rules), 레이블 전이 시스템 (LTS) 을 정의했습니다.
• 이중 시뮬레이션 (Bisimulation) 분석:
  • 순방향 매핑 ($\Phi$): SGD 를 MCP 로 매핑하여 구조적 동등성을 증명했습니다.
  • 역방향 매핑 ($\Phi^{-1}$) 분석: MCP 를 SGD 로 역매핑할 때 발생하는 정보 손실 (lossy) 과 부분성 (partiality) 을 규명했습니다.
• 타입 시스템 확장: 발견된 격차를 메우기 위해 5 가지 설계 원칙을 타입 시스템 확장으로 형식화하여 **MCP+**를 정의했습니다.

3. 주요 기여 (Key Contributions)

1. SGD 와 MCP 의 첫 번째 형식적 의미론: π-계산을 기반으로 두 프로토콜의 구문과 운영 의미론을 정의했습니다.
2. 구조적 동등성 증명: 매핑 $\Phi$ 하에서 SGD 와 MCP 가 이중 시뮬레이션 (bisimilar) 임을 증명했습니다 ($SGD \sim MCP$).
3. 역방향 매핑의 한계 규명: $\Phi^{-1}$이 부분적이고 정보 손실이 발생함을 증명했습니다. 특히 MCP 는 거래성 플래그 (transactionality flag), 자원 (Resource), 프롬프트 (Prompt) 등의 개념이 SGD 와 매핑되지 않아 표현력이 제한됨을 보였습니다.
4. 5 가지 설계 원칙 도출: 완전한 행동 동등성을 위해 필수적인 5 가지 원칙을 제시했습니다.
   1. 의미적 완전성 (Semantic Completeness): 파라미터의 존재 이유를 설명하는 고밀도 설명.
   2. 명시적 행동 경계 (Explicit Action Boundaries): 사이드 이펙트 (쓰기/삭제) 발생 시 승인 필요성 명시.
   3. 실패 모드 문서화 (Failure Mode Documentation): 예상 오류 및 복구 전략 명시.
   4. 점진적 공개 호환성 (Progressive Disclosure Compatibility): 토큰 효율성을 위한 요약 및 상세 설명 분리.
   5. 도구 간 관계 선언 (Inter-Tool Relationship Declaration): 도구 간 의존성 (예: A 실행 후 B 실행) 명시.
5. MCP+ 와 완전 동등성: 위 5 가지 원칙을 적용한 확장된 프로토콜 **MCP+**가 SGD 와 완전한 전단사 (bijection) 관계에 있음을 증명 ($MCP+ \cong SGD$) 했습니다.
6. 보안 속성의 프로세스 불변성: 권한 제한, 도구 중독 방지, 승인 순서 보장 등을 형식적으로 검증 가능한 속성으로 정의했습니다.

4. 연구 결과 (Results)

• 동등성: SGD 는 MCP 로 매핑 가능하지만, 기존 MCP 는 SGD 의 모든 특성 (특히 거래성, 의존성, 자원 관리) 을 포착하지 못합니다.
• 격차 분석: MCP 는 수동적인 컨텍스트 (Resource) 나 런타임 능력 협상 (Capability Negotiation) 을 지원하지만, SGD 는 이를 지원하지 않습니다. 반대로 SGD 는 명시적인 거래성 플래그를 가지지만, MCP 스키마에는 이를 기계적으로 읽을 수 있는 필드가 없습니다.
• 해결책: 5 가지 원칙을 적용한 **MCP+**는 SGD 와 완전히 동등한 표현력을 가지며, 에이전트 시스템의 안전성을 수학적으로 보장할 수 있는 기반을 마련했습니다.
• 보안 검증: 형식적 모델을 통해 "승인 없이 쓰기/삭제 작업이 수행되지 않음"이나 "의존 도구 실행 순서가 보장됨"과 같은 보안 속성을 프로세스 불변성으로 증명할 수 있음을 보였습니다.

5. 의의 및 중요성 (Significance)

• 형식적 검증의 토대 마련: LLM 에이전트 시스템의 안전성과 정확성을 검증하기 위한 최초의 수학적 기반을 제공했습니다.
• 스키마 품질의 증명 가능한 속성: 스키마의 품질이 단순한 휴리스틱이 아닌, 타입 시스템으로 검증 가능한 속성으로 격상되었습니다.
• Software 3.0 의 안전성 보장: 자율 에이전트가 금융, 의료, 인프라 등 중요한 영역에서 동적으로 도구를 조율하는 'Software 3.0' 시대에, 임의의 관행이 아닌 검증 가능한 안전한 시스템으로 발전할 수 있는 방향을 제시합니다.
• 미래 연구 방향: 기계 증명 (Mechanized proofs), 확률적 이중 시뮬레이션, 멀티 에이전트 choreography, 모델 체킹 등을 통한 확장 가능성을 제시했습니다.

결론적으로, 이 논문은 SGD 와 MCP 의 개념적 수렴을 형식적으로 증명하고, MCP 의 표현력 한계를 보완하여 에이전트 프로토콜의 안전성을 수학적으로 보장할 수 있는 **MCP+**를 제안함으로써, AI 에이전트 시스템의 신뢰성 확보에 중요한 이정표를 세웠습니다.