OpenShell, 형식 기법으로 AI 에이전트의 권한 이탈을 수학적으로 증명하다
What we have learned at OpenShell applying formal methods to control AI agents
AI 에이전트가 수백 시간 동안 자율적으로 작동하면 기존 권한 검토가 무너진다. OpenShell 팀은 Z3 SMT 솔버를 활용해 에이전트가 제안한 정책 변경이 사전 승인된 범위를 벗어나지 않음을 형식적으로 증명하는 방법을 연구했다. 이 접근은 밀리초 단위로 결정적 검증을 제공하며, 토큰 비용 없이 감사 추적을 남긴다. 확률적 AI 검토자의 한계를 보완하는 강력한 도구다.
AI 모델은 인간과 마찬가지로 확률적이어서 중요한 세부 사항을 놓칠 수 있다. 게다가 모든 에이전트 행동을 동일한 지능의 검토 모델로 검토하면 컴퓨팅 비용이 두 배로 늘고 토큰 처리량은 사실상 절반으로 줄어든다.