LLM과 대수적 표현으로 항공 교통 버그를 잡다!
영국 항공 교통 관제 시스템 붕괴(UK air traffic control meltdown)를 야기한 버그를 Lean으로 검증하는 과정에서 LLM의 한계와 가능성을 확인
LLM은 사양(Specs) 작성에 어려움을 겪었지만, 일상적인 증명(Routine Proofs)에는 뛰어난 능력을 보임
문제 해결을 위해 대수적 표현(Algebraic Terms)을 도입하여 증명 과정을 단순화하고 효율성을 높임
형식적 검증(Formal Verification)의 실용성을 높이기 위해 LLM과 같은 도구의 활용 가능성을 제시
LLM 기반 형식적 검증의 한계와 가능성
저자는 LLM이 사양(Specs) 작성에 어려움을 겪는다고 지적하며, LLM이 생성한 사양이 종종 부정확하거나 구현에 맞춰져 있다고 비판한다. 하지만 일상적인 증명(Routine Proofs) 작업에는 매우 효과적이며, 특히 대수적 표현을 사용했을 때 그 효율성이 극대화된다고 강조한다. 이는 LLM이 아직 추상화(Abstraction) 능력이 부족하지만, 반복적인 작업에는 강점을 보인다는 것을 의미한다.
대수적 표현을 활용한 문제 해결
저자는 항공 교통 관제 시스템의 버그를 해결하기 위해 대수적 표현(Algebraic Terms)을 도입하여 증명 과정을 단순화했다. 특히, 비행 계획을 범주(Category)로 모델링하고, 비행 경로의 합성(Composition) 연산을 정의함으로써 문제 해결의 핵심을 파악했다. 이러한 접근 방식은 증명의 효율성을 높였으며, Mathlib 라이브러리의 광범위한 기능을 활용할 수 있게 했다.
비행 계획의 형식적 검증을 위한 아키텍처
저자는 비행 계획을 대수적 구조(Algebraic Structure)로 표현하고, 이를 기반으로 최소 UK 하위 계획(Least UK sub-plan)을 찾는 알고리즘을 설계했다. 이 과정에서 재조정(Reconciliation)과 트리밍(Trimming) 두 단계로 나누어 구현했으며, 각 단계별로 Lean을 사용하여 형식적 검증을 수행했다. 특히, 데이터 격리 아키텍처(Data Isolation Architecture)를 통해 중복된 지점 문제를 해결했다.
구현 및 정확성 검증
구현 단계에서 저자는 재조정(Reconciliation) 알고리즘의 정확성을 증명하기 위해 세 가지 주요 정리를 제시했다. 완전성(Completeness), 사운드니스(Soundness), 그리고 중복 없음(No Duplicates)을 증명함으로써 알고리즘의 신뢰성을 확보했다. 특히, 함수자(Functor)의 속성을 활용하여 재조정 알고리즘의 정확성을 입증하는 과정은 주목할 만하다.
