Nonlinear Arithmetic with SMTLIB Division is Undecidable

마치 매우 엄격한 규칙 세트를 사용하여 미스터리를 해결하려는 형사라고 상상해 보세요. 컴퓨터 과학 세계에서 이러한 규칙은 "이론"이라고 불리며, 컴퓨터가 수학 퍼즐에 해가 있는지 여부를 결정하는 데 도움을 줍니다.

이 논문은 **비선형 실수 산술 (Nonlinear Real Arithmetic, NRA)**이라는 특정 규칙 세트에 관한 것입니다. 이를 실수 (3.14, -5, 0.001 등) 로 이루어진 게임으로 생각할 수 있으며, 여기서 당신은 이 수들을 더하고, 빼고, 곱하고, 나눌 수 있습니다.

게임을 무너뜨리는 "마법" 규칙

오랫동안 수학자들은 이 게임이 완벽하게 해결 가능하다고 믿었습니다. 컴퓨터에 이러한 숫자를 사용한 퍼즐을 주면, 결국 "네, 해가 있습니다" 또는 "아니요, 해가 없습니다"라고 말할 수 있었습니다.

그러나 저자 데얀 조바노비치 (Dejan Jovanović) 는 공식 규칙서 (SMTLIB 표준) 에 숨겨진 함정을 발견했습니다. 그 함정은 규칙들이 0 으로 나누기를 처리하는 방식에 있습니다.

일반적인 수학에서 0 으로 나누기는 큰 "아니요"입니다. 하지만 이 특정 컴퓨터 규칙서에서는 규칙이 이렇게 말합니다: "0 으로 나누는 경우, 답이 무엇인지 우리는 신경 쓰지 않습니다. 0 으로 나누지 않을 때 일반 숫자처럼 행동하는 한, 무엇이든 될 수 있습니다."

저자는 이를 **"해석되지 않은 함수 (uninterpreted function)"**라고 부릅니다. 비유를 들어보겠습니다: 모든 간식을 구매할 때 완벽하게 작동하는 자판기를 상상해 보세요. 하지만 "영 (Zero) 간식"을 구매하려고 하면, 기계가 고장 나지 않습니다. 대신 무언가를 뱉어냅니다. 아마도 캔디 바일 수도 있고, 돌일 수도 있고, 구름일 수도 있습니다. 규칙은 그것이 무엇이 될지 알려주지 않습니다. 그저 "무언가가 될 것"이라고만 말합니다.

어떻게 이 게임이 해결 불가능하게 되는가

이 논문은 0 나누기에 대한 "무엇이든 가능"한 규칙이 혼란의 문을 여는 열쇠라고 주장합니다.

논리를 단순화하면 다음과 같습니다:

1. 목표: 저자는 이 "마법" 나눗셈 규칙이 있다면, 컴퓨터를 속여 정수 퍼즐 (1, 2, 3 과 같은 정수 퍼즐) 을 해결하게 할 수 있음을 증명하고자 합니다.
2. 문제: 정수 퍼즐을 해결하는 것은 모든 경우에 대해 컴퓨터가 완벽하게 수행하는 것이 유명한 불가능한 일입니다 (힐베르트의 10 번 문제라고 알려져 있습니다). 이는 영원히 자라나는 건초더미 속에서 바늘을 찾으려는 것과 같습니다.
3. 기교: 저자는 "마법" 0 나누기를 사용하여 수학적 다리를 구축할 수 있음을 보여줍니다. 어려운 정수 퍼즐을 가져와 이 나눗셈 기교를 사용하여 실수 퍼즐로 번역할 수 있습니다.
   • 비유: 인간만이 이해할 수 있는 언어 (정수) 로 작성된 비밀 코드가 있다고 상상해 보세요. 당신은 이 코드를 컴퓨터가 이해할 수 있는 언어 (실수) 로 번역하는 기계 (나눗셈 기교) 를 만듭니다. 컴퓨터의 언어에는 이 "마법" 0 나누기 규칙이 있기 때문에, 컴퓨터는 우연히 인간의 코드를 해결할 수 있게 됩니다.
4. 결과: 컴퓨터가 모든 정수 퍼즐을 해결할 수 없다는 것이 알려져 있고, 이 기교가 컴퓨터로 하여금 실수를 사용하여 정수 퍼즐을 해결하려 하게 만들기 때문에, 이는 컴퓨터가 모든 실수 퍼즐도 해결할 수 없음을 의미합니다. 게임은 **결정 불가능 (undecidable)**해집니다.

"바닥 (Floor)" 함수 비유

이를 증명하기 위해 저자는 교묘한 기교를 사용합니다. 그들은 이 "마법" 나눗셈이 있다면, 컴퓨터를 **바닥 함수 (floor function, 3.9 를 3 으로 반올림하는 것처럼 수를 가장 가까운 정수 아래로 반올림하는 함수)**처럼 작동하게 만들 수 있음을 보여줍니다.

컴퓨터가 수를 아래로 반올림할 수 있게 되면, 정수를 세기 시작할 수 있습니다. 정수를 셀 수 있게 되면, 그 불가능한 정수 퍼즐들을 해결하려 할 수 있습니다. 이러한 퍼즐들은 일반적으로 해결할 수 없으므로, 이 나눗셈 규칙을 포함한 실수 수학 전체 시스템도 일반적으로 해결할 수 없게 됩니다.

현실 세계에 대한 의미 (논문에 따르면)

이 논문은 미래의 AI 나 의학적 용도에 대해 이야기하지 않습니다. 현재 컴퓨터 벤치마크 (테스트 문제) 의 상태에 초점을 맞춥니다:

• 함정: SMTLIB 라이브러리 (컴퓨터를 테스트하는 데 사용되는 거대한 수학 퍼즐 모음) 에 있는 많은 기존 테스트 문제들은 변수를 사용한 나눗셈 (예: x / y) 을 사용합니다. 만약 y 가 우연히 0 이 된다면, 이러한 퍼즐들은 "결정 불가능"한 함정에 빠집니다.
• 해결책? 저자는 규칙서를 수정하는 두 가지 방법을 제안합니다:
  1. 특정 답을 선택하기: 0 으로 나누는 것이 항상 특정 숫자 (0 또는 1 등) 와 같다고 결정합니다. 이는 일부 컴퓨터 시스템이 이진수를 처리하는 방식과 유사합니다.
  2. 게임을 분리하기: 변수로 나누는 문제에 대한 새롭고 별도의 카테고리를 만들고, 알려진 숫자 (상수) 로만 나누는 문제에 대해서는 "안전한" 카테고리를 유지합니다.

결론

이 논문은 컴퓨터가 "0 으로 나누기"를 처리하는 방식에 대한 특정이고 겉보기에 무해한 규칙이 실수를 포함한 모든 수학 문제를 해결하는 컴퓨터의 능력을 우연히 무너뜨린다고 주장합니다. 이는 컴퓨터가 해결할 수 없어야 할 문제를 은밀히 해결하게 함으로써 해결 가능한 게임을 해결 불가능한 것으로 만듭니다.