당신이 마법 같고 스스로 교정되는 벽돌 세트로 집을 짓고 있다고 상상해 보세요. 이 벽돌들은 "Rust"라고 불리며, 불안정한 것을 짓지 못하도록 막아서는 내장된 안전 검사관으로 유명합니다. 만약 당신이 벽이 있어야 할 자리에 창문을 놓으려고 하면, 검사관은 "안 돼!"라고 비명을 지르며 첫 번째 돌을 놓기도 전에 당신을 멈춰 세웁니다. 이 덕분에 Rust는 소프트웨어를 구축할 때 매우 안전하며, 문제가 발생하기 전에 크래시나 보안 취약점을 방지합니다. 하지만 때때로 숙련된 건축가는 무거운 빔을 빠르게 옮기기 위해 특수한 위험한 도구를 사용하는 것처럼, 검사관이 이해하지 못하는 일을 해야 할 때가 있습니다. Rust의 세계에서 이것은 "unsafe code(안전하지 않은 코드)"라고 불립니다. 이것은 검사관을 우회할 수 있는 비밀 통패스 같은 것이지만, 그에 따른 대가가 매우 큽니다. 단 하나의 실수만 해도 집 전체가 무너질 수 있기 때문입니다. 집을 계속 세워두기 위해서는, 이 위험한 도구들을 어떻게 안전하게 사용하는지 정확하게 증명하는 매우 엄격한 수학적 "규칙서(specification)"를 작성해야 합니다. 하지만 이러한 규칙서를 손으로 쓰는 것은 매우 어렵고, 느리며, 인간의 실수에 취약합니다.

여기서 KaPilot의 이야기가 시작됩니다. 이 프로젝트의 연구진은 간단한 질문을 던졌습니다. "우리가 이 똑똑한 컴퓨터 두뇌(AI)에게 우리 대신 이 안전 규칙서를 쓰도록 가르칠 수 있을까?" 문제는 이 AI들이 코드를 작성하는 데는 뛰어나지만, 코드에 담긴 '의도'를 이해하기보다는 그들이 보는 코드의 실수를 그대로 복사하는 경향이 있다는 점입니다. 그들은 완벽해 보이는 규칙서를 작성할 수도 있지만, 아주 작고 치명적인 세부 사항을 놓칠 수 있습니다. 이 논문은 이 퍼즐을 풀기 위해 함께 협력하는 AI 에이전트 팀인 KaPilot을 제시합니다. 단순히 AI에게 "규칙을 써라"라고 요청하는 대신, KaPilot은 탐정, 작가, 그리고 엄격한 편집자 역할을 모두 수행합니다. 그것은 설계자의 노트(문서)를 읽고, 진정한 안전 규칙을 추출하고, 초안을 작성하고, 구멍이 있는지 확인한 다음, 실제로 작동하는지 확인하기 위해 엄격한 테스트를 거칩니다. 그 결과, 이 시스템은 인간 전문가의 도움 없이도 위험한 코드를 위한 고품질의 안전 규칙을 자동으로 생성할 수 있게 해줍니다.

탐정, 작가, 그리고 편집자

unsafe Rust 코드를 검증하는 과정을 브레이크가 없는 고속 레이싱 카를 위한 완벽한 사용 설명서를 쓰는 과정이라고 생각해 보세요. 설명서가 틀리면 차는 충돌합니다. 설명서가 너무 모호하면 운전자가 운전을 할 수 없습니다. 설명서가 너무 엄격하면 운전자가 움직일 수 없습니다.

KaPilot은 멀티 에이전트 프레임워크인데, 이는 단순히 전문화된 AI 캐릭터들이 협력하는 팀이라는 뜻입니다. 이들이 역할을 수행하는 방식은 다음과 같습니다:

1. 탐정 (SafetyReq): 무엇을 쓰기 전에, 팀은 규칙이 무엇이어야 하는지 알아야 합니다. 보통 이러한 규칙은 코드와 함께 제공되는 무질서한 인간 작성 노트(문서) 속에 숨겨져 있습니다. "SafetyReq" 에이전트는 탐정처럼 행동합니다. 이 에이전트는 노트를 읽고, 군더더기를 무시하며, 깨끗하고 간결한 안전 요구 사항 목록을 추출합니다. 이는 "빨간 버튼을 만지지 마세요"라는 두서없는 이야기를 "1. 빨간 버튼을 누르지 마십시오. 2. 빨간 버튼으로부터 5피트 이내에 서 있지 마십시오."와 같은 명확한 번호가 매겨진 목록으로 바꾸는 것과 같습니다. 이 단계는 AI가 코드의 실수를 단순히 복사하는 것을 방지하기 때문에 매우 중요합니다.
2. 작가 (SpecGenerate): 탐정이 목록을 만들면, "SpecGenerate" 에이전트가 투입됩니다. 이 에이شن은 그 목록을 컴퓨터가 이해할 수 있는 공식적인 수학적 언어(구체적으로 Kani라고 불리는 언어)로 바꾸는 작가입니다. 이 에이전트는 단순히 추측하는 것이 아니라, 탐정의 목록을 엄격한 가이드로 사용합니다.
3. 편집자 (SpecPrecheck): 작가의 초안이 최종 보스에게 가기 전에, "SpecPrecheck" 에이전트가 이를 검토합니다. 이 에이전트는 "탐정이 찾은 모든 점을 다 다루었는가? 문장이 너무 약한가? 아니면 너무 강한가?"라고 묻는 엄격한 편집자입니다. 만약 초안이 엉성하다면, 편집자는 수정 방법에 대한 구체적인 메모와 함께 작가에게 초안을 돌려보냅니다. 초안이 탄탄해질 때까지 이 과정은 반복됩니다.
4. 테스트 드라이버 (SpecVerify): 마지막으로, "SpecVerify" 에이전트는 초안을 가져가 실제 환경 테스트를 수행합니다. 이 에이전트는 Kani라는 도구를 사용하여 수백만 가지의 서로 다른 주행 시나리오를 시뮬레이션하여 차가 충돌하는지 확인합니다. 만약 차가 충돌한다면(검증 실패), 테스트 드라이버는 작가에게 정확히 왜 충돌했는지 알려주고 루프는 다시 시작됩니다.

"셔플 앤 믹스(Shuffle and Mix)" 전략

여기서 팀은 정말 영리해집니다. 때때로 AI는 몇 가지 다른 버전의 규칙서를 생성합니다. 어떤 버전은 완벽한 "시작" 조건(precondition)을 가졌지만 약한 "종료" 조건(postcondition)을 가질 수 있습니다. 또 다른 버전은 약한 시작을 가졌지만 완벽한 종료를 가질 수 있습니다. 만약 하나만 선택한다면, 최상의 조합을 놓칠 수 있습니다.

KaPilot은 **"셔플 앤 임플리케이션(shuffle-and-implication)"**이라 불리는 전략을 사용합니다. 각기 다른 규칙서의 부분을 담고 있는 카드 덱이 있다고 상상해 보세요. 팀은 이 카드들을 섞어서, 한 버전의 가장 좋은 "시작" 부분과 다른 버전의 가장 좋은 "종료" 부분을 결합합니다. 그런 다음 이 새로운 조합들을 테스트하여 원래의 초안들보다 더 잘 작동하는지 확인합니다. 이것은 마치 한 자동차의 엔진과 다른 자동차의 타이어를 가져와 궁극의 레이싱 카를 만드는 것과 같습니다. 이를 통해 그들은 단순히 "적당한" 규칙서에 안주하는 것이 아니라, 최상의 규칙서를 찾아낼 수 있습니다.

연구 결과

연구진은 124개의 서로 다른 unsafe Rust 코드를 대상으로 KaPilot을 테스트했습니다. 이들은 두 그룹으로 나누었습니다:

• 골드 세트 (Gold Set, 54개 함수): 인간 전문가가 작성한 "그라운드 트루스(ground truth)" 규칙서가 있어, 팀이 KaPilot의 작업이 정확한지 확인할 수 있었습니다.
• 울트라 세트 (Ultra Set, 70개 함수): 인간의 규칙서가 없으므로, 팀은 KaPilot이 작동하는 규칙서를 생성할 수 있는지만 확인했습니다.

결과는 인상적이었습니다. 골드 세트의 경우, KaPilot은 **88.9%**의 함수에 대해 작동하는 규칙서를 성공적으로 생성했습니다. 더욱 중요한 점은, **57.4%**의 경우에 KaPilot이 작성한 규칙서가 인간 전문가가 작성한 것만큼 좋거나 혹은 더 좋았다는 것입니다. 울트라 세트의 경우, 작동하는 규칙서를 **71.4%**의 함수에 대해 만들어냈습니다.

KaPilot을 이 시스템에 맞춰 조정된 AutoSpec이라는 다른 AI 도구와 비교했을 때, KaPilot이 압도적인 승리를 거두었습니다. KaPilot은 테스트를 통과하는 규칙서를 14.8% 더 많이 생성했으며, 인간이 작성한 것과 의미론적으로 동일하거나 더 나은 규칙서를 25.9% 더 많이 생성했습니다.

이것이 왜 중요한가

이 논문은 단순히 AI에게 "이 코드를 바탕으로 안전 규칙을 써라"라고 요청하는 것이 효과적이지 않다고 주장합니다. AI는 코드의 결함을 복사하거나 복잡함에 혼란을 느끼는 경향이 있기 때문입니다. 작업을 전문화된 팀(문서를 읽는 역할, 쓰는 역할, 편집하는 역할, 테스트하는 역할)으로 나눔으로써, KaPilot은 이러한 함정을 피합니다.

연구진은 또한 인간의 노트(문서)의 품질이 매우 중요하다는 것을 발견했습니다. 노트가 모호하면 AI는 어려움을 겪습니다. 하지만 노트가 명확할 때 KaPilot은 빛을 발합니다. 또한 그들은 "셔플" 전략이 핵심 요소임을 발견했습니다. 이 전략이 없다면 시스템은 완벽한 규칙의 조합을 찾는 대신 평범한 해결책에 머물렀을 것입니다.

요약하자면, KaPilot은 우리가 인간의 전문성과 AI의 속도 중 하나를 선택할 필요가 없음을 시사합니다. 엄격하고 논리적인 프로세스를 따르는 전문화된 조수 팀으로서 AI를 활용함으로써, 우리는 가장 위험한 소프트웨어 부분에 대한 안전 규칙 생성을 자동화하여 디지털 세상을 더 안전하게 만들 수 있습니다. 이 논문은 이것이 모든 문제를 해결한다고 주장하는 것은 아니지만(복잡한 루프는 여전히 인간의 도움이 필요합니다), 이 멀티 에이전트 접근 방식이 소프트웨어 검증을 자동화하고 신뢰할 수 있게 만드는 거대한 진전임을 입증합니다.