TLA+로 검증할 수 있는 것과 없는 것
Key Point
TLA+로 AI 시스템 검증을 완벽히 해결할 수 있다는 기대가 커지고 있는데, 형식화 불가능한 성질, 다중 단계 속성, 행동 수열 비교 같은 근본적 한계를 알아야 현실적 기대를 조정할 수 있다.
핵심 요약
- AI 안전을 TLA+ 형식검증으로 완전히 해결할 수 있다는 기대가 커지고 있지만, 실제 한계가 크다.
- TLA+는 시스템을 상태 수열로 나누고, 각 상태에서 불린 식을 표현하며 항상(always), 다음(prime), 결국(eventually) 같은 시간논리 연산자로 성질을 정의한다.
- 불변식(invariants)과 안전 성질(safety properties)은 TLA+의 가장 기본적인 검증 대상이며, 생생성 성질(liveness properties)은 좋은 일이 언젠가 일어남을 보장한다.