The TPTP Format for Interpretations

개요: "만약에"라는 시나리오를 찾아내기

당신이 미스터리를 풀려는 탐정이라고 상상해 보세요. 당신에게는 일련의 규칙(공리)과 어떤 사건에 대한 이론(추측)이 있습니다. 보통 당신의 임무는 그 규칙들에 근거하여 그 이론이 반드시 참임을 증명하는 것입니다.

하지만 때로는 그 이론이 틀렸음을 증명하고 싶을 때가 있습니다. 그러기 위해서는 규칙은 성립하지만 이론은 무너지는 특정한 시나리오, 즉 "반례(counterexample)"를 찾아내야 합니다. 컴퓨터 논리의 세계에서 이 시나리오를 해석(interpretation) 또는 **모델(model)**이라고 부릅니다.

오랫동안 컴퓨터는 이러한 "틀린" 시나리오를 찾아낼 수는 있었지만, 그 결과를 자기들끼리만 알고 있었습니다. 컴퓨터는 그저 "반례를 찾았습니다!"라고 말할 뿐, 그것이 실제로 어떻게 생겼는지는 보여주지 않았습니다. 이는 마치 탐정이 "집사가 범인이 아닙니다"라고 말하면서도, 정작 집사의 알리바이가 무엇인지는 보여주기를 거부하는 것과 같습니다.

이 논문은 컴퓨터가 이러한 시나리오를 기록할 수 있는 새로운 표준화된 방식을 소개합니다. 이를 통해 인간과 다른 컴퓨터들이 이를 읽고, 확인하고, 이해할 수 있게 합니다. 이것은 마치 이러한 대안적 현실들을 위한 보편적인 "설계도"를 만드는 것과 같습니다.

세 가지 유형의 설계도

이 논문은 이러한 시나리오를 구축하는 세 가지 주요 방법을 설명하며, 새로운 포맷은 이 모든 것을 처리할 수 있습니다.

1. 유한한 세계 (타르스키 해석 - Tarskian Interpretations)
특정한 수의 사람과 물건이 존재하는 작고 폐쇄된 방을 상상해 보세요.

• 비유: 클루(Clue) 같은 보드게임을 생각해보세요. 당신에게는 고정된 캐릭터(커널 머스터드, 미시스 피콕), 고정된 방, 그리고 고정된 무기가 있습니다.
• 포맷: 컴퓨터는 목록을 작성합니다: "이 세계에는 정확히 4명의 사람이 있습니다. 커널 머스터드는 서재에 있습니다. 촛대는 주방에 있습니다." 컴퓨터는 모든 연결 관계를 명시적으로 나열합니다.
• 중요한 이유: 이는 시스템이 적은 수의 항목으로 잘 작동하는지 확인하는 데 매우 유용합니다.

2. 무한한 세계 (무한 해석 - Infinite Interpretations)
이제 숫자 선(1, 2, 3, 4... 영원히)처럼 끝이 없는 세계를 상상해 보세요.

• 비유: 무한한 숫자의 목록을 적을 수는 없습니다. 대신 레시피나 규칙을 적습니다: "0에서 시작한다. 다음 숫자를 얻으려면 1을 더한다."
• 포맷: 컴퓨터는 모든 숫자를 나열하지 않습니다. 대신 "임의의 숫자 $X$에 대하여, 다음 사람은 $X+1$이다"와 같은 규칙을 사용합니다. 수학 공식을 사용하여 무한한 군중을 묘라는 식입니다.
• 중요한 이유: 이는 시간, 돈, 또는 한계 없이 늘어날 수 있는 데이터와 같이 다루는 데 필요합니다.

3. 멀티버스 (크립키 해석 - Kripke Interpretations)
때때로 규칙은 당신이 어디에 있는지, 혹은 언제 보느냐에 따라 달라집니다.

• 비유: "당신의 선택에 따라 결말이 달라지는(Choose Your Own Adventure)" 책이나 멀티버스 영화를 생각해보세요. 한 방(세계 A)에서는 비가 내립니다. 다음 방(세계 B)에서는 햇빛이 납ند습니다. 캐릭터들은 각 방마다 다를 수도 있고, 그대로일 수도 있습니다. 방들 사이에는 연결 통로(접근성)가 있습니다.
• 포맷: 컴퓨터는 모든 방의 지도, 열려 있는 문, 그리고 각 방의 날씨를 기록합니다. "세계 1에서는 비가 온다. 세계 2에서는 햇빛이 난다. 세계 1에서 세계 2로 갈 수는 있지만, 돌아올 수는 없다"라고 기록합니다.
• 중요한 이유: 이는 보안 프로토콜이나 AI 추론처럼 진실이 맥락에 따라 달라지는 상황에서 매우 중요합니다.

포맷을 위한 "레시피"

이 논문은 TPTP라고 불리는 특정 언어를 사용하여 이러한 설계도를 정확히 어떻게 작성하는지 상세히 설명합니다. TPTP를 논리를 위한 보편적인 프로그래밍 언어라고 생각하면 됩니다.

• 재료: 이 포맷은 "도메인"(방 안에 누가 있는지), "매핑"(누가 무엇을 하는지), 그리고 "규칙"(무엇이 참인지 거짓인지)을 정의할 것을 요구합니다.
• 유연성: 이 포맷은 똑똑합니다. 전체 세계를 설명하는 크고 복잡한 문단 형태인 거친 입자(coarse-grained) 방식이 될 수도 있고, 개별 사람과 물건을 상세히 나누어 놓은 상세한 스프레드시트 형태인 가는 입자(fine-grained) 방식이 될 수도 있습니다.
• "헤브란드(Herbrand)" 특수 사례: 때때로 "세계"는 컴퓨터가 스스로 생성한 단어와 문장들의 목록일 뿐입니다. 논문에서는 이를 "헤브란드 해석"이라고 부릅니다. 이는 사전의 정의가 전적으로 사전 속의 단어들로만 구성되어 있는 사전과 같습니다.

왜 이것이 필요한가? ("믿어달라는 문제")

논문은 단순히 해결책을 찾는 것만으로는 충분하지 않으며, 이를 **검증(verify)**해야 한다고 주장합니다.

• 과거의 방식: 컴퓨터가 "버그를 찾았습니다!"라고 말합니다. 그러면 당신은 컴퓨터를 믿어야만 합니다. 만약 컴퓨터가 실수를 했다면, 당신은 망가진 시스템을 떠안게 됩니다.
• 새로운 방식: 컴퓨터가 당신에게 설계도(해석)를 건네줍니다. 당신(또는 다른 컴퓨터)은 그 설계도를 읽고 수학을 확인할 수 있습니다.
  • 읽을 수 있는가? 네, 포맷은 인간이 읽을 수 있도록 설계되었습니다.
  • 확인할 수 있는가? 네, 설계도가 실제로 규칙을 따르는지 확인하기 위해 간단한 테스트를 실행할 수 있습니다.
  • 유용한가? 네, 버그를 발견했을 때 설계도는 정확히 어디에서 오류가 발생했는지 보여줍니다 (예: "존은 주방에 있지만, 규칙에 따르면 서재에 있어야 한다").

"도구 상자"

논문은 이를 돕기 위해 이미 존재하는 도구들을 언급합니다.

• 시각화 도구 (Visualizers): 특정 "세계"를 클릭하여 그 안의 캐릭터들을 볼 수 있는 3D 지도라고 상상해 보세요. 논문은 유한한 세계에 대해 정확히 이 기능을 수행하는 "대화형 해석 뷰어(Interactive Interpretation Viewer, IIV)"라는 도구를 언급합니다.
• 검증 도구 (Verifiers): 설계도와 원래의 규칙을 가져와서 두 가지가 서로 일치하는지 자동으로 확인하는 도구입니다.

요약

요약하자면, 이 논문은 컴퓨터가 자신의 "만약에" 시나리오를 공유하는 방식을 표준화하는 것에 관한 것입니다.

이전에는 컴퓨터가 반례를 찾아내긴 했지만, 그것을 검은 상자(black box) 안에 숨겨두었습니다. 이제 컴퓨터는 이를 명확하고 표준화된 "설계도" 언어로 작성할 수 있습니다. 이를 통해 인간은 설계도를 보고 시스템이 왜 실패했는지 이해할 수 있으며, 컴퓨터가 실수를 하지 않았는지 검증할 수 있습니다. 이는 "믿어달라"는 순간을 "보여달라"는 순간으로 바꾸어 놓습니다.