A coalgebraic higher-order modal fixed-point logic

당신이 컴퓨터에게 미래를 생각하는 법을 가르치려 한다고 상상해 보세요. 당신은 교통 신호 체계, 비디오 게임 세계, 또는 로봇의 의사 결정 과정과 같은 복잡한 시스템을 바라보며 다음과 같은 질문에 답하기를 원합니다. "이 로봇이 영영 갇히게 될까?", 혹은 "로봇이 반드시 승리하는 경로가 존재할까?" 수십 년 동안 컴퓨터 과학자들은 이러한 질문을 던지기 위해 '모달 로직(modal logic, 양상 논리)'이라 불리는 특별한 수학적 언어를 사용해 왔습니다. 이 언어를 일종의 마법 주문 세트라고 생각해 보세요. 어떤 주문은 어떤 일이 '지금 당장' 일어나는지를 확인하고, 다른 주문은 어떤 일이 '결국에는' 일어날 것인지를 확인합니다.

하지만 현실 세계는 무질서합니다. 때때로 시스템은 단순히 '켜짐' 또는 '꺼짐' 상태가 아닙니다. 왼쪽으로 갈 확률이 70%, 오른쪽으로 갈 확률이 30%일 수도 있습니다. 또한, 어떤 경우에는 관점에 따라 게임의 규칙이 변하기도 하며, 시스템이 너무 복잡해서 함수가 다른 함수에 작용하는 경우(예를 들어, 재료 목록을 스스로 작성하는 레시피와 같은 경우)도 있습니다. 이러한 문제를 다루기 위해 과학자들은 두 가지 강력한 도구를 개발했습니다. 하나는 확률이 있는 시스템(동전 던지기와 같은)을 위한 것이고, 다른 하나는 고차원적 복잡성(규칙이 규칙을 바꾸는 경우)을 가진 시스템을 위한 것입니다. 여기서 큰 질문은 이것입니다. "우리가 이 두 세계를 동시에 이해할 수 있는 단 하나의 보편적인 '마스터 언어'를 구축할 수 있을까?" 이것이 바로 컴퓨터 과학자 라이언 테이(Ryan Tay), 하쉬 베오하르(Harsh Beohar), 찰스 그렐로이스(Charles Grellois)가 해결하고자 했던 퍼즐입니다.

컴퓨터 세계를 위한 만능 번역기

이 논문에서 저자들은 코알제브라 고차 모달 고정점 논리(Coalgebraic Higher-Order Modal Fixed-Point Logic, 줄여서 "Coalgebraic HFL")라는 새로운 초강력 언어를 소개합니다. 이것이 무엇인지 이해하기 위해, '코알제브라(coalgebra)'를 무서운 수학 용어가 아니라 모든 움직이는 시스템에 대한 '보편적인 설계도'라고 상상해 보세요. 단순한 교통 신호든, 복잡한 로봇이든, 혹은 확률적인 게임이든, 코알제브라는 시스템이 한 상태에서 다음 상태로 어떻게 이동하는지를 설명하는 방식일 뿐입니다.

저자들은 이미 복잡하고 높은 수준의 규칙을 다루는 데 능숙했던 기존의 논리 언어(HFL)를 가져와서, 여기에 **프레디케이트 리프팅(predicate liftings)**이라는 새로운 '안경'을 씌워 주었습니다. 이 안경을 '어댑터'라고 생각해 보세요. 이전에는 이 논리가 특정 유형의 시스템만을 볼 수 있었다면, 이제 이 어댑터를 통해 논리는 단순한 예/아니오 선택이든, 복잡한 확률 구름이든, 혹은 고차 함수를 포함한 시스템이든 관계없이 코알제브라 설계도에 부합하는 모든 시스템을 볼 수 있게 되었습니다. 이는 마치 하나의 유니버설 리모컨이 TV, 드론, 스마트 냉장고를 모두 동일한 버튼 세트로 조작할 수 있게 된 것과 같습니다.

거대한 발견: 만물을 다스리는 하나의 논리

이 논문의 주요 발견은 이 새로운 "Coalgebraic HFL"이 두 명성 있는 조상의 역할을 동시에 수행할 만큼 강력하다는 것입니다. 이 언어는 표준 컴퓨터 프로그램(대개 '예/아니오' 결정임)의 논리와 확률적 시스템(어떤 일이 일어날 확률이 존재하는 시스템)의 논리를 모두 설명할 수 있습니다.

이를 증명하기 위해 저자들은 단순히 "작동한다"라고 말하는 대신, 옛 세계의 매우 어려운 두 가지 문제를 이 새로운 언어로 완벽하게 번역할 수 있음을 보여주었습니다.

1. "공집합(Empty Set)" 문제: 비결정론적 기계(여러 경로를 동시에 선택할 수 있는 로봇)를 상상해 보세요. 당신은 로봇이 성공하는 경로가 단 하나라도 있는지, 아니면 어떤 경우에도 실패하는지를 알고 싶습니다. 저자들은 이 질문을 던지는 것이 자신들의 새로운 논리에서 특정 질문을 던지는 것과 정확히 같다는 것을 보여주었습니다.
2. "값-1(Value-1)" 문제: 확률에 기반하여 결정을 내리는 로봇(주사위 던지기와 같은)을 상상해 보세요. 당신은 로봇이 정확히 100%(또는 "1")의 확률로 성공하는 전략이 있는지 알고 싶습니다. 저자들은 이 까다로운 확률 문제가 이 새로운 논리의 모델 체킹(model-checking) 문제로 환원된다는 것을 증명했습니다.

쉽게 말해, 그들은 다리를 놓았습니다. 만약 당신이 새로운 논리에서 문제를 풀 수 있다면, 당신은 사실상 이 옛 세계의 어려운 문제들을 해결한 것입니다. 이는 서로 다른 두 가지 방식의 컴퓨터 시스템 사고를 하나의 지붕 아래로 통합했다는 점에서 매우 중요한 성과입니다.

구현 방법: "서포트(Support)" 기법

이것이 작동하게 만들기 위해 저자들은 규칙을 정의할 때 매우 주의를 기울여야 했습니다. 그들은 시스템의 상태에 대한 일종의 '지문'과 같은 개념인 "서포트(support)"를 도입했습니다. 그들은 만약 시스템이 특정 수학적 규칙(구체적으로, '포함 관계(inclusions)'와 '약한 와이드 풀백(weak wide pullbacks)'을 보존한다는 것, 즉 줌 인/아웃을 해도 시스템이 일관되게 행동한다는 의미)을 따른다면, 어떤 기계에 대해서도 "최댓값(top value)"을 정의할 수 있음을 보여주었습니다.

그 후 그들은 탐정 역할을 하는 특정한 공식(이 논리의 특정 주문)을 구성했습니다. 이 탐정 공식은 기계를 조사하여 그 기계의 "최댓값"을 계산합니다. 만약 기계가 단순한 예/아니오 로봇이라면, 공식은 그것이 언제든 "예"라고 말할 수 있는지 확인합니다. 만약 확률 로봇이라면, 공식은 그것이 100% 성공률에 도달할 수 있는지를 확인합니다. 논문은 이 공식이 내놓는 답이 모든 가능한 시나리오를 통해 로봇을 실행했을 때 얻게 되는 답과 수학적으로 정확히 일치함을 증명합니다.

아직 하지 못한 것 (현재의 한계)

이 논문이 주장하지 않는 부분도 명확히 밝혀두는 것이 중요합니다. 저자들은 자신들의 논리가 확률적 시스템의 본질을 포착하고는 있지만, 현존하는 가장 진보된 확률 논리(PHFL)의 모든 미세한 뉘 Nuance를 다 담아내지는 못한다고 솔직하게 밝히고 있습니다. 구체적으로, "상향 폐쇄 부분 집합(upwards-closed subsets)"(값이 함께 증가하는 그룹을 뜻하는 기술적 표현)과 관련된 매우 복잡한 공식들은 현재 버전에서 완벽하게 처리하지 못합니다. 저자들은 이를 한계점으로 인정하며 향후 과제로 제시했습니다.

또한, 저자들은 이 논리가 이러한 문제들을 표현할 수 있다는 점은 보여주었지만, 실제로 컴퓨터에서 이 논리를 실행하는 것이 얼마나 어려운지에 대해서는 해결책을 제시하지 않았습니다. 실제로 그들은 일부 버전의 시스템(특히 확률과 관련된 경우)에서 공식이 참인지 확인하는 문제가 "결정 불가능(undecidable)"하다는 점을 지적합니다. 이는 어떤 복잡한 시스템의 경우, 어떤 컴퓨터 프로그램도 유한한 시간 내에 정답을 보장할 수 없음을 의미합니다. 저자들은 이 문제를 해결했다고 주장하는 것이 아니라, 단지 이 새로운 논리가 그 문제를 설명하기 위한 올바른 언어임을 보여준 것입니다. 설령 그 문제 자체가 일반적인 경우에 해결 불가능할지라도 말입니다.

이것이 왜 중요한가

왜 호기 ک이 로봇의 경로를 체크하는 논리에 관심을 가져야 할까요? 왜냐하면 세상이 점점 더 자동화됨에 따라, 우리가 만드는 시스템은 그 어느 때보다 더 복잡하고 불확실해지고 있기 때문입니다. 우리는 비와 안개를 다루는 자율주행 자동차(확률)와, 층층이 쌓인 규칙에 따라 결정을 내리는 AI(고차 함수)를 마주하고 있습니다.

이 논문은 이러한 모든 시스템에 대해 이야기할 수 있는 단일하고 통합된 방법론에 대한 이론적 토대를 제공합니다. 새로운 종류의 로봇이나 게임이 나올 때마다 매번 새로운 언어를 발명하는 대신, 우리는 결국 이 "Coalgebraic HFL"을 사용하여 우리의 디지털 세계가 안전하고 공정하며 의도대로 작동하는지 검증할 수 있게 될 것입니다. 이는 기술이 아무리 복잡해지더라도, 우리 기술이 충돌하지 않고, 속이지 않으며, 우리가 요청한 대로 정확히 수행할 것임을 수학적으로 증명할 수 있는 세상을 향한 한 걸음입니다.