당신이 똑똑한 로봇에게 이야기를 쓰는 법을 가르치고 있다고 상상해 보세요. 당신은 로봇에게 프롬프트를 주고, 로봇은 이야기를 뱉어냅니다. 하지만 여기 함정이 있습니다. 당신은 단순히 이야기를 원하는 것이 아닙니다. 당신은 수학적으로 진실임이 보장되고, 플롯 구멍(plot hole)이 없으며, 물리 법칙을 깨뜨리는 마법이 없고, 캐릭터가 설명 없이 사라지는 일이 없는 이야기를 원합니다. 이것이 바로 **검증된 코드 생성(verified code generation)**의 세계입니다. 이는 인공지능에게 단순히 소프트웨어를 작성하는 것을 넘어, "나는 내가 말한 대로 이 코드가 모든 가능한 상황에서 정확히 작동할 것임을 약속한다"라고 말하는 수학적 증명서, 즉 '정확성 증명(proof of correctness)'을 함께 가져오라고 요구하는 컴퓨터 과학의 한 분야입니다.

오랫동안 이 작업을 수행하는 표준적인 방법은 일종의 2단계 댄스와 같았습니다. 먼저 로봇이 코드를 쓰고(이야기를 쓰고), 그 다음 별도의 로봇 교정팀이 그 이야기가 말이 되는지 확인하려고 시도하는 것입니다. 만약 교정팀이 플롯 구멍을 발견하면, 그들은 이야기를 다시 작성자에게 보내 수정하게 합니다. 작성자는 이야기를 패치하여 다시 보내고, 이 사이클은 반복됩니다. 하지만 이 논문은 이 "쓰고 나서 확인하는" 댄스가 종종 서투르고 비효율적이라고 주장합니다. 그것은 마치 다리를 다 건설한 후에야 지지보를 넣는 것을 잊었다는 사실을 깨닫고, 결국 다리를 허물고 다시 건설해야 하는 것과 같습니다. 이 논문의 저자들은 새로운 방식을 제안합니다. 코드를 쓰고 나서 증명을 따로 하는 대신, 로봇이 처음 스케치를 할 때부터 도로와 지지보를 동시에 계획하여 두 가지가 완벽하게 맞물리도록 만드는 것입니다.

문제점: "쓰고 나서 확인하는" 함정

**"Joint Program-and-Proof Planning for Verified Code Generation"**이라는 제목의 이 논문은 AI가 검증된 소프트웨어를 작성할 때 겪는 좌절스러운 병목 현상을 다룹니다. 현재 대부분의 시스템은 "프로그램 후 증명(program-then-proof)" 워크플로우를 따릅니다. 이것은 마치 요리사에게 복잡한 요리를 만들라고 요청한 뒤, 음식이 식탁에 올라온 후에야 음식 평론가에게 재료가 신선했는지 그리고 조리법이 안전했는지 증명하라고 요청하는 것과 같습니다. 만약 평론가가 문제(예: 덜 익은 닭고기)를 발견하면, 요리사는 다시 돌아가서 요리를 다시 만들어 이번에는 평론가가 만족하기를 바라야 합니다.

저자들은 이러한 순차적인 접근 방식이 결함이 있다고 주장합니다. AI가 코드를 먼저 작성하도록 결정하면, 겉보기에는 괜찮아 보이지만 증명하기에는 악몽 같은 구조를 선택할 수 있기 때문입니다. 예를 들어, AI가 리스트에서 가장 큰 숫자를 찾는 프로그램을 작성한다고 가정해 봅시다. AI는 쓰기는 짧고 간결하지만, 그것이 작동함을 증명하기 위해 믿을 수 없을 정도로 복잡하고 숨겨진 수학적 규칙을 요구하는 방법을 선택할 수 있습니다. 일단 코드가 작성되면, AI는 갇혀버립니다: 그 특정 코드에 맞춰서 매우 어려운 증명을 만들어내거나, 아니면 코드를 찢어버리고 처음부터 다시 시작해야 합니다. 이는 많은 시간, 비용, 그리고 AI가 코드를 계속 패치하고 증명을 수정하지만 서로 결코 맞지 않게 되는 "수리 루프(repair loops)"로 인한 낭비를 초래합니다.

해결책: P3 (손에 손 잡고 하는 플래너)

이를 해결하기 위해 연구진은 AI가 벽돌을 한 장 쌓기도 전에 건물과 안전 점검을 위한 청사진을 모두 그리는 숙련된 건축가처럼 행동하는 새로운 워크플로인 P3를 도입했습니다.

P3는 곧바로 코드를 작성하는 대신, 먼저 **통합된 계획(unified plan)**을 생성합니다. 이 계획은 두 가지 질문에 동시에 답하는 고수준의 스케치입니다:

1. 코드는 어떻게 작동할 것인가? ("프로그램 스케치")
2. 우리는 그것이 작동함을 어떻게 증명할 것인가? ("증명 스케치")

이 계획은 솔루션의 구조를 결정합니다. 코드의 "형태"(예: 재귀 루프와 폴드 중 선택)를 결정하는 동시에, 그 형태가 안전함을 증명하는 데 필요한 수학적 규칙(불변량, invariants)을 동시에 선택합니다. 이것은 "우리는 현수 케이블을 사용하여 다리를 건설할 것이므로, 우리의 증명 계획에는 그 케로의 장력을 체크하는 과정이 포함되어야 한다"라고 결정하는 것과 같습니다.

이 공유된 계획이 확정되면, AI는 세부 사항을 "정교화(elaborate)"합니다. AI는 실제 코드와 실제 증명을 작성하지만, 이는 이미 합의된 청사진의 빈칸을 채우는 작업일 뿐입니다. 만약 증명이 실패하더라도, AI는 이미 구조가 결정되었기 때문에 어디를 살펴봐야 할지 정확히 알 수 있습니다. 만약 계획 자체가 잘못되었다면(예: 다리 설계가 불가능한 경우), AI는 완성된 건물을 필사적으로 패치하는 대신 계획 단계로 돌아가 청사진을 다시 그립니다.

새로운 시험장: Lean4Commit0

저자들은 기존의 AI 시스템 테스트들이 로봇에게 교과서의 수학 퍼즐을 풀라고 하는 것처럼 너무 쉽다는 것을 깨달았습니다. 실제 소프트웨어는 훨씬 더 무질서합니다. 이 새로운 방법을 제대로 테스트하기 위해, 그들은 Lean4Commit0이라는 새로운 벤치마크를 구축했습니다.

그들은 108개의 실제 오픈 소스 소프트웨어 라이브러리(Python, Rust, C/C++, Java로 작성됨)를 긁어모아 그 핵심 기능들을 "검증된 코드" 도전 과제로 변환했습니다. 단순한 "두 숫자 더하기" 작업 대신, 이 도전 과제들은 프로그램의 서로 다른 부분들 사이의 복잡한 관계를 포함합니다. 예를 들어, 구성 시스템(configuration system)에서 "설정을 '높음(High)'으로 설정한 후 나중에 '낮음(Low)'으로 설정하면, 시스템이 '낮음' 설정을 올바르게 기억하는가?"를 증명하도록 요구할 수 있습니다. 이러한 작업은 AI가 서로 다른 함수들이 어떻게 통신하는지를 이해할 것을 요구하며, 이는 교과서적인 문제들보다 훨씬 더 어렵습니다.

결과: 스마트한 계획이 승리한다

연구팀은 네 가지 강력한 AI 모델(Codex, Gemini, Claude의 버전 포함)을 대상으로 세 가지 벤치마크(Verina, AlgoVeri, 그리고 새로운 Lean4Commit0)에서 P3를 테스트했습니다.

결과는 명확했습니다: 함께 계획하는 것이 따로 쓰는 것보다 더 낫습니다.

• 성공률: P3는 모든 테스트에서 다른 어떤 방법보다 더 많은 과제를 해결했습니다. 가장 어려운 과제에서, P3는 기존의 최고 방법들보다 성공률을 4.6 ~ 11.2 퍼센트 포인트 향상시켰습니다.
• 효율성: 단순히 더 많은 문제를 푸는 것뿐만 아니라, 더 빠르고 저렴하게 해결했습니다. 어려운 과제에서 P3는 API 호출 비용을 최대 40% 줄였고, 소요 시간을 최대 37% 단축했습니다. 이는 AI가 불가능한 것을 증명하려고 애쓰거나 구조적으로 잘못된 코드를 다시 쓰는 데 시간을 낭비하지 않았기 때문입니다.
• "결합(Joint)"의 이점: "결합된 계획"이 비결임을 증명하기 위해, 연구팀은 AI가 코드를 계획하되 증명을 미리 계획하지 않는 테스트를 실행했습니다. 이 "코드 전용 계획(code-only planning)" 방식은 P3보다 성능이 떨어졌으며, 이는 코드를 계획하는 동안 증명에 대해서도 함께 생각하는 것이 차이를 만든다는 것을 확인시켜 주었습니다.

실제 사례: 레드-블랙 트리 (Red-Black Tree)

이 방식이 실제로 어떻게 작동하는지 보여주기 위해, 저자들은 컴퓨터 과학의 고전적인 문제인 "레드-블랙 트리(데이터를 효율적으로 조직하기 위해 사용되는 복잡한 데이터 구조)에서 노드를 삭제하는 문제"를 살펴보았습니다.

• 기존 방식 (프로그램 후 증명): AI는 노드를 삭제하는 특정한 방식을 결정했습니다. 알고 보니 이 방식은 구조적으로 너무 지저킨 형태여서, 구멍을 메우기 위해서만 6,300줄 이상의 코드가 필요하거나 아예 실패했습니다.
• P3 방식: AI는 먼저 삭제 과정을 계획했습니다. AI는 다른 구조적 접근 방식이 증명하기에 더 쉬울 것이라는 점을 깨달았습니다. AI는 그 계획을 고수했고, 단 1,105줄 만에 문제를 해결했습니다.

이것이 중요한 이유

이 논문은 AI가 진정으로 신뢰할 수 있는 소프트웨어를 작성하기 위해서는 "코드"와 "증명"을 별개의 작업으로 취급하는 것을 멈춰야 한다고 시사합니다. AI가 코드를 설계하는 동안 수학적 안전성을 함께 생각하도록 강제함으로써, 우리는 구축 단계부터 올바르고(correct by construction), 더 저렴하고 빠르게 생산할 수 있는 소프트웨어를 얻게 됩니다. 이는 "나중에 고치는 것"에서 "처음부터 제대로 만드는 것"으로의 전환이며, 우리가 의존하는 소프트웨어가 그것을 증명하는 수학만큼이나 견고함을 보장하는 길입니다.