실전 산업 규모 검증을 향하여: seL4 기반의 LLM 주도 정리 증명

섹션별 상세

기존의 LLM 기반 정리 증명 연구는 miniF2F와 같은 수학 중심 벤치마크에 편중되어 있거나, 수천억 개의 파라미터를 가진 폐쇄형 모델을 사용하여 실제 산업 현장의 로컬 배포 및 비용 문제를 해결하기 어려웠다.

AutoReal 방법론은 LLM에게 증명 단계 뒤에 숨겨진 논리적 근거를 가르치는 'Chain-of-Thought(CoT) 기반 증명 훈련'을 도입하여, 모델이 단순한 증명 코드 생성을 넘어 단계별 설명을 함께 제공할 수 있도록 설계되었다.

프로젝트 내의 기존 증명 데이터를 활용하여 LLM의 증명 능력을 강화하는 '문맥 보강(Context Augmentation)' 기법을 적용함으로써, 특정 검증 프로젝트의 고유한 특성과 패턴을 모델이 더 잘 파악하도록 지원한다.

7B 파라미터 규모의 AutoReal-Prover 모델은 seL4의 주요 이론 10개 카테고리, 660개 정리에서 51.67%의 성공률을 달성하며 기존 최고 기록인 27.06%를 크게 상회하는 성능을 보여주었다.

보안 관련 AFP(Archive of Formal Proofs) 프로젝트의 451개 정리에 대해 추가 평가를 진행한 결과 53.88%의 성공률을 기록하며, 특정 프로젝트에 국한되지 않는 범용적인 정리 증명 능력을 입증했다.

형식 검증(Formal Verification): — 소프트웨어나 하드웨어 시스템이 명세대로 정확히 동작함을 수학적으로 입증하는 과정이다. 시스템의 모든 가능한 상태를 논리적으로 검사하여 결함이 없음을 보장하므로 보안 및 안전 필수 시스템에서 매우 중요하다.
정리 증명(Theorem Proving): — 논리적 추론 규칙을 사용하여 특정 명제가 참임을 수학적으로 입증하는 행위이다. 컴퓨터 과학에서는 프로그램의 속성을 증명하여 버그가 없음을 확인하는 데 널리 사용되며, 자동화된 도구를 통해 효율성을 높인다.
seL4: — 보안성이 극대화된 마이크로커널로, 소스 코드와 기계어 수준에서 수학적 명세와의 일치성이 세계 최초로 증명된 운영체제 커널이다. 산업 규모의 복잡한 검증 사례로 자주 인용된다.
Isabelle: — 고차 논리(HOL)를 지원하는 대화형 정리 증명 도구이다. 사용자가 수학적 증명을 작성하면 이를 기계적으로 검증하며, seL4 프로젝트의 핵심 검증 도구로 사용되었다.