MAGS: 에이전트 출력 안전성을 보장하는 다중 에이전트 자동 형식화
MAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs
arXivLLM 코딩 에이전트의 복잡한 코드 안전성 확보는 큰 난제입니다. 연구진은 다중 에이전트 자동 형식화 프레임워크 MAGS를 제시하여 이 문제를 해결했습니다.
- MAGS는 코드를 형식 검증 언어(Dafny)로 변환하고, 명시된 안전 요구사항을 기계적으로 확인하며 오류를 수정합니다. 테스트 결과 220개 예제에서 높은 안전성을 가진 프로그램을 성공적으로 생성했습니다.
- 이 방법론은 사람이 직접 명세화하기 어려웠던 CUDA 커널이나 로봇 공학 등 다양한 고난도 분야의 코드까지 검증할 수 있는 기반을 마련했다는 점에서 주목됩니다.
- 다만, 시스템의 안전 속성을 자동으로 형식화하는 과정에서 실제 목표 행동이나 복잡한 의도를 완벽히 담아내지 못하면 오류가 발생할 수 있다는 한계가 있습니다.
코딩 가 생성하는 복잡한 프로그램은 안전성 및 보안 실패 위험을 높여 인간의 검토만으로는 한계에 부딪힙니다. 기존의 퍼즈 테스트, 정적 분석, 또는 LLM 기반 검증자 접근법 등도 모든 엣지 케이스를 다루기 어렵습니다. 이에 연구진은 형식적인 안전 보장을 제공하는 통합 다중 에이전트 프레임워크인 MAGS(Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs)를 제안했습니다.
MAGS는 Dafny를 검증 인식 중간 표현으로 사용하여 실행 가능한 프로그램에 형식적 안전 보장을 부여합니다. 이 과정에서 사람이 감사한 와 안전 요구사항을 형식화하고 고정하며, 생성된 코드를 Dafny로 변환하고, 검증기 피드백을 이용해 위반 사항을 수리한 후, 최종적으로 검증된 프로그램을 실행 가능한 코드로 컴파일하는 과정을 거칩니다.
MAGS는 100개의 커널, 100개의 터미널 스크립트, 그리고 20개의 로봇 팔 작업 등 총 220개 예제에 대해 평가되었습니다. 이 모든 예제에서 비자명한 안전 보장을 가진 프로그램을 생성하는 데 100%의 성공률을 달성했습니다. 다만, 독립적인 평가 결과, 자동 형식화된 의미론이 목표 행동이나 복잡한 의도를 완전히 포착하지 못할 경우 실패가 발생한다는 점도 확인되었습니다.
용어 풀이
- LLM
- 방대한 글을 학습해 문장을 이해하고 만들어 내는 AI 모델. ChatGPT, Claude, Gemini가 여기에 속해요.
- 에이전트
- 목표를 받으면 스스로 계획을 세우고 도구를 써서 여러 단계의 작업을 해내는 AI.
- API
- 프로그램끼리 기능을 주고받는 약속된 창구. AI 모델은 보통 API로 불러 써요.
- CUDA
- 엔비디아 GPU에서 계산 프로그램을 돌리게 해 주는 개발 플랫폼.