TLA+로 검증할 수 있는 것과 없는 것

핵심 요약

• AI 안전을 TLA+ 형식검증으로 완전히 해결할 수 있다는 기대가 커지고 있지만, 실제 한계가 크다.
• TLA+는 시스템을 상태 수열로 나누고, 각 상태에서 불린 식을 표현하며 항상(always), 다음(prime), 결국(eventually) 같은 시간논리 연산자로 성질을 정의한다.
• 불변식(invariants)과 안전 성질(safety properties)은 TLA+의 가장 기본적인 검증 대상이며, 생생성 성질(liveness properties)은 좋은 일이 언젠가 일어남을 보장한다.
• TLA+가 검증할 수 없는 첫 번째 한계는 형식화 불가능한 성질들이다. 새의 개념 같은 인간의 직관을 논리식으로 표현할 수 없으면 검증도 불가능하다.
• 다중 단계에 걸친 성질('delete 후 undo하면 원래 상태'처럼)이나 부동소수점 연산, 실제 시간에 관한 성질도 네이티브로는 정의할 수 없다.
• TLA+ 성질은 모든 가능한 행동 수열에 대해 암묵적으로 전체한정되므로, '특정 행동이 가능하다'는 도달 가능성 성질을 직접 표현할 수 없다.
• 게임이 이길 수 있는지 증명하거나, 에너지절약 모드가 항상 더 적은 전력을 쓴다는 (두 행동 수열을 비교하는) 초성질도 TLA+로 표현 불가능하다.
• 상태 공간 전체에 대한 성질('상태 X에서 Y로 가는 경로가 하나뿐'처럼)도 검증할 수 없다.
• 보조 변수나 자기합성 같은 우회 기법으로 일부 한계를 극복할 수 있지만, 이들은 세밀한 설정이 필요하고 모델을 실제 시스템과 맞지 않게 만들며 다른 TLA+ 기능과 조화롭지 않다.
• CTL, PRISM 같은 다른 도구를 사용하면 도달성이나 확률 성질을 검증할 수 있지만, 각각 다른 영역에서 TLA+보다 약하다.
• TLA+는 불변식과 생생성 성질로 커버되는 많은 저수준 문제를 잘 검증하지만, 표현 불가능한 성질이 매우 많아서 형식검증의 만능 도구가 아니다.