← 최신 논문
🤖 AI

Escaping the Quicksand: A Call to Arms

AI 주도 개발로 인해 악화되는 기술 부채의 가속화되는 위험에 대응하기 위해, 본 논문은 순수하게 산문 기반의 명세에서 벗어나 테스트, 실행 가능한 명세, 그리고 형식적 증명의 유연한 결합으로 전환할 것을 제안하며, 이는 인간 및 AI 엔지니어 모두를 위한 더 효과적인 피드백 루프를 생성하기 위해 새로운 시맨틱스 인프라에 의해 뒷받침되어야 한다고 주장한다.

원저자: Peter Sewell, Jean Pichon-Pharabod

게시일 2026-08-21
📖 5 분 읽기🧠 심층 분석

원저자: Peter Sewell, Jean Pichon-Pharabod

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

현대 생활의 보이지 않는 기계 장치들—우리의 은행, 병원, 전력망, 그리고 통신 네트워크—이 서서히 가라앉고 있는 토대 위에 세워져 있다고 상상해 보십시오. 이것이 오늘날 컴퓨팅 산업이 직면한 현실입니다. 수십 년 동안 소프트웨어를 구축하는 표준적인 방식은 프로그램이 무엇을 해야 하는지에 대한 대략적인 설명을 작성한 다음, 코드를 쓰고, 마지막으로 다양한 입력을 실행하여 프로그램이 깨지는지 확인하며 테스트하는 것이었습니다. '테스트 및 디버깅(test-and-debug)' 개발로 알려진 이 방식은 기술의 번영을 가능하게 했지만, 시스템 곳에 숨겨진 결함들을 남겨두었습니다. 원래의 설명들이 종종 모호하고 일반적인 언어로 작성되기 때문에 기계가 이를 검증할 수 없으며, 테스트는 프로그램이 보여줄 수 있는 수십억 개의 가능한 동작 중 극히 일부만을 다룰 수 있기 때문에 많은 오류가 빠져나가게 됩니다. 인공지능이 더 많은 코드를 작성하기 시작함에 따라, 이 순환은 더욱 가속화되어, 사이버 공격이 드물고 컴퓨팅 능력이 부족했던 시절에 내려진 수십 년 된 설계 선택지라는 '늪' 위에 더욱 복잡하고 취약한 거대 시스템을 만들어낼 위험이 있습니다.

두 명의 연구자, 케임브리지 대학교의 피터 세월(Peter Sewell)과 아루스 대학교의 진 피숑-파라보드(Jean Pichon-Pharabod)는 업계가 75년 동안 위험한 루프에 갇혀 있다고 주장합니다. 그들은 우리가 코드를 작성하는 데는 매우 숙련되었지만, 그 코드가 달성해야 할 목표에 대한 정밀한 정의를 소홀히 해왔다고 관찰합니다. 현재의 접근 방식은 산문 형태의 명세(prose specifications), 즉 시스템의 동작을 설명하는 문장들의 단락에 의존합니다. 이러한 방식은 인간이 읽기에는 쉽지만, 본질적으로 모호하고 불완전합니다. 인간 독자는 문장을 한 가지 방식으로 해석할 수 있는 반면, 기계나 다른 인간은 다르게 해석할 수 있습니다. 이러한 설명은 컴퓨터에 의해 직접 테스트될 수 없기 때문에, 개발자들은 프로그램이 실제로 올바른 일을 하고 있는지 검증하기보다는 단순히 "프로그램이 충돌하는가?"와 같은 간단한 확인 작업에 의존하며 올바른 동작이 무엇인지 추측해야만 합니다. 이렇게 작성된 의도와 실제 코드 사이의 간극은 막대한 양의 기술 부채를 생성하며, 이는 보안 취약점이나 공격자가 악용할 수 있는 시스템 실패라는 형태로 나타나는 숨겨진 비용입니다.

저자들은 해결책이 테스트를 포기하는 것이 아니라, 명세를 사용하는 방식을 바꾸는 것이라고 제안합니다. 모호한 단락을 쓰는 대신, 컴퓨터가 실행할 수 있는 형태, 즉 '실행 가능한(executable)' 명세를 만드는 것을 제안합니다. 명세가 개발 과정 중에 작동하는 살아있는 심판 역할을 한다고 상상해 보십시오. 코드가 작성되거나 생성됨에 따라, 이 실행 가능한 명세가 코드와 함께 실행되며 코드의 동작이 의도된 규칙과 일치하는지 즉각적으로 확인합니다. 만약 코드가 명세에서 금지한 행동을 하려고 하면, 시스템은 즉시 이를 알립니다. 이는 훨씬 더 긴밀한 피드백 루프를 만들어, 개발자가 몇 주 뒤가 아니라 오류가 발생하는 즉시 이를 잡아낼 수 있게 합니다. 이 접근 방식은 다양한 방식으로 적용될 수 있습니다. 코드를 먼저 작성하고 그에 맞는 명세를 쓰거나, 명세에서 시작하여 그에 부합하는 코드를 생성하거나, 혹은 두 가지를 함께 구축할 수 있습니다. 핵심은 명세가 단순히 읽기 위한 문서가 아니라, 사용하기 위한 도구여야 한다는 점입니다.

그러나 연구자들은 이것이 단순히 스위치를 올리는 것처럼 간단한 작업은 아니라는 점을 인정합니다. 이를 대규모로 구현하기 위해서는 컴퓨팅 커뮤니티가 새로운 계층의 인프라를 구축해야 합니다. 현재 C 프로그래밍 언어, 러스트(Rust) 언어, 또는 컴퓨터 칩에서 실행되는 명령어와 같은 많은 근본적인 기술의 동작에 대해 보편적으로 수용되는 기계 판독 가능한 정의가 존재하지 않습니다. 일부 연구자들이 시스템의 특정 부분에 대해 이러한 정의를 성공적으로 만들어냈지만, 이들을 모두 연결하는 통합된 프레임워크는 없습니다. 저자들은 이 인프라를 구축하는 것이 규모와 협력의 문제라고 지적합니다. 이는 하드웨어부터 클라우드 서비스에 이르기까지 컴퓨팅 기술의 전체 스택에 대한 정밀한 정의를 생성, 검증 및 유지 관리하기 위해 대학, 정부, 기술 기업의 대대적이고 조율된 노력을 필요로 합니다.

또한 이 논문은 인공지능의 역할에 대해서도 다룹니다. 저자들은 더 나은 피드백 루프 없이 단순히 AI를 사용하여 더 많은 코드를 작성하는 것은 문제를 악화시킬 뿐이라고 경고합니다. AI는 인간보다 더 빠르게 코드를 생성할 수 있지만, 만약 그 코드가 불안정한 토대 위에 구축되고 구식의 비효율적인 방식으로만 테스트된다면, 더 많은 숨겨진 오류를 가진 더 큰 시스템을 만들 뿐일 것입니다. 반대로, AI가 이러한 실행 가능한 명세를 생성하고 검증하는 데 도움을 준다면, AI는 소프트웨어 품질을 개선하는 강력한 도구가 될 수 있습니다. 저자들은 AI가 엄격한 명세를 만드는 데 도움을 주고, 그 명세가 인간이 작성한 코드와 AI가 작성한 코드 모두의 정확성을 검증하는 데 사용되는 미래를 구상합니다. 이를 통해 모든 개발자가 수학자가 될 필요 없이, 단순한 테스트에서 시작하여 복잡한 수학적 정당성 증명으로 나아가는 점진적인 신뢰도 향상을 이룰 수 있을 것입니다.

앞으로 나아갈 명확한 경로에도 불구하고, 저자들은 업계가 인센티브의 불일치로 인해 발목을 잡히고 있다고 주장합니다. 기술 기업들은 시장 점유율을 확보하기 위해 제품을 빠르게 출시하는 데 동기가 부여되어 있는 반면, 실패의 위험은 주로 사회와 최종 사용자에게 전가됩니다. 이러한 실패를 방지하기 위해 필요한 견고한 인프라를 구축하는 것은 비용이 많이 들고 시간이 오래 걸리는 일이며, 단일 기업이 모두에게 영향을 미치는 문제를 해결하는 데 드는 전체 비용을 전적으로 부담하고 싶어 하지 않습니다. 연구자들은 물리학이나 생물학에서 볼 수 있는 대규모 프로젝트와 유사하게, 이러한 '시맨틱 인프라(semantic infrastructure)'의 구축을 위해 자금을 지원하고 조율하는 집단적 노력을 촉구합니다. 그들은 그 비용이 상당하지만, 현재 인공지능에 투입되는 비용의 아주 작은 부분이며 컴퓨팅의 미래를 확보하는 데 필수적이라고 제안합니다. 이러한 변화 없이는, 업계는 점점 더 복잡한 시스템을 너무 약한 토대 위에 구축하는 순환 속에 갇혀 있으며, 사회를 지속적인 위험에 노출된 상태로 남겨두게 될 것입니다.

저자들은 이 문제를 해결할 도구와 방법이 이미 존재한다고 결론짓습니다. 연구자들은 복잡한 시스템의 동작을 정의하고 높은 신뢰도로 검증하는 방법을 성공적으로 입증해 왔습니다. 부족한 것은 이러한 방법들을 일상적인 실무로 가져오고, 모두가 사용할 수 있는 공유 인프라를 구축하려는 의지입니다. 이 논문은 연구 커뮤니티, 산업 리더, 그리고 자금 지원 기관이 이 과업을 위해 협력할 것을 촉구하는 행동 촉구의 메시지입니다. 모호한 설명을 버리고 정밀하고 실행 가능한 명세로 나아감으로써, 컴퓨팅 세계는 기술 부채라는 늪에서 벗어나 더 혁신적일 뿐만 아니라 근본적으로 더 안전하고 신뢰할 수 있는 미래를 건설할 수 있습니다.

연구 분야의 논문에 파묻히고 계신가요?

연구 키워드에 맞는 최신 논문의 일일 다이제스트를 받아보세요 — 기술 요약 포함, 당신의 언어로.

Digest 사용해 보기 →