Bound-Founded Semantics for Answer Set Programming with Difference Constraints: Preliminary Report

당신이 논리와 수학의 규칙이 완벽한 조화를 이루며 공존하는 도시를 건설하려는 숙련된 건축가라고 상상해 보십시오. 이 세계는 **답집합 프로그래밍(Answer Set Programming, ASP)**의 세계이며, 이는 컴퓨터에게 사실과 규칙의 목록을 제공함으로써 복잡한 퍼즐을 해결하는 방법을 알려주는 방식입니다. 보통 이러한 퍼즐은 "전등이 켜져 있다" 또는 "문이 잠겨 있다"와 같은 참 또는 거짓의 진술에 관한 것입니다. 하지만 현실 세계는 단순히 흑백 논리로만 이루어져 있지 않습니다. 숫자, 거리, 그리고 한계로 가득 차 있습니다. 만약 당신이 컴퓨터에게 "온도가 70도 이상일 때만 전등이 켜진다"라고 말하고 싶다면 어떻게 해야 할까요? 바로 여기서 **선형 제약 조건(linear constraints)**이 등장하며, 이를 통해 프로그램이 논리와 함께 수학을 다룰 수 있게 됩니다.

오랫동안 컴퓨터 과학자들은 이 두 세계를 결합하려고 노력해 왔습니다. 어떤 시스템은 수학 규칙을 엄격하고 변하지 않는 사실으로 취급하는 반면, 다른 시스템은 그것을 증명되어야 할 유연한 제안으로 취급합니다. 문제는 이러한 서로 다른 시스템들이 서로 다른 "언어"를 사용하며, 무엇이 유효한 해답인지에 대해 합의하지 못한다는 점입니다. 이는 마치 세 그룹의 건축가가 동일한 도시를 건설하려고 하는데, 한 그룹은 다리가 존재할 '수 있다면' 유효하다고 생각하고, 다른 그룹은 다리가 '가장 짧은' 형태여야만 유효하다고 생각하며, 세 번째 그룹은 다리가 '증명된' 재료로 만들어져야만 유효하다고 생각하는 것과 같습니다. 단일화된 설계도가 없다면, 어떤 도시가 "정답"인지 혹은 어떻게 설계를 개선해야 하는지 알기 어렵습니다. 이 논문은 이 모든 접근 방식을 하나의 지붕 아래에서 이해하고 비교할 수 있는 방법을 제공함으로써, 이 누락된 설계도를 제시하고자 합니다.

---

거대한 논리 퍼즐: 수학과 규칙의 통합

컴퓨터 과학의 세계에서는 논리와 숫지 사이의 매혹적인 줄다리기가 일어나고 있습니다. 한쪽에는 **답집합 프로그래밍(ASP)**이 있습니다. 이는 컴퓨터가 규칙에 기반하여 어떤 사실이 "참"인지 파악함으로써 복잡한 문제의 해답을 찾는 강력한 도구입니다. 이를 탐정이 증거의 명확한 사슬이 이어질 때만 용의자가 유죄라고 믿는 과정이라고 생각하십시오. 다른 한쪽에는 **차이 제약 조건(difference constraints)**이 있습니다. 이는 "도시 A와 도시 B 사이의 거리는 10마일 미만이어야 한다"와 같은 세련된 수학적 규칙입니다.

문제는 탐정의 논리와 수학자의 규칙을 결합하려고 할 때 상황이 복잡해진다는 것입니다. 서로 다른 컴퓨터 시스템들(clingo[DL], clingcon, flingo)은 이 혼합을 완전히 다른 방식으로 처리합니다. 어떤 시스템은 매우 엄격합니다. 그들은 규칙이 특정 숫자를 강제할 때만 그 숫자가 값을 갖는다고 말합니다. 다른 시스템은 더 느슨하여, 일반적인 규칙에 부합하기만 하면 숫자들이 자유롭게 움직일 수 있도록 허용합니다. 이는 "사이먼 가라사대, 빨간 사각형 위에 서라"라고 말하는 버전과 "사이먼 가라사대, 파란색이 아닌 아무 사각형에나 서라"라고 말하는 버전이 있는 '사이먼 가라사대' 게임과 같습니다. 어떤 버전을 플레이하느냐에 따라 게임판의 모습은 완전히 달라집니다.

스페인, 미국, 독일의 연구진으로 구성된 이 논문의 저자들은 이 혼란을 해결하기로 했습니다. 그들은 이 모든 서로 다른 시스템이 어떻게 작동하는지 설명할 수 있는 단일한 보편적 언어를 만들고자 했습니다. 그래야만 왜 그 시스템들이 그렇게 행동하는지 이해하고, 더 나아가 더 나은 시스템을 구축할 수 있기 때문입니다.

"경계-근거(Bound-Founded)" 설계도

이를 해결하기 위해 연구팀은 **HTb(Bound-founded Logic of Here-and-There)**라고 불리는 새로운 종류의 논리적 프레임워크를 발명했습니다. 만약 이전의 시스템들을 서로 다른 방언이라고 가정한다면, 이 새로운 프레임워크는 그 모든 것을 이해할 수 있는 보편적인 번역기와 같습니다.

흥식한 점은, 그들이 다양한 유형의 변수들(예: "참/거짓" 사실과 "숫자")을 논리적 생태계 내의 서로 다른 "종(species)"으로 취급했다는 것입니다. 이 새로운 시스템에서 그들은 숫자를 위한 특별한 "순서 도메인(ordered domain)"을 만들었습니다. 이를 사다리라고 생각해 보십시오. 어떤 시스템에서 사다리는 평평합니다(무순서). 즉, 규칙에 맞는 어떤 숫자라도 괜찮습니다. 반면, 널리 사용되는 **clingo[DL]**와 같은 시스템에서 사다리는 특정한 순서를 가지며, 시스템은 규칙을 만족하는 가장 낮은 단계의 발판만을 수용합니다.

논문은 이 "다중 분류(many-sorted)" 접근 방식(서로 다르지만 연결된 세계에 각기 다른 유형의 것들이 거주하는 방식)을 사용함으로써, 각 시스템이 어떻게 유효한 해답을 결정하는지 수학적으로 정확히 증명할 수 있음을 보여줍니다. 그들은 **clingo[DL]**가 산을 오르는 가장 짧은 경로를 선택하는 등산객처럼, '최소한의' 또는 '가장 작은' 유효한 숫자를 찾는 방식으로 작동함을 입증했습니다. 그들은 이러한 동작이 단순히 소프트웨어의 무작위적인 특이점이 아니라, 그들의 새로운 논리를 사용하여 완벽하게 설명될 수 있는 특정한 유형의 "평형 모델(equilibrium model)"임을 증명했습니다.

"근거 있음(Founded)" 대 "외부적(External)" 논쟁

이 논문에서 발견한 가장 큰 발견 중 하나는 이 시스템들이 무엇을 "정당화된 것"으로 간-주하는지에 대한 방식입니다. 논리학에서 어떤 사실이 "근거가 있다(founded)"는 것은 씨앗으로부터 자라나는 나무처럼 견고한 시작점으로 추적될 수 있음을 의미합니다. 만약 어떤 사실이 "근거가 없다(unfounded)"면, 그것은 뿌리 없이 공중에 떠 있는 나무와 같습니다.

연구진은 세 가지 주요 시스템이 "수학적 원자(math atoms)"(숫자와 관련된 규칙)를 매우 다르게 처리한다는 것을 발견했습니다.

• Clingcon은 모든 수학 규칙을 "외부적(external)" 사실으로 취야합니다. 이는 "우리는 이 숫자들을 주어진 것으로 받아들일 뿐, 그것들을 증명할 필요가 없다"라고 말하는 것과 같습니다.
• Flingo는 그것들을 "근거가 있는(founded)" 것으로 취급합니다. 그것은 "증거를 보여라! 이 숫자가 필요하다는 것을 증명할 수 없다면, 그것은 존재하지 않는다"라고 주장합니다.
• **Clingo[DL]**는 중간 지점을 취하지만 "근거 있음"과 "최단 경로" 규칙에 크게 의존합니다. 그것은 "만약 이 숫자가 필요하다는 것을 증명할 수 있다면 수용하겠지만, 오직 가능한 가장 작은 숫자여야 한다"라고 말합니다.

논문은 이 시스템들이 단순히 무작위적인 변형이라는 생각을 명시적으로 배제합니다. 대신, 그들의 차이는 두 가지 주요 선택에서 기인한다는 것을 보여줍니다: 숫자를 위한 순서 있는 사다리를 사용하는가? 그리고 수학 규칙을 증명된 사실으로 취급할 것인가, 아니면 단순히 주어진 입력으로 취급할 것인가?

미래를 위한 의미

저자들은 단순히 문제를 기술하는 데 그치지 않고, 이를 해결할 도구를 구축했습니다. 그들은 이 모든 서로 다른 시스템을 자신들의 새로운 "HTb" 언어로 번역할 수 있음을 보여주었습니다. 이는 미래에 개발자들이 어떤 시스템을 사용할지 고민하거나 서로 다른 언어를 사용하고 있을까 봐 걱정할 필요가 없음을 의미합니다. 그들은 이 통합된 프레임워크를 사용하여 다음을 수행할 수 있습니다:

1. 시스템이 왜 특정 답을 내놓는지 정확히 이해한다.
2. 논리를 깨뜨리지 않으면서 불필요한 규칙을 제거하여 프로그램을 단순화한다.
3. 기존의 장점들을 혼합하여 새로운 시스템을 설계한다.

예를 들어, 만약 당신이 **clingo[DL]**처럼 작동하는 시스템을 원한다면, 숫자의 "사다리"를 올바르게 설정하고 시스템이 가장 작은 유효한 단계를 찾도록 지시하기만 하면 됩니다. 만약 clingcon과 같은 시스템을 원한다면, 사다리를 제거하고 모든 것을 주어진 것으로 취급하면 됩니다.

연구진은 자신들이 논리를 성공적으로 매핑하고 이 시스템들이 어떻게 연관되는지 증명했지만, 우주의 모든 가능한 수학 문제를 "해결"했다고 주장하는 것이 아님을 주의 깊게 밝히고 있습니다. 대신, 그들은 이러한 시스템들이 오늘날 어떻게 작동하는지를 설명하는 엄격하고 수학적인 토대를 제공했습니다. 그들은 혼란스러운 다양한 규칙의 덩어리를 명확하고 조직화된 지도로 바꾸어 놓았으며, 이 하이브리드 논리 시스템들의 표면 아래에서 그들이 실제로 동일한 근본적인 언어를 말하고 있다는 것을 보여주었습니다. 단지 서로 다른 억양을 가지고 있을 뿐입니다.

결국, 이 논문은 논리 프로그래밍의 로제타 스톤을 찾는 것과 같습니다. 이것은 우리가 한 시스템의 지침을 읽고 다른 시스템들이 무엇을 하고 있는지 정확히 이해할 수 있게 해주며, 마음의 논리와 세상의 수학을 모두 다룰 수 있는 더 스마트하고 유연하며 신뢰할 수 있는 컴퓨터 프로그램을 위한 길을 열어줍니다.