LLM과 대수적 표현으로 항공 교통 버그를 잡다!
by DD
2개월 전
조회수 6
영국 항공 교통 관제 시스템 붕괴(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)로 모델링하고, 비행 경로의 연산을 정의함으로써 문제 해결의 핵심을 파악했다. 이러한 접근 방식은 증명의 효율성을 높였으며, Mathlib 라이브러리의 광범위한 기능을 활용할 수 있게 했다.
