인터넷이 TLA+를 발견했습니다. 이제 어떻게 될까요?
1. 이게 뭔가요?
보리스 체르니라는 개발자가 30년이 넘은 컴퓨터 시스템 설계 및 검증 도구인 티엘에이플러스를 인공지능 기술과 함께 소개한 글이 소셜 미디어에서 큰 관심을 받았습니다. 티엘에이플러스는 복잡한 소프트웨어가 오류 없이 작동하는지 수학적으로 증명하는 도구입니다.
2. 왜 화제인가요?
과거에는 사람이 일일이 수작업으로 해야 했던 복잡한 시스템 검증 과정을 최신 인공지능 기술을 통해 대규모로 자동화할 수 있게 되었기 때문입니다. 단순한 프로그램 설계도를 넘어 실제 컴퓨터 코드가 오류 없이 작동함을 엄격하게 증명하는 새로운 가능성이 주목받고 있습니다.
3. 핵심 내용
컴퓨터 시스템은 여러 장치가 올바른 순서로 소통하고 오류 없이 결정을 내려야 합니다. 이를 설계하고 검증하기 위해 사용하는 티엘에이플러스는 시스템이 가질 수 있는 가능한 행동들과 시간이 흐름에 따라 만족해야 하는 성질들을 간결한 언어로 표현합니다. 예를 들어 세 대의 컴퓨터가 서로 소통하여 리더를 선출할 때 동시에 두 명의 리더가 절대 생기지 않는다는 안전성 규칙과 언젠가는 반드시 리더가 선출된다는 생동성 규칙을 정의하고 검증할 수 있습니다. 티엘에이플러스는 시스템의 설계도를 검사하는 유용한 도구이지만, 정해진 규모 안에서만 상태를 탐색하고 실제 프로그램 코드와는 따로 떨어져 있다는 한계가 있습니다. 이러한 한계를 극복하기 위해 최신 수학적 증명 시스템과 실제 프로그래밍 언어로 작성된 코드를 연결하려는 시도가 이루어지고 있습니다. 특히 베루스라는 도구는 설계 규칙과 증명을 실제 프로그램 코드와 나란히 둘 수 있어 설계와 실제 구현 사이의 간격을 좁혀줍니다. 프로그램이 제대로 작동하는지 증명하는 과정은 가능한 행동을 나누어 불변식을 추적하거나 수치가 줄어드는 것을 확인하는 등의 반복적인 작업이 많기 때문에, 인공지능이 이를 자동화하기에 매우 알맞은 분야입니다. 연구진은 1만 6,459개의 실제 티엘에이플러스 설계 명세와 성질 쌍을 베루스 증명 코드로 바꾸는 자동화 번역기를 개발하고, 인공지능이 증명을 작성하고 다른 인공지능이 검토하는 순환 구조를 구축했습니다. 이를 통해 컴퓨터가 기계적으로 검증한 3,000개 이상의 안전성 및 생동성 증명을 만들어내며 인공지능 모델들의 성능을 평가했습니다.
4. 나에게 어떤 영향이 있나요?
일반 사용자가 당장 직접 다운로드하거나 설정을 바꿀 일은 없지만, 우리가 일상적으로 사용하는 클라우드 서비스나 데이터베이스, 대형 플랫폼의 백그라운드 안정성이 앞으로 인공지능과 고급 검증 기법을 통해 더욱 탄탄해질 수 있습니다. 소프트웨어를 개발하는 엔지니어 입장에서는 사람이 수작업으로 하던 복잡하고 반복적인 수학적 증명 작업을 인공지능이 대신 처리해 주는 미래의 개발 환경을 엿볼 수 있습니다.