최근 대규모 언어모델(LLM) 기반의 코딩 에이전트들이 복잡한 프로그램을 대규모로 생성하면서, 이를 사람이 일일이 검토하기가 점점 어려워지고 있습니다. 이는 잠재적인 안전 및 보안 결함으로 이어질 수 있어 심각한 문제로 인식되고 있습니다. 기존의 퍼즈 테스팅(fuzz testing), 정적 분석(static analysis), 또는 LLM 기반 검증(LLM-as-a-Verifier) 같은 방법들은 많은 오류를 찾아내지만, 모든 예외 상황(edge cases)을 완벽하게 커버하는 데는 한계가 있었습니다.
이러한 문제를 해결하기 위해 'MAGS(Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs)'라는 새로운 다중 에이전트 프레임워크가 등장했습니다. MAGS는 형식 검증(formal verification)이라는 접근 방식을 활용합니다. 형식 검증은 특정 속성에 대해 기계적으로 검증 가능한 보증을 제공하지만, 기존에는 상당한 수동 사양 정의와 증명 엔지니어링이 필요했습니다. MAGS는 이 과정을 자동화하여, 인간이 감사한 API와 안전 요구사항을 형식화하고, 생성된 코드를 Dafny와 같은 검증 가능한 중간 표현(intermediate representation)으로 변환합니다. 이후 검증기 피드백을 통해 위반 사항을 자동으로 수정하고, 검증된 프로그램을 다시 실행 가능한 코드로 컴파일합니다.
연구팀은 MAGS를 100개의 CUDA 커널, 100개의 터미널 스크립트, 20개의 로봇 팔 작업 등 총 220가지 예제에 적용했습니다. 그 결과, 모든 예제에서 지정된 안전 사양에 대해 100% 성공률로 안전 보장이 되는 프로그램을 생성하는 데 성공했습니다. 이는 AI가 생성한 코드의 신뢰성을 획기적으로 높일 수 있음을 보여줍니다. MAGS는 개발자가 AI 생성 코드의 안전성을 확신하고 실제 시스템에 더 폭넓게 적용할 수 있도록 돕는 중요한 진전이며, 복잡한 시스템의 안정성과 보안을 강화하는 데 기여할 것으로 기대됩니다.