당신이 수천 개의 레고 브릭으로 거대하고 복잡한 성을 쌓고 있다고 상상해 보세요. 당신은 어떻게 쌓더라도 탑이 무너지지 않고, 비밀 문 때문에 안에 갇히는 일이 없도록 만들고 싶습니다. 컴퓨터 과학의 세계에서 이 "성"은 우리 은행, 병원, 그리고 인터넷을 실행하는 복잡한 소프트웨어입니다. 이 성이 안전한지 알려주는 "설계도"를 **형식 명세(formal specifications)**라고 부릅니다. 이것은 소프트웨어가 정확히 어떻게 동작해야 하는지를 설명하는 초정밀 수학적 규칙책과 같습니다. 수십 년 동안 이 규칙책을 쓰는 것은 마치 소수의 천재들만 사용하는 언어로 소설을 쓰는 것과 같았습니다. 전문가들이 몇 달 동안 엄청난 노력을 들여야 했고, 만약 아주 작은 실수라도 하나 저지르면 전체가 쓸모없게 되었습니다.

최근에 AI 에이전트라고 불리는 새로운 종류의 "로봇 작가"가 등장했습니다. 이들은 코드(code)를 읽고 새로운 코드를 쓸 수 있는 대규모 언어 모델(챗봇 뒤에 있는 기술과 동일한 기술)을 기반으로 하는 컴퓨터 프로그램입니다. 사람들은 이 로봇들이 우리 대신 규칙책을 써주어 시간과 노력을 아껴주기를 기대했습니다. 하지만 함정이 있었습니다. 이 로봇들은 "환각(hallucinations)"(내용을 지어내는 것)과 "보상 해킹(reward hacking)"(실제로 맞지는 않으면서 잘한 것처럼 속이는 것)을 저지르기 쉽다는 점입니다. 이들은 서류상으로는 완벽해 보이지만 실제 레고 브릭과는 일치하지 않는 성을 설명하는 규칙책을 작성할 수도 있습니다. 큰 질문은 이것입니다: 인간 전문가가 손을 잡아주지 않아도, AI가 복잡한 시스템의 안전 매뉴얼을 작성하는 것을 믿을 수 있을까요?

여기 Specula라는 새로운 시스템이 있습니다. 이는 마치 초스마트하고 자기 수정 능력을 갖춘 로봇 팀처럼 작동합니다. 단순히 AI에게 "규칙책을 써라"라고 요청하는 대신, Specula는 AI를 '행동하고, 실패하고, 다시 시도하며 배우는 호기심 많은 견습생'으로 취급합니다. 이 시스템은 로봇이 규칙책을 쓰고, 실제 코드와 대조하여 확인하고, 실수를 찾아낸 뒤, 자신의 이해도를 스스로 수정하는 영리한 루프를 사용합니다. 연구진은 이 시스템이 48개의 서로 다른 복잡한 소프트웨어 프로젝트에 대해 고품질의 규칙책을 자율적으로 생성할 수 있다는 것을 발견했습니다. 이 시스템은 단순히 뻔한 오류를 찾아낸 것이 아니라, 249개의 버그를 찾아냈으며, 그중 89개는 개발자들에게 보고되었고, 68개가 확인되었으며 24개가 이미 수정되었습니다. 가장 중요한 점은, 이 시스템이 초기 규칙책을 작성하는 데 인간 전문가의 도움 없이도 이러한 버그들을 찾아냈다는 것이며, 이는 우리가 AI에게 자신의 실수를 통해 배울 수 있는 적절한 도구를 제공하기만 한다면 AI를 사용하여 소프트웨어의 안전 점검을 확장할 수 있음을 증명합니다.

Specula의 이야기: 생각하는 법을 배우는 로봇 탐정

당신이 잠들지 않는 도시에서 미스터리를 풀려는 탐정이라고 상상해 보세요. 그 도시는 복잡한 소프트웨어이고, 미스터리는 "도시를 붕괴시킬 숨겨진 함정은 어디에 있는가?"입니다. 과거에는 전문가 팀이 도시의 지도(형식 모델)를 그리고 도시가 어떻게 작동하는지에 대한 규칙(불변량, invariants)을 적어야 했습니다. 이는 몇 달이 걸렸습니다. 이제 당신에게 로봇 탐정이 있다고 상상해 보세요. 당신은 "좋아! 로봇에게 지도를 그리라고 하면 되겠군"이라고 생각할지도 모릅니다. 하지만 문제는 여기 있습니다. 만약 당신이 로봇에게 그냥 지도를 그리라고 명령한다면, 로봇은 실제 거리와는 맞지 않는, 마치 만화처럼 아름답기만 한 도시를 그릴 수도 있습니다. 존재하지 않는 다리를 만들어내거나, 충돌을 일으키는 신호등을 잊어버릴 수도 있습니다. 이것이 AI가 스스로 형식 명세를 작성하려고 할 때 발생하는 문제입니다. 즉, "분위기"는 맞추지만 세부 사항은 틀리는 것입니다.

Specula는 이 문제에 대한 해결책입니다. 이것은 단순히 지도를 그리는 로봇이 아니라, 엄격하고 자기 수정적인 훈련 프로그램을 가진 로봇입니다. 이것을 비디오 게임처럼 생각해보세요. 로봇은 설계사 역할을 수행하지만, 벽을 하나 세울 때마다 "심판"이 그 벽이 실제 코드에 존재하는지 확인합니다. 만약 벽이 가짜라면, 로봇은 그 벽을 허물고 다시 시도해야 합니다.

로봇 팀의 작동 방식

Specula 시스템은 협력하는 전문화된 로봇 팀과 같습니다:

1. 호기심 많은 독자: 먼저, 로봇은 소프트웨어 코드, 문서, 심지어 버그 보고서(마치 도시의 역사서를 읽는 것과 같습니다)까지 읽습니다. 그리고 도시의 규칙을 추측합니다. 예를 들어, "메시지가 전송되면 반드시 수신되어야 한다"라고 추측할 수 있습니다. 이것을 **불변량(invariant)**이라고 부릅니다.
2. 설계사: 다음으로, 로봇은 **TLA+**라고 불리는 특수한 언어를 사용하여 도시의 단순화된 모델을 구축합니다. 이 모델은 (벽돌의 색깔 같은) 사소한 세부 사항은 무시하지만 (교통 흐름 같은) 중요한 부분은 유지하는 청사진과 같습니다.
3. 현실 검증 (Trace Validation): 이 단계가 가장 중요합니다. 로봇은 청사진을 가져와 실제 코드와 비교합니다. 로봇은 코드를 실행하고 "트레이스(trace)"(코드가 실제로 수행하는 일을 기록한 영상)를 기록합니다. 그런 다음 다음과 같이 확인합니다: "내 청사진이 이 영상을 허용하는가?" 만약 청사진은 "예, 이것은 가능합니다"라고 말하는데 영상은 불가능한 상황을 보여준다면, 청사진이 틀린 것입니다.
4. 자기 수정 루프: 만약 청사진이 틀렸다면, 로봇은 그냥 포기하지 않습니다. 로봇은 "이 부분을 놓쳤습니다!" 또는 "실제와 다른 규칙을 만들었습니다!"라는 힌트를 얻습니다. 그러면 로봇은 다시 돌아가 코드를 다시 읽고 자신의 청사진을 수정합니다. 로봇은 "아, 나는 신호등이 초록색이라고 생각했는데, 코드는 빨간색이라고 말하고 있구나"라고 깨달을 수 있습니다. 로봇은 청사진이 실제 코드의 현실과 완벽하게 일치할 때까지 이 과정을 반복합니다.
5. 버그 사냥꾼: 청사진이 완벽해지면, 로봇은 "모델 체커(model checker)"(초고속 시뮬레이터)를 사용하여 청 blueprint 내의 모든 가능한 시나리오를 실행합니다. 로봇은 규칙이 깨지는 모든 상황을 찾습니다. 만약 규칙 위반을 발견하면, 단순히 "오류"라고 말하는 데 그치지 않습니다. 로봇은 실제 코드로 돌아가서 정확히 어떤 순간에 충돌이 발생했는지 재현하려고 시도하며, 추상적인 오류를 개발자가 보고 수정할 수 있는 실제 재현 가능한 테스트 케이스로 변환합니다.

위대한 실험

연구진은 48개의 서로 다른 오픈 소스 소프트웨어 프로젝트를 대상으로 Specula를 테스트했습니다. 이들은 단순한 프로그램이 아니었습니다. MongoDB(데이터베이스), GCC libgomp(병렬 컴퓨팅 도구), 그리고 다양한 Raft 구현체(컴퓨터 간의 동기화를 유지하는 프로토콜)와 같은 복잡한 시스템들이었습니다. 이 시스템들은 C++, Go, Rust, Java와 같은 언어로 작성되었습니다.

결과는 인상적이었습니다. Specula는 총 249개의 버그를 찾아냈습니다.

• 207개는 아무도 몰랐던 새로운 버그였습니다.
• 42개는 아직 수정되지 않은 알려진 버그였습니다.
• 팀은 이 중 89개의 버그를 개발자들에게 보고했습니다.
• 현재까지 68개가 실제 버그로 확인되었으며, 24개가 이미 수정되었습니다.

Specula의 가장 멋진 점 중 하나는 단순히 간단한 실수를 찾아낸 것이 아니라는 점입니다. Specula는 매우 구체적이고 드문 방식으로 문제가 발생하는 "깊은(deep)" 버그들을 찾아냈습니다. 예를 들어, libgomp라는 라이브러리에서 Specula는 최소 5년 동안 코드 속에 숨어 있던 데드락(deadlock)(프로그램이 영원히 멈춰버리는 상황)을 찾아냈습니다. 이 버그는 특정 스레드가 아주 정확하게 잘못된 순간에 깨어날 때만 발생했습니다. 인간 테스터는 이런 상황을 거의 잡을 수 없는데, 이는 마치 모래 폭풍 속에서 떨어지는 특정 모래알 하나를 잡으려는 것과 같기 때문입니다. 하지만 Specula의 모델 체커는 모래가 떨어질 수 있는 모든 가능한 경로를 살펴보고, 충돌을 일으킨 바로 그 지점을 찾아냈습니다.

또 다른 예는 데이터 센터에서 사용되는 네트워크 운영 체제인 SONiC에서 나왔습니다. Specula는 두 스위치가 상태를 업데이트하는 방식의 아주 작은 오류 때문에 시스템이 서로의 조율을 멈추게 되는 버그를 찾아냈습니다. 이 버그는 너무 미묘해서 프로젝트 자체 테스트에서도 잡아내지 못했습니다.

이것이 왜 중요한가 (그리고 왜 마법이 아닌가)

당신은 "왜 그냥 AI에게 코드를 직접 쓰라고 하지 않았나요?"라고 물을 수 있습니다. 논문은 단순히 AI에게 형식 명세를 쓰라고 요구하는 것이 함정이라고 주장합니다. 만약 단순히 AI에게 "규칙책을 써라"라고 요청한다면, AI는 속임수를 쓸 수 있습니다. AI는 너무 모호하거나 너무 쉬운 규칙책을 작성하여, 모든 테스트를 통과할 수는 있지만 실제 시스템을 제대로 설명하지는 못할 수도 있습니다. 이것을 **보상 해킹(reward hacking)**이라고 합니다.

Specula는 AI에게 자신의 작업을 증명하도록 강제함으로써 이 문제를 해결합니다. 이 시스템은 "자기 진화 루프(self-evolving loop)"를 사용합니다. 만약 AI가 실수를 하면, 시스템이 이를 포착하여 AI가 배우도록 만듭니다. 연구진은 이 루프가 필수적이라는 것을 발견했습니다. 테스트에서 시스템은 **60.5%**의 경우 모델을 수리해야 했고, **22.2%**의 경우 코드 인스트루멘테이션(instrumentation)을 수정해야 했으며, **17.3%**의 경우 규칙(불변량)을 개정해야 했습니다. 이 루프가 없었다면 AI는 유용하게 쓰일 수 없을 만큼 너무 많은 실수를 저질렀을 것입니다.

또한 논문은 AI의 "품질"이 중요하다는 것을 보여줍니다. 연구진은 다양한 버전의 AI(Claude Opus, Sonnet, Haiku)로 Specula를 테스트했습니다. 가장 강력한 버전(Opus)은 62개의 버그를 찾아냈습니다. 약간 약한 버전(Sonnet)은 10개만을 찾아냈습니다. 가장 약한 버전(Haiku)은 하나도 찾지 못했습니다. 이는 시스템(Specula)이 강력하더라도, 제대로 작동하기 위해서는 여전히 스마트한 AI의 두뇌가 필요하다는 것을 말해줍니다. 이는 마치 훌륭한 자동차(Specula)를 가지고 있어도 목적지에 도달하려면 숙련된 운전자(AI)가 필요하다는 것과 같습니다.

안전의 비용

이것이 비싼가요? 연구진은 Specula를 시스템에 실행하는 데 1.43시간에서 9.86시간이 걸렸으며, 컴퓨팅 파워(토큰 비용) 비용은 $19에서$168 사이가 들었다고 계산했습니다. 무료 도구에 비해 이 금액이 많아 보일 수 있지만, 논문은 인간 전문가가 유사한 규칙책을 수작업으로 작성하는 데 몇 달이 걸린다는 점을 지적합니다. 따라서 거시적인 관점에서 볼 때, 이것은 사실 매우 저렴한 편입니다.

논문은 이것이 모든 것을 해결하는 "마법 지팡이"는 아니라고 신중하게 밝히고 있습니다. 이 시스템은 여전히 AI가 코드를 읽는 것에 의존하며, 만약 AI가 코드의 큰 부분을 놓친다면 모델이 불완전할 수 있습니다. 그러나 Specula의 "자기 진화적" 특성은 설령 AI가 실수를 하더라도 시스템이 이를 포착하고 수정하도록 설계되어 있어, 단순히 AI에게 규칙을 "추측"하게 하는 것보다 훨씬 더 신뢰할 수 있게 만듭니다.

결국, Specula는 우리가 소프트웨어를 안전하게 유지하기 위해 형식 수학의 전문가가 될 필요가 없는 미래를 보여줍니다. 우리가 AI에게 자신의 실수를 확인하고, 실수를 교정하며, 결코 속임수를 쓰도록 내버려 두지 않는 적절한 도구를 제공하기만 한다면, AI를 활용해 힘든 일을 맡길 수 있습니다. 이는 우리의 디지털 성이 단순히 보기 좋은 것이 아니라, 완벽하게 정확한 청사진을 바탕으로 구축되는 세상을 향한 한 걸음입니다.