Case study: solving P-99 with LPTP and an LLM

컴퓨터가 단순히 딱딱하고 로봇 같은 명령을 따르는 것을 넘어, 인간이 문제를 설명하는 모호하고 불분명한 방식을 실제로 이해할 수 있는 세상을 상상해 보십시오. 이것이 바로 인공지능(AI), 그중에서도 **대규모 언어 모델(LLM)**이라 불리는 분야의 최전선입니다. LLM을 인터넷에 있는 거의 모든 것을 읽은 매우 똑똑하고 박학다식한 학생이라고 생각해 보십시오. 만약 당신이 이야기를 써달라고 하면 쓸 수 있고, 코드를 짜달라고 하면 짤 수 있습니다. 하지만 함정이 하나 있습니다. 이 학생은 "환각(hallucination)" 증세를 보일 수 있는데, 이는 자신이 사실을 자신 있게 지어내거나, 실행하려고 하면 몰래 고장 나는 완벽해 보이는 코드를 작성할 수 있음을 의미합니다.

이를 해결하기 위해 과학자들은 **형식 검증(Formal Verification)**을 사용합니다. 이는 마치 수학 선생님이 학생의 숙제 모든 단계를 일일이 확인하여 논리적으로 틀리는 것이 불가능하도록 만드는 것과 같습니다. 컴퓨터 과학의 세계에는 **99 Prolog 문제(또는 P-99)**라는 유명한 도전 과제들이 있습니다. 이것들은 논리 프로그래밍(단계별로 '어떻게' 할지를 설명하기보다 '무엇'을 원하는지를 기술하는 코딩 방식)의 "체육관 운동"과 같습니다. 연구자들이 던지는 핵심 질문은 이것입니다. "우리가 AI 학생에게 간단한 영어 설명에 기반해 코드를 쓰게 하고, 그 직후에 수학 선생님이 그것이 실제로 올바른지 즉각적으로 확인할 수 있을까?" 이 논문은 바로 이 실험을 탐구하며, AI의 창의적인 자유와 형식 논리의 철저한 안전성을 결합합니다.

---

실험: 엄격한 선생님과 함께하는 코딩 듀오

이 연구에서 연구팀은 **"바이브 코딩(vibe-coding)"**과 **"베리코딩(vericoding)"**을 혼합한 새로운 작업 방식을 테스트하기로 결정했습니다. "바이브 코딩"을 당신이 냅킨에 대충 그린 스케치를 바탕으로 창의적인 친구에게 트리하우스를 만들어 달라고 요청하는 것이라고 상상해 보십시오. 당신은 "미끄럼틀과 비밀 문이 있는 트리하우스가 필요해"라고 말하고, 친구는 그냥 만들기 시작합니다. 빠르고 재미있지만, 결과물이 흔들거릴 수도 있습니다. "베리코딩"은 그 반대입니다. 이는 건축가를 고용하여 못 하나를 박기 전에도 설계도, 스트레스 테스트, 그리고 안전 점검을 요구하는 것과 같습니다.

연구진은 이 두 가지 접근 방식을 결합할 수 있는지 확인하고 싶었습니다. 그들은 창의적인 제작자 역할을 하기 위해 Claude(구체적으로 Opus 4.6 버전)라는 AI 모델을 사용했습니다. 그들은 유명한 P-99 목록 중 처음 33개의 문제를 제시했는데, 이 문제들은 단순하고 비형식적인 영어로 작성되어 있습니다. 예를 들어, 한 문제는 단순히 "리스트의 마지막 요소를 찾아라"라고 되어 있습니다.

AI의 임무는 다음과 같습니다:

1. 문제를 해결하기 위한 Prolog 코드를 작성한다.
2. 코드가 작동하는지 확인하기 위한 테스트 파일을 작성한다.
3. 코드가 안전하고, 정확하며, 항상 실행을 마칠 것임을 수학적으로 보장하는 **형식적 증명(formal proof)**을 작성한다.

이 증명들을 검증하기 위해, 그들은 **LPTP(Logic Program Theorem Prover)**라는 도구를 사용했습니다. LPTP를 "그럴듯해 보인다"라는 답변은 절대 받아들이지 않는 엄격한 수학 선생님이라고 생각하십시오. LPTP는 모든 주장에 대해 단계별 논리적 유도를 요구합니다.

결과: 마법과 수학의 혼합

실험은 성공적이었지만, 마법의 지팡이는 아니었습니다. 연구팀은 이 방법을 사용하여 **88개 중 33개(약 37.5%)**의 연습 문제를 해결했습니다. 그 배후에서 일어난 일은 다음과 같습니다:

• 창의적인 부분 (바이브 코딩): AI는 초기 코딩에 놀라울 정도로 뛰어났습니다. AI는 단 몇 분 만에 58개의 논리 프로시저(실제 코드)와 508개의 테스트 케이스를 작성했습니다. AI는 영어 지침을 이해했고, 정상적으로 실행되는 코드를 생성했습니다.
• 엄격한 부분 (베리코딩): 여기서부터 진짜 작업이 시작되었습니다. AI는 자신의 코드가 왜 올바른지 증명해야 했습니다. AI는 257개의 보조 정리(lemmas)(작은 수학적 사실들)를 생성했으며, 무려 11,800줄의 증명을 작성했습니다.
• 인간의 손길: 연구진은 단순히 AI가 제멋대로 하게 내버려 두지 않았습니다. 그들은 모든 파일을 수동으로 점검했습니다. 그들은 테스트를 실행하고, 논리적 진술을 읽고, LPTP로 증명을 다시 실행했습니다. 만약 AI가 막히거나 말이 안 되는 증명을 작성하면, 인간이 개입하여 힌트를 주었습니다. 예를 들어, 리스트의 마지막 항목을 찾는 문제에 대해, 인간은 AI에게 "이것이 append 함수와 어떻게 연결되나요?"라고 물어보며 올바른 증명을 구성하도록 도왔습니다.

주요 발견

이 논문은 이 새로운 작업 방식에 대해 몇 가지 핵심적인 사실을 밝혀줍니다:

1. AI는 "바이브 코딩"에 능숙해지고 있다: AI는 모호한 영어 설명을 빠르게 작동하는 Prolog 코드로 바꿀 수 있었습니다. 심지로 실제 세상의 Prolog 코드에서 자주 사용하는 "불순한(impure)" 트릭들을 피하고, 수학 선생님(LPTP)이 이해할 수 있는 엄격한 논리적 스타일을 고수했습니다.
2. AI는 "베리코딩"을 위해 밀어주는 손길이 필요하다: AI는 코드를 쉽게 생성할 수 있었지만, 그것이 왜 올바른지 증명하는 것은 더 어려웠습니다. 복잡한 기능적 속성(예: 코드가 의도한 대로 정확히 수행되는지 증명하는 것)의 경우, AI는 때때로 인간 연구자가 먼저 평이한 영어로 논리를 설명해 주기를 필요로 했습니다. 일단 인간이 힌트를 주면, AI는 그것을 형식화하고 증명할 수 있었습니다.
3. 아직 "해결된" 문제는 아니다: 팀은 99개의 문제를 모두 해결하지 못했습니다. 어떤 문제는 AI가 단 15분 만에 해결했지만(단순한 "마지막 요소" 문제처럼), 다른 문제들은 몇 시간이 걸렸습니다( "소인수 분해" 문제처럼). 연구진은 가장 어려운 문제들의 경우, AI가 인간의 지도 없이 스스로 올바른 증명 전략을 찾아내는 데 여전히 어려움을 겪고 있다고 언급했습니다.

미래의 모습: "MCP"와의 연결

논문은 또한 그들이 구축하고 있는 **모델 컨텍스트 프로토콜(Model Context Protocol, MCP)**이라는 새로운 도구를 설명합니다. 현재 AI와 수학 선생님(LPTP)은 파일과 텍스트 문서를 통해 대화하는데, 이는 마치 서로 편지를 주고받는 것과 비슷합니다. 새로운 MCP 도구는 그들에게 직통 전화선을 놓아주는 것과 같습니다. 이를 통해 AI는 실시간으로 수학 선생님에게 도움을 요청하고, 자신의 작업을 즉시 확인하며, 인간이 개입하기를 기다리지 않고도 오류를 수정할 수 있습니다. 그들은 이를 다른 AI 모델(Gemini 등)로 테스트했으며, 일부 모델은 증명을 위한 아이디어를 생성할 수는 있지만, 엄격한 검사를 통과하는 유효한 증명을 성공적으로 생성할 수 있는 것은 Claude뿐이라는 것을 발견했습니다.

결론

이 논문은 우리가 AI가 복잡하고 논리적인 코드를 작성하는 창의적인 파트너 역할을 할 수 있는 시대에 진입하고 있음을 보여주지만, 여-전히 가장 어려운 부분에서는 인간 "조종사"의 조종이 필요하다는 것을 보여줍니다. AI는 코드를 쓰고 심지어 수학 증명 초안을 작성할 수도 있지만, 때로는 세부 사항에서 길을 잃기도 합니다. AI의 속도와 창의성을 LPTP와 같은 형식 증명 검사기와 결합함으로써, 연구진은 AI의 실수가 실제 버그가 되기 전에 잡아내는 시스템을 만들었습니다. 아직 완전히 자동화된 "모든 것을 고치는" 기계는 아니지만, 소프트웨어를 그 어느 때보다 빠르고 안전하게 작성할 수 있게 해주는 강력한 새로운 도구입니다.