상상해 보세요. 여러분이 **거대한 도서관 (대형 소프트웨어 시스템, 예: seL4 운영체제)**에 있습니다. 이 도서관에는 수만 권의 책 (코드와 증명) 이 있고, 여러분은 새로운 책 한 권을 써야 합니다. 하지만 이 책은 다른 수만 권의 책에 있는 내용을 참조해야만 쓸 수 있는 매우 복잡한 책입니다.
1. 기존 방법의 문제점: "단어만 찾는 검색 엔진"
지금까지 인공지능 (LLM) 이 이 일을 할 때의 방식은 이랬습니다:
방식: "내가 지금 '사과'라는 단어를 쓰고 있는데, 도서관에서 '사과'라는 단어가 들어간 다른 책들을 찾아줘."
문제점: 도서관에서 '사과'라는 단어가 들어간 책은 수천 권일 수 있습니다. 하지만 그 책들이 어떤 논리로 쓰였는지, 어떤 순서로 이야기를 전개했는지는 모릅니다.
결과: 인공지능은 엉뚱한 책 내용을 가져와서 억지로 끼워 맞추려다 실패하거나, 같은 실수를 반복하며 지쳐버립니다. 특히 도서관이 너무 크고 책들이 서로 복잡하게 얽혀 있으면 (운영체제 같은 경우), 이 방식은 통하지 않습니다.
2. PROMISE 의 혁신: "증명의 '흐름'과 '구조'를 읽는 탐정"
PROMISE 는 단순히 단어를 찾는 게 아니라, **"증명이라는 이야기가 어떻게 흘러가는지"**를 봅니다.
핵심 아이디어: "이 책의 3 장에서 주인공이 '문'을 열려고 했을 때, 다른 책들에서 비슷한 상황 (문 열기) 이 어떻게 해결되었는지 그 순서와 패턴을 찾아줘."
비유:
기존 방식은 **"키워드 (사과)"**만 보고 책을 추천합니다.
PROMISE 는 **"이야기의 흐름 (문 열기 → 자물쇠 풀기 → 들어가기)"**을 보고 추천합니다.
예를 들어, "문 열기"라는 상황에서는 '자물쇠'를 풀어야 한다는 논리적 흐름이 있습니다. PROMISE 는 과거의 성공적인 증명들에서 **"문 열기 상황 → 자물쇠 풀기"**라는 구조적인 패턴을 찾아내어, 지금의 상황에 적용합니다.
3. PROMISE 가 어떻게 작동하나요? (3 단계 프로세스)
구조적 검색 (Structural Retrieval):
지금 증명 중인 부분의 '상태'를 보고, 과거의 증명 기록에서 비슷한 논리적 흐름을 가진 부분을 찾아냅니다.
비유: "지금 내가 '고양이'를 잡으려고 하는데, 과거에 '고양이'를 잡았던 다른 사냥꾼들은 어떤 순서로 잡았지? (먼저 숨고, 그다음에 던지고...)"
맞춤형 레시피 제공 (Context-Aware):
찾아낸 패턴을 바탕으로, 지금 상황에 쓸 수 있는 **정확한 도구 (함수나 규칙)**를 골라줍니다.
비유: "고양이 잡기 패턴을 찾았으니, 이제 그 패턴에 맞는 '고양이 사냥용 그물'이라는 도구를 가져와줘." (단순히 '그물'이라는 단어만 찾는 게 아니라, 지금 상황에 맞는 그물을 줍니다.)
단계별 검증 (Iterative Search):
한 번에 끝내려고 하지 않습니다. 한 걸음씩 나아가고, 매 단계마다 "이게 맞는지" 컴퓨터가 직접 확인합니다. 틀리면 바로 뒤로 돌아서 다른 길을 시도합니다.
비유: 미로에서 한 걸음씩 걸어가며 "이 길은 막혔네? 그럼 다른 길로 가자"를 반복하며, 실수하면 즉시 수정합니다.
🌟 왜 이것이 중요한가요?
기존의 한계: 큰 시스템 (운영체제 등) 을 증명하려면 수천 개의 작은 논리 조각들이 서로 얽혀 있습니다. 기존 AI 는 이 얽힌 실타래를 풀지 못했습니다.
PROMISE 의 성과: 이 연구팀은 PROMISE 를 통해 **seL4(세계에서 가장 안전한 운영체제 중 하나)**의 증명 작업에서 기존 방법보다 최대 2 배 이상 더 많은 증명을 성공적으로 자동화했습니다.
의미: 이제 인공지능이 단순히 "글을 잘 쓰는 것"을 넘어, **"복잡한 논리를 구조적으로 이해하고 해결하는 능력"**을 갖게 되었습니다. 이는 앞으로 자율주행차, 항공기 제어 시스템 등 생명이 걸린 중요한 소프트웨어를 자동으로 검증하는 데 큰 도움이 될 것입니다.
📝 한 줄 요약
"PROMISE 는 인공지능에게 단순히 '단어'를 찾아주는 게 아니라, 복잡한 증명 문제를 해결할 때 '어떤 순서로, 어떤 패턴으로' 접근해야 하는지 알려주는 똑똑한 나침반을 만들어준 연구입니다."
1. 문제 정의 (Problem Definition)
배경: 형식적 검증 (Formal Verification) 은 안전-중요 시스템의 기능적 정확성을 수학적으로 보장할 수 있지만, 증명 생성 과정이 매우 노동 집약적이고 전문성이 요구됩니다. 예를 들어, seL4 마이크로커널 검증에는 수십 년에 걸친 인력이 투입되었습니다.
현재의 한계: 최근 대규모 언어 모델 (LLM) 의 발전에도 불구하고, 자동 증명 생성은 여전히 큰 과제로 남아 있습니다. 기존 LLM 기반 접근법들은 다음과 같은 근본적인 한계를 가집니다:
단일 샷 (Single-shot) 또는 얕은 검색: 증명을 한 번에 생성하거나, 표면적인 텍스트 유사성 (키워드 기반) 에만 의존하여 관련 증명을 검색합니다.
구조적 의존성 무시: 운영체제나 컴파일러와 같은 대규모 시스템은 파일, 모듈, 추상화 계층 간에 깊은 구조적 의존성을 가집니다. 기존 방식은 이러한 복잡한 의존성과 증명 상태의 진화 패턴을 포착하지 못해 확장성이 떨어집니다.
문맥 민감성 부족: 실제 증명 엔지니어는 현재 증명 상태 (Goal, Assumptions) 와 논리적 흐름에 맞춰 증명을 구성하지만, 기존 모델들은 정적인 증명 조각 (Lemma, Proof script) 만을 재사용하려 합니다.
2. 방법론 (Methodology: PROMISE)
저자들은 PROMISE (PROof MIning via Structural Embeddings) 를 제안합니다. 이는 LLM 을 이용한 증명 생성을 단순한 텍스트 생성이 아닌, 구조적 유사성에 기반한 상태 기반 (Stateful) 및 반복적 탐색 과정으로 재정의합니다.
핵심 아이디어: 구조적 모방 (Structural Imitation)
인간 증명 엔지니어가 증명할 때, 단순한 텍스트 매칭이 아닌 '증명 상태의 진화 패턴 (Proof-state transition patterns)'을 따라가며 유사한 논리적 구조를 재사용한다는 점에 착안했습니다.
주요 구성 요소
증명 상태 전이 추적 (Proof-State Transition Traces):
증명을 단일 문장이 아닌, 초기 상태 -> 전술 적용 -> 새로운 상태로 이어지는 시퀀스로 모델링합니다.
성공적인 증명들에서 Goal, Assumption, Context 가 어떻게 변하는지 (Transition) 를 추출하여 데이터베이스를 구축합니다.
구조적 검색 (Structural Retrieval):
기존 키워드 기반 검색 대신, 현재 증명 상태의 전이 패턴과 구조적으로 유사한 과거 증명 조각을 검색합니다.
Semantic Reranking: 구조적 유사성뿐만 아니라 현재 Goal 과의 의미적 유사성 (s_goal) 및 상수 중첩 (s_const) 을 고려하여 재순위화합니다.
검색된 결과는 전체 증명이 아닌, 전술 템플릿 (Tactic Templates) 형태로 추출되어 Few-shot 예시로 활용됩니다.
이름 검색 (Name Retrieval):
구조적 패턴을 채울 구체적인 Lemma 와 정의 (Definition) 이름을 현재 증명 컨텍스트에서 검색합니다.
Isabelle 의 PIDE(Proof IDE) 와 정적 분석을 통해 현재 스코프 내에서 유효한 이름만 선별하여 LLM 에 제공합니다.
Beam Search 기반 증명 탐색:
Command Generator (C): 현재 프론트 (Frontier) 의 각 노드에서 구조적 검색과 이름 검색을 기반으로 프롬프트를 구성하고, LLM 에게 다음 전술 (Tactic) 후보를 생성하도록 요청합니다.
검증 및 필터링: 생성된 후보는 Isabelle 에서 실행 (Machine-checked) 되어 문법 오류를 제거하고, 증명 상태를 업데이트합니다.
Beam Scoring: 증명 진행도 (Subgoal 감소), 증명 길이, 전술 다양성 등을 고려하여 다음 탐색 단계로 넘어갈 노드를 선별합니다.
안전 장치:
Leakage Prevention: 타겟 증명의 원본 코드는 검색 과정에서 완전히 배제되어 데이터 누출을 방지합니다.
Whole-Theory Check: 국소적으로 증명이 완료된 경우에도 전체 이론 (Theory) 환경에서 일관성 검사를 통과해야 최종 성공으로 인정합니다.
3. 주요 기여 (Key Contributions)
증명 생성에 대한 새로운 관점: 증명 생성을 키워드 검색이나 전술 예측이 아닌, 증명 상태 전이 (Proof-state transitions) 에 대한 프로세스 수준의 추론 문제로 재정의했습니다.
구조 인식형 프레임워크 (PROMISE): 모델 독립적 (Model-agnostic) 인 프레임워크를 개발하여, LLM 의 학습 없이도 구조적 검색과 상태 인식 탐색을 통해 증명을 유도합니다.
포괄적인 실험 평가: seL4 마이크로커널 검증 벤치마크 (223 개 정리) 에서 기존 최첨단 방법론 (Selene, Rango) 과 다양한 LLM 백엔드 (GPT-3.5, GPT-4.1, Qwen2.5-Coder-7B) 를 비교 평가했습니다.
4. 실험 결과 (Results)
성능 향상: PROMISE 는 대부분의 설정에서 기존 방법론을 압도적으로 능가했습니다.
Qwen2.5-Coder-7B-Instruct 기준: Selene ACC5 대비 P1 에서 +47 점, P2 에서 +34 점의 절대적 성능 향상을 기록했습니다.
최대 향상: GPT-3.5-Turbo 환경에서 Selene 대비 최대 +26 포인트 (상대적 186% 증가) 의 개선을 보였습니다.
P3 (고난이도) 증명: Qwen2.5-Coder-7B-Instruct 를 사용한 P3 레미마 (23 개) 에서 7 개를 성공적으로 증명하여, 차기 1 위인 Rango(3 개) 의 두 배 이상 성능을 발휘했습니다.
모델 간 안정성: LLM 의 능력 차이에 덜 민감합니다. GPT-4.1 과 Qwen2.5-Coder-7B 사이에서 성능 편차가 기존 방법론보다 훨씬 작게 나타나, 구조적 검색 전략이 모델 크기와 무관하게 효과적임을 입증했습니다.
예외 사례: GPT-4.1 을 사용한 P2 난이도에서 Rango 보다 2 포인트 낮았습니다. 이는 GPT-4.1 이 강력한 추론 능력을 가지고 있음에도 불구하고, PROMISE 의 엄격한 Few-shot 프롬프트 구조가 모델의 유연한 추론을 제한했을 가능성이 있다고 분석했습니다.
5. 의의 및 결론 (Significance & Conclusion)
확장성 확보: 대규모 시스템 소프트웨어 검증에서 LLM 의 확장성 한계를 극복하는 중요한 단계를 제시했습니다. 단순한 텍스트 유사성이 아닌 구조적 유사성을 활용함으로써 복잡한 의존성 그래프를 가진 증명에서도 효과적으로 작동함을 보였습니다.
실용적 가치: seL4 와 같은 실제 산업용 시스템 검증에 적용 가능한 수준의 자동화를 보여주었습니다. 이는 수동 증명 비용을 획기적으로 줄이고 형식적 검증의 대중화를 가속화할 수 있는 잠재력을 가집니다.
미래 전망: 추후 전체 seL4 검증 코어에 대한 확장성 평가와, 휴리스틱 검색을 대체할 강화학습 기반의 데이터 주도 선택 전략 도입을 계획하고 있습니다.
요약하자면, PROMISE 는 LLM 이 인간 증명 엔지니어처럼 '증명의 논리적 흐름과 구조'를 이해하고 재사용하도록 함으로써, 대규모 형식적 검증의 자동화 난제를 해결하는 획기적인 접근법을 제시한 연구입니다.