Revisiting Incremental Linearization for Nonlinear Integer Arithmetic

당신이 탐정이 되어 미스터리를 풀고 있다고 상상해 보세요. 하지만 당신에게 주어진 단서들은 어떻게 보느냐에 따라 그 의미가 변하는 언어로 쓰여 있습니다. 이것이 바로 컴퓨터 과학의 한 분야인 **만족 가능성 모듈로 이론(Satisfiability Modulo Theories, SMT)**의 세계입니다. SMT는 소프트웨어가 일련의 논리적 규칙들이 동시에 참이 될 수 있는지를 파악하려고 시도하는 과정입니다. 이것을 프로그램이 충돌할지, 비밀 코드를 해독할 수 있을지, 혹은 로봇의 경로가 안전할지를 확인하는 초스마트 퍼즐 해결사라고 생각하면 됩니다.

대부분의 경우, 이 퍼즐들은 직선과 단순한 덧셈(예: $x + y = 5$)만을 포함하므로 해결하기 쉽습니다. 컴퓨터는 이런 작업에 매우 능숙합니다. 하지만 비선형 산술(nonlinear arithmetic)—즉, 곱셈이나 거듭제곱(예: $x \times y$ 또는 $x^3$)이 포함된 규칙이 도입되면 상황은 복잡해집니다. 갑자기 규칙들이 곡선을 그리며 뒤틀리기 시작하고, 수학은 믿기 힘들 정도로 어려워집니다. 실제로 정수론의 관점에서 볼-때, 이러한 모든 퍼즐을 완벽하게 100% 해결할 수 있는 완전한 방법론을 만드는 것은 수학적으로 불가능합니다. 그렇기 때문에 컴퓨터 과학자들은 모든 불가능한 사례를 해결하겠다고 약속하는 대신, 빠르게 답을 찾아낼 수 있는 영리한 지름길을 사용하는 "충분히 좋은" 탐정들을 구축합니다.

당신이 읽게 될 논문은 이전의 탐정들보다 이 까다롭고 구불구불한 퍼즐을 더 잘 해결하는 새로운 탐정인 qfn2l을 소개합니다. 저자들인 체코 기술 대학교(Czech Technical University in Prague)의 연구진은 기존의 지름길들이 특정 유형의 어려운 퍼즐, 즉 거듭제곱(예: $x^3$)이나 혼합 곱(예: $x^2y$)이 포함된 퍼즐에서 고전하고 있다는 점을 깨달았습니다. 그들은 이전보다 더 촘촘한 그물처럼 작동하여, 예전에는 빠져나갔던 잘못된 추측들을 잡아낼 수 있는 새로운 규칙 세트로 탐정의 도구 상자를 업그레이드하기로 했습니다.

과거의 방식: 해석 불가능한 함수를 이용한 추측

이 업그레이드를 이해하기 위해, 이전의 탐정들이 어떻게 작동했는지 살펴봅시다. $f(x, y)$라고 적힌 신비로운 상자가 있다고 상상해 보세요. 당신은 그 안에 무엇이 들어있는지는 모르지만, 같은 숫자를 넣으면 항상 같은 숫자가 나온다는 사실은 알고 있습니다. 기존 방식은 모든 곱셈(예: $x \times y$)을 이 신비로운 상자처럼 취급했습니다. 컴퓨터는 이 상자의 값을 추측하고, 그 값이 타당한지 확인한 뒤, 만약 그렇지 않다면 그 추측을 수정하기 위한 규칙을 추가했습니다.

이 방식은 단순한 경우에는 괜찮았지만, 수박의 무게를 단순히 "무겁다"라고만 아는 상태에서 무게를 맞추려는 것과 같았습니다. 너무 모호했습니다. 퍼즐에 $x^3$과 같은 높은 차수의 거듭제곱이 포함되면 기존의 규칙은 너무 느슨했습니다. 탐정은 값을 추측하고, 컴퓨터는 "아니오, 맞지 않습니다"라고 말한 뒤, 이를 수정하기 위해 매우 약한 규칙을 추가할 뿐이었습니다. 탐정은 답을 찾기도 전에 수백 번을 추측하고 실패하며 결국 시간을 다 써버리곤 했습니다.

새로운 기술: 할선(Secant)으로 그물을 좁히기

이 논문의 저자들은 이러한 거듭제곱을 신비로운 상자로 취급하는 대신, 거듭제곱의 결과값을 나타내는 새로운 상수(fresh constants)—즉, 평범하고 단순한 숫자—로 취급하기로 했습니다. 하지만 진짜 마법은 이 숫자들을 검증하기 위해 추가한 새로운 규칙에 있습니다.

그들은 임의의 정수 $v$에 대해, 함수 $x^k$(예: $x^3$)가 $v$와 $v+1$ 사이에서 매우 예측 가능한 방식으로 행동한다는 것을 발견했습니다. 그들은 **할선(secant lines)**을 기반으로 한 새로운 규칙을 만들었습니다. 그래프 위의 곡선을 상상해 보세요. 할선은 곡선 위의 두 점을 잇는 직선입니다. 저자들은 점 $(v, v^k)$와 그다음 정수 지점 사이를 잇는 직선을 그리면, 그 직선이 곡선 주위에 매우 촘촘한 "울타리"를 형성한다는 것을 깨달았습니다.

여기 비유가 있습니다:

• 과거의 방식: 탐정은 가능한 답 주변에 크고 느슨한 원을 그렸습니다. 그리기는 쉬웠지만, 많은 오답을 허용했습니다.
• 새로운 방식: 탐정은 곡선을 아주 밀착하여 감싸는 일련의 촘촘하고 곧은 직선 울타리(할선)를 그립니다. 만약 어떤 추측이 이 촘촘한 울타리 밖에 떨어진다면, 탐정은 즉시 그것이 틀렸음을 인지하고 추측을 안쪽으로 밀어 넣는 규칙을 추가합니다.

이 울타리들이 매우 촘촘하기 때문에, 탐정은 예전만큼 많이 추측할 필요가 없습니다. 특히 세제곱이나 혼합 곱이 포함된 퍼즐에서 훨씬 빠르게 정답에 수렴합니다.

"세 세제곱수의 합" 챌린지

새로운 탐정이 제대로 작동하는지 증명하기 위해, 저자들은 "세 세제곱수의 합"이라 불리는 유명한 유형의 퍼즐로 테스트를 진행했습니다. 이 퍼즐들은 "세 정수를 세제곱하여 더했을 때 특정 숫자가 되는 숫자를 찾을 수 있는가?"를 묻습니다.

예를 들어, 퍼즐은 다음과 같을 수 있습니다: $x^3 + y^3 + z^3 = 79$.

이것은 표준 솔버들에게는 악몽과 같습니다. 숫자는 매우 커질 수 있고 관계는 복잡합니다. 저자들은 자신들의 새로운 솔버인 qfn2l을 기존의 최고 성능 솔버들(Z3, cvc5, MathSAT 등)과 비교 테스트했습니다.

• 다른 솔버들은 $x^3 + y^3 + z^3 = 79$ 퍼즐을 풀려고 시도하다가 3분 만에 포기했습니다("타임아웃").
• 새로운 솔버인 qfn2l은 단 20초 만에 정답($x = -19, y = 35, z = -33$)을 찾아냈습니다.

결과: 경쟁력 있는 새로운 도전자

연구진은 SMT-LIB이라는 표준 라이브러리에서 가져온 25,444개의 방대한 퍼즐 모음으로 솔버를 테스트했습니다. 결과는 다음과 같습니다.

1. 전반적인 성능: 새로운 솔버는 현존하는 최고의 도구들과 경쟁할 만한 수준입니다. 총 14,000개의 퍼즐을 해결했으며, 이는 최상위 성능의 도구들과 근접한 수치입니다. 비록 모든 종류의 퍼즐에서 최고 성능(예: Z3)을 압도하지는 못했지만 말입니다.
2. 강점(Sweet Spot): 새로운 솔버는 거듭제곱과 혼합 곱이 지배적인 퍼즐에서 독보적인 기량을 발휘합니다. (세 세제곱수의 합을 포함하는) "MathProblems" 제품군에서 약 **53%**의 인스턴스(1,100개 중 585~587개)를 해결했습니다. 다른 솔버들은 이러한 특정 유형의 문제에서 훨씬 더 큰 어려움을 겪었습니다.
3. 트레이드오프(Trade-off): 저자들은 퍼즐의 서로 다른 부분들이 일관성을 갖는지(이를 "합동 공리(congruence axioms)"라고 함)를 더욱 철저히 확인하는 버전을 테스트했습니다. 그 결과, 이러한 추가적인 검증이 일반적인 퍼즐에서는 오히려 솔버의 속도를 늦추어 전체적으로 약 1,600개의 인스턴스를 덜 해결하게 만든다는 것을 발견했습니다. 이는 대부분의 문제에서 촘촘한 울타리(할선 경계)만으로도 충분하며, 모든 일관성 규칙을 확인하기 위한 과도한 연산은 필요하지 않음을 시사합니다.

이것이 왜 중요한가

이 논문은 해결 불가능한 문제를 해결했다고 주장하는 것이 아닙니다. 저자들은 이 문제가 수학적으로 결정 불가능(undecidable)하기 때문에, 어떤 컴퓨터도 모든 사례를 해결할 수는 없다는 점을 인정합니다. 그러나 그들은 이러한 구불구불한 비선형 규칙들을 어떻게 근사화하느냐에 따라(특히 이 촘촘한 할선 기반의 울타리를 사용함으로써), "충분히 좋은" 탐정들을 훨씬 더 똑똑하게 만들 수 있음을 보여주었습니다.

그들은 오픈 소스이며 기존 엔진(Z3) 위에서 작동하는 도구를 구축함으로써, 더 똑똑한 전략이 가장 어려운 정수 퍼즐 유형에서 무차별 대입 방식(brute-force)보다 우월할 수 있음을 입증했습니다. 소프트웨어가 충돌하지 않을지, 혹은 암호 프로토콜이 안전한지를 검증하려는 모든 이들에게, 이 새로운 방법은 배후의 수학을 더 빠르고 신뢰할 수 있게 확인하는 길을 제시합니다.

요약하자면, 저자들은 복잡하고 구불구불한 문제를 가져와 그 주변에 더 촘촘한 선을 그림으로써, 컴퓨터가 이전보다 훨씬 빠르게 진실을 찾을 수 있도록 만들었습니다.