Semi-Competitive Differential Game Logic

당신이 두 자율 시스템(자율주나 드론 같은 것들)이 서로 상호작용할 때 안전을 유지할 수 있는지 검증하려고 한다고 상상해 보십시오. 과거에 컴퓨터 과학자들은 이러한 상호작용을 확인하기 위해 "제로섬(zero-sum)" 접근 방식을 사용했습니다. 이것은 마치 체스 게임과 같습니다. 한 명의 플레이어가 승리하면, 다른 한 명은 반드시 패배해야 합니다. 이 논리는 다른 모든 에이전트가 자신을 들이받으려는 악의적인 적이라고 가정했습니다. 이는 안전하긴 하지만, 지나치게 비관적일 수 있습니다. 현실 세계에서 두 대의 비행기는 서로 충돌하고 싶어 하지 않습니다. 그들은 둘 다 안전하게 착륙하기를 원합니다. 비록 서로 다른 방향으로 가고 싶어 할지라도 말입니다. 그들은 적이 아니라, 단지 서로 다를 뿐입니다.

이 논문은 이러한 현실 세계의 상황, 즉 에이전트들이 완전한 적도 아니면서 완벽한 팀원도 아닌 상황을 다루기 위해 dGLsc(준경쟁적 미분 게임 논리, Semi-Competitive Differential Game Logic)라는 새로운 논리를 소개합니다.

다음은 일상적인 비유를 사용하여 이 논문의 개념을 정리한 것입니다:

1. 문제점: "편집증" vs "순진함"

저자들은 기존의 도구들이 우리에게 두 가지 나쁜 선택지 중 하나를 강요한다고 주장합니다:

• 편집증적 관점 (제로섬): 우리는 상대방이 우리를 해치려는 악당이라고 가정합니다. 이는 지나치게 조심스러운 결과를 초래합니다. 예를 들어, 자율주행 자동차는 상대 차량이 단순히 주차를 하려는 것뿐인데도, 그 차가 자신을 들이받으려 한다고 가정하여 아예 움직이지 않기로 결정할 수 있습니다.
• 순진한 관점: 우리는 모든 사람이 항상 우리를 도와줄 완벽한 친구라고 가정합니다. 이는 위험합니다. 왜냐하면 오해가 발생할 수 있고, 사람들이 이미 "졌다"고 생각하면 협력하지 않을 수도 있기 때문입니다.

해결책: 준경쟁성 (Semi-Competitiveness).
이 논문은 중간 지대를 제안합니다. 앨리스와 밥이 산 정상으로 걸어가는 모습을 상상해 보십시오.

• 두 사람 모두 정상에 도달하고 싶어 합니다 (공통된 안전 목표).
• 하지만 앨리스는 왼쪽 길로 가고 싶어 하고, 밥은 오른쪽 길로 가고 싶어 합니다 (개별적인 목표).
• 준경쟁적 행동이란 다음과 같습니다: "내가 나의 목표를 달 이루는 데 도움이 된다면, 나는 당신의 목표를 이루도록 도울 것이다. 만약 우리가 둘 다 이길 수 있다면, 우리는 협력한다. 하지만 내가 이길 수 없다면, 나는 당신을 돕기 위해 나 자신을 희생하지는 않을 것이다."
• 결정적으로, 앨리스는 밥이 비협조적일 것이라고 생각한다면 그를 맹목적으로 신뢰하지 않을 것입니다. 그들은 서로의 목표에 대해 알고 있는 바에 따라 이성적으로 행동합니다.

2. "사탕" 비유

논문은 왜 이 논리가 필요한지를 설명하기 위해 사탕 예시를 사용합니다.
앨리스와 밥이 서로를 위해 사탕을 고르고 있다고 상상해 보십시오.

• 앨리는 밥에게 그가 좋아하는 딸기 사탕을 주고 싶어 합니다.
• 밥은 앨리스에게 그녀가 좋아하는 레몬 사탕을 주고 싶어 합니다.
• 만약 그들이 "제로섬" 게임(적 관계)을 한다면, 앨리스는 밥을 짜증 나게 하기 위해 레몬 사탕을 줄 것이고, 밥도 똑같이 할 것입니다. 둘 다 패배합니다.
• 만약 그들이 "준경쟁적" 게임을 한다면, 앨리스는 밥에게 딸기 사탕을 주는 것이 그를 이기게 하는 데 도움이 된다는 것을 알게 됩니다. 돕는 것이 자신에게 해가 되지 않으므로, 그녀는 그렇게 합니다. 앨리스가 자신을 도왔다는 것을 본 밥은, 자신 또한 앨리스에게 레몬 사탕을 줌으로써 그녀를 이길 수 있다는 것을 깨닫습니다. 둘 다 승리합니다.
• 그러나 이 논리는 "만약 ~라면"의 상황도 고려합니다. 만약 앨리스가 어떻게 해도 이길 수 없는 상황이라면, 그녀는 밥을 돕지 않을 것입니다. 이는 존재하지 않는 마법 같은 협력을 시스템이 가정하는 것을 방지합니다.

3. 작동 방식 (메커니즘)

이 논문은 이러한 상호작용을 위한 수학적 "규칙집"(논리)을 구축합니다.

• 플레이어: 그들은 "천사(Angel, 착한 놈)"와 "악마(Demon, 까다로운 놈)"라고 부르지만, dGLsc에서 그들은 단지 각자의 목표를 가진 두 명의 플레이어일 뿐입니다.
• 게임: 그들은 "하이브리드 시스템" 위에서 게임을 합니다. 이는 연속적으로 변화하는 것(자동차가 속도를 높이는 것 등)과 갑자기 점프하는 것(신호등이 바뀌는 것 등)을 다루는 복잡한 수학적 용어입니다.
• 반전: 기존 논리에서는 천사가 이기면 악마는 집니다. 이 새로운 논리에서는 둘 다 이기거나, 둘 다 지거나, 혹은 한 명은 이기고 다른 한 명은 질 수도 있습니다. 이 논리는 *"상대방이 무엇을 원하는지 안다면, 내가 할 수 있는 가장 영리한 수는 무엇인가?"*라고 물음으로써 "승리 영역"(플레이어가 자신의 목표를 보장할 수 있는 시작 지점들의 집합)을 계산합니다.

4. "마술 트릭" (증명)

저자들은 단순히 이론을 만든 것이 아니라, 증명 계산기를 만들었습니다.

• 그들은 컴퓨터가 시스템이 안전한지 증명하기 위해 따를 수 있는 규칙(레시피와 같은)을 만들었습니다.
• 그들은 이 새로운 논리가 **건전(sound)**하다는 것을 증명했습니다 (즉, 거짓말을 하지 않습니다. 만약 시스템이 안전하다고 말한다면 정말로 안전합니다).
• 그들은 이 논리가 **완전(complete)**하다는 것도 증명했습니다 (즉, 그 규칙 내에서 실제로 참인 모든 것을 증명할 수 있습니다).
• 핵심 통찰: 그들은 이 새로운 논리가 매우 복잡함에도 불구하고, 원한다면 실제로 기존의 "적" 논리로 다시 번역할 수 있다는 것을 보여주었습니다. 하지만 이를 수동으로 번역하는 것은 악몽과 같습니다 (마치 소설의 의미를 포착하는 대신 단어를 일대일으로 직역하는 것과 같습니다). 이 새로운 논리는 "협력 대 경쟁"의 균형을 자동으로 처리하여 엄청난 양의 작업을 절감해 줍니다.

5. 왜 중요한가 (논문에 따르면)

논문은 항공 충돌 방지(비행기 간의 충돌 회피) 사례를 사용합니다.

• 기존 방식: 상대방 비행기를 미사일이라고 가정합니다. 그 결과는 안전하지만 쓸모없는 비행 경로가 됩니다. 즉, 비행기들이 서로 근처에도 가지 못하게 됩니다.
• 새로운 방식 (dGLsc): 상대방 비행기 역시 충돌을 피하고 싶어 하지만, 동시에 자신의 목적지에 도착하고 싶어 한다고 가정합니다. 이 논리는 그들이 중앙 통제 장치의 지시 없이도 서로의 움직임을 조율함으로써 안전하고 효율적으로 비행할 수 있음을 증명합니다.

요약하자면: 이 논문은 두 지능형 에이전트가 "프레너미(frenemies, 친구이자 적)"인 상황을 묘사하는 새로운 수학적 언어를 제공합니다. 그들은 경쟁할 수도 있지만, 그것이 합리적이라면 협력할 만큼 똑똑하며, 협력이 자신에게 승리를 가져다주지 않는다면 협력을 멈출 만큼 똑똑합니다. 이를 통해 엔지니어들은 과도하게 편집증적인 태도를 취하지 않고도 자율주행 자동차와 같은 복잡한 시스템이 안전하다는 것을 증명할 수 있습니다.