기울기 크기를 고르게 맞추면 부동소수점 SMT가 빨라질까

오늘 다룰 연구는 Accelerating Floating-Point Satisfiability Solving via Gradient Normalization이며, arXiv에 2610.08808로 공개된 논문입니다. 이 논문은 부동소수점 SMT를 연속 완화 위에서 그래디언트 하강으로 풀 때 일부 어려운 clause가 전체 최적화 궤적을 장악하는 gradient domination 현상을 진단하고, 각 clause를 멀티태스크 학습의 task처럼 취급해 GradNorm으로 기울기 크기를 실행 중에 맞추는 GradSAT와 연속 탐색 뒤에 비트 정밀 로컬 탐색을 잇는 2단계 파이프라인을 제안합니다. 원문 링크는 제목 아래에 걸어 두었습니다.

왜 저는 이 논문을 끝까지 읽었을까

안녕하세요, 패트릭입니다. 저는 SMT 솔버 논문을 볼 때 보통 벤치마크 표부터 넘겨보는 편인데요, 이번에는 도입부의 진단 문장에서 멈췄습니다. 어려운 clause 몇 개가 최적화 궤적을 통째로 끌고 간다는 표현 때문이었습니다. 생각해보면 최적화 기반 솔버가 흔들릴 때 우리는 흔히 학습률이나 초기화, 혹은 완화 함수를 탓합니다. 그런데 저자들은 원인을 다른 곳에서 찾았고, 그 선택이 저에게는 낯설면서도 설득력 있게 다가왔습니다.

제가 이 논문에서 가장 눈길이 간 부분은 문제를 푸는 기술보다 문제를 부르는 방식이었습니다. 논리식 하나를 통째로 풀어야 할 대상으로 보지 않고, clause들의 모임으로 본 뒤 각 clause에 따로 기울기를 물어보는 태도 말이죠. 여러 사람이 함께 일하다 보면 목소리 큰 두어 명이 회의 전체를 끌고 갈 때가 있습니다. 그렇다면 수백 개 clause가 함께 최적화될 때도 비슷한 일이 생길까요. 이 논문은 그 질문에 꽤 직접적으로 답합니다.

여기서는 조금 조심해서 읽을 필요가 있습니다. 이 글은 새로운 솔버의 구조와 직관을 해설하는 글이고, 제가 저자들의 실험 환경을 직접 돌려본 것은 아닙니다. 그래서 숫자 자랑보다는 왜 이런 설계가 나왔는지, 어떤 지점에서 엔지니어의 고민과 맞닿는지를 따라가 보려 합니다. 저희가 새로운 AI 아키텍처를 볼 때도 benchmark 숫자만 보지는 않습니다. 실제로 무엇이 바뀌었고, 그 변화가 시스템에서 어떤 비용 구조를 만드는지를 함께 봅니다.

부동소수점 검증은 왜 유독 까다로울까

부동소수점 위의 SMT, 그중에서도 Quantifier-Free Floating-Point라 불리는 영역은 소프트웨어 검증이나 프로그램 분석, 그리고 컴파일러 테스트처럼 정확한 추론이 필요한 작업들과 맞닿아 있습니다. 밤사이 공시가 늦게 도착하거나 아침에 특정 종목이 거래 정지에 걸려도 예측 라인은 멈추면 안 되는 것처럼, 검증 파이프라인에서도 솔버 하나가 멈추면 뒤따르는 분석 전체가 기다리게 되는데요. 그래서 이 영역의 속도 문제는 연구실 점수 이상의 체감을 갖습니다.

그런데 부동소수점은 실수와 닮은 듯 다릅니다. 반올림이 끼어들고, 오버플로우와 언더플로우, NaN 같은 예외 값이 있으며, 같은 수식도 연산 순서에 따라 비트 단위 결과가 달라질 수 있습니다. 연속 함수처럼 미분하면서도, 막상 답을 낼 때는 비트 하나까지 정확해야 하는 이중성이 있죠. 이 간극 때문에 전통적인 기호 추론은 정확하지만 때로 느리고, 연속 최적화는 빠르지만 마지막 비트에서 미끄러지기 쉽습니다. 그렇다면 두 세계의 장점을 잇는 다리를 놓을 수 있을까요. GradSAT는 그 다리를 2단계 파이프라인으로 놓겠다고 합니다.

저는 이 지점에서 논문의 문제 설정이 과장 없이 읽혔습니다. 부동소수점을 어렵게 만드는 요인을 나열하며 겁을 주기보다, 연속 완화로 풀 때 생기는 특정 실패 모드에 초점을 맞추기 때문입니다. 진단은 좁을수록 손댈 곳이 분명해지죠.

논리를 미분 가능한 곡면 위에 올린다는 발상

최적화 기반 SMT 솔버의 출발점은 논리식을 연속적인 손실 곡면으로 바꾸는 일입니다. clause가 얼마나 어겨졌는지를 재는 부드러운 페널티를 만들고, 그 페널티들을 합쳐 전체 위반량을 정의한 뒤, 변수 값을 조금씩 움직이며 위반량을 줄여 나가는 것이죠. 만족할 만한 할당을 찾는 과정이 곧 경사를 따라 내려가는 과정이 됩니다. 일종의 등산 지도를 펼치고, 가장 가파른 내리막을 따라 내려가며 계곡 바닥을 찾는 셈입니다.

이 발상이 매력적인 이유는 병렬 하드웨어와 잘 어울리기 때문입니다. 수많은 변수에 대한 기울기를 한 번에 계산할 수 있고, GPU 위에서 벡터 연산으로 밀어붙일 수 있으니까요. 예전에는 경우를 나누고 가지치기를 하며 하나씩 따져야 했던 탐색이, 여기서는 미분 가능한 공간에서의 움직임으로 바뀝니다. 물론 완화는 근사이고, 근사는 거짓말을 조금 섞습니다. 원래 논리식에서는 참과 거짓만 있었는데, 완화된 세계에서는 거의 참 같은 중간 상태가 생기기 때문입니다. 그런데도 이 접근이 힘을 받는 이유는, 좋은 분지(basin) 근처까지는 빠르게 데려다줄 수 있기 때문입니다. 문제는 그 다음입니다. 분지 근처까지는 잘 가는데, 정작 마지막에 비트 단위 정답으로 착지하지 못하는 경우가 생깁니다.

저는 여기서 멈칫했습니다. 완화 자체는 오래된 아이디어인데, 왜 지금 다시 꺼냈을까 싶었기 때문입니다. 답은 뒤에 나오는 진단과 실행 환경에 있었습니다. 완화의 오래된 약점을 그대로 두지 않고, 기울기 균형과 2단계 마무리라는 장치를 덧붙였기 때문입니다.

일부 clause가 전체 궤적을 끌고 가는 순간

논문이 지목하는 실패 모드는 gradient domination입니다. 수백 개 clause 중에서 유독 어려운 몇 개가 내는 기울기가 너무 커서, 전체 업데이트 방향을 자기들 쪽으로 끌어당기는 현상 말이죠. 회의실에서 목소리 큰 두 사람이 의제를 독점하면 나머지 안건은 뒤로 밀리는 것과 비슷합니다. (물론 회의와 달리 여기서는 목소리 크기가 수학적으로 측정됩니다. 기울기 노름이죠.)

이 현상이 생기면 솔버는 넓은 식을 고르게 만족시키는 대신, 어려운 clause 몇 개를 달래는 데 대부분의 걸음을 씁니다. 전체 위반량은 줄어드는 듯 보이지만, 실상은 한쪽 구석에서 맴도는 것에 가깝습니다. 그래서 지역 최소값에 갇혔다는 표현이 나옵니다. 모든 clause가 조금씩 만족되어야 참이 되는 논리식의 특성상, 일부만 과하게 신경 쓰는 궤적은 끝까지 가도 답에 닿지 못합니다.

그렇다면 왜 하필 부동소수점에서 이 문제가 두드러질까요. 제 해석은 이렇습니다. 부동소수점 연산은 스케일이 들쭉날쭉하고, 완화 함수의 기울기도 연산 종류와 값 범위에 따라 크게 요동칠 수 있습니다. 어떤 clause는 지수 연산이나 경계 근처 비교 때문에 기울기가 폭발하고, 다른 clause는 평탄한 구간에 걸려 거의 속삭이듯 신호를 냅니다. 이렇게 되면 옵티마이저는 큰 소리 나는 쪽만 따라가게 되죠. 학습률을 낮추면 폭발은 가라앉지만 전체 탐색이 기어다니게 되고, 학습률을 높이면 어려운 clause가 궤적을 통째로 흔듭니다. 어느 쪽도 답이 아닙니다. 그래서 저자들은 학습률 하나를 만지는 대신, clause 사이의 크기 균형 자체를 문제 삼았습니다.

clause 하나를 task 하나로 본다는 전환

여기서 논문의 시선이 바뀝니다. 논리식 전체를 하나의 손실로 보지 않고, clause마다 독립된 task가 있는 멀티태스크 학습으로 다시 쓴 것입니다. 멀티태스크 학습에서는 여러 task를 함께 배우다가 특정 task의 기울기가 다른 task를 압도하면 전체 모델이 한쪽으로 기웁니다. 그래서 task 사이 기울기 크기를 맞추는 기법들이 오래 연구되어 왔죠. 저자들은 SMT의 clause들도 같은 처지에 놓여 있다고 보았습니다.

이 전환이 저에게는 꽤 신선했습니다. 논리와 학습은 보통 다른 세계의 언어를 쓰는데, 여기서는 clause 만족을 task 손실처럼 다루면서 학습 쪽의 도구를 그대로 가져오기 때문입니다. 문제를 처음부터 새로 풀기보다, 문제를 이미 답이 있는 동네로 이사시킨 셈이죠. 이사를 잘하면 기존 가구를 그대로 쓸 수 있습니다. GradNorm이라는 가구가 바로 그 경우에 해당합니다.

다만 여기서 오해하지 말아야 할 점이 있습니다. clause를 task처럼 본다고 해서 논리식의 의미가 바뀌는 것은 아닙니다. 원래 식이 요구하는 것은 여전히 모든 clause의 연언이고, 완화된 손실의 합도 그대로 유지됩니다. 달라지는 것은 각 clause가 내는 신호를 어떻게 취급할지, 그 가중치를 실행 중에 어떻게 조절할지뿐입니다. 의미는 그대로 두고, 최적화의 예절만 바꾸는 것이죠. 저는 이런 종류의 개입을 좋아합니다. 문제 정의를 뒤흔들지 않으면서 궤적의 품질을 바꾸기 때문입니다.

기울기 크기를 실행 중에 맞추는 장치

GradNorm의 역할은 이름 그대로 기울기의 크기를 맞추는 일입니다. 각 clause에서 오는 기울기 벡터의 노름을 재고, 지나치게 큰 신호는 누르고, 너무 작은 신호는 살려서, 모든 clause가 비슷한 음량으로 이야기하도록 조절합니다. 오케스트라 조율에 비유하면, 금관 몇 개가 너무 크게 울릴 때 지휘자가 손을 낮추라고 신호하는 장면과 비슷합니다. 곡 자체를 바꾸지 않고 밸런스만 맞추는 것이죠.

눈여겨볼 대목은 이 조절이 실행 중에 일어난다는 점입니다. 미리 정해둔 가중치로 clause별 비중을 고정하는 방식과 달리, 최적화가 진행되면서 기울기 크기가 계속 바뀌므로 균형도 매 스텝마다 다시 잡아야 합니다. 초반에는 경계 조건 clause가 크게 울다가, 중반에는 산술 연산 clause가 치고 나오고, 후반에는 또 다른 clause가 남는 식으로 양상이 바뀌기 때문입니다. 고정된 가중치는 이런 흐름을 따라가지 못합니다. 그래서 동적이라는 수식어가 붙습니다. 매 순간 누가 소리를 키우는지 듣고, 그때그때 믹싱 보드를 만지는 것이죠.

실제 시스템 관점에서 보면 다음 질문이 바로 생깁니다. 기울기 노름을 매번 재고 가중치를 조정하는 비용이 들 텐데, 그 오버헤드를 감당할 만할까요. 논문이 GPU 가속 PyTorch 백엔드를 전면에 내세우는 이유도 여기와 연결됩니다. 균형을 맞추는 연산 자체가 벡터화되고 융합되면, 매 스텝 조절이라는 부담이 감당 가능한 수준으로 내려가기 때문입니다. 균형 장치와 실행 장치는 따로 떨어진 부품이 따로 놀지 않고, 서로를 정당화하는 관계에 있습니다.

연속 탐색 뒤에 정밀 탐색을 잇는 이유

GradSAT의 파이프라인은 2단계로 짜여 있습니다. 먼저 완화된 연속 공간에서 좋은 분지까지 내려가고, 그 후보 할당을 비트 정밀 로컬 탐색 엔진에 넘겨 정확한 할당으로 매듭짓는 구조입니다. 앞 단계가 넓은 지도 위에서 계곡을 찾는다면, 뒷 단계는 계곡 바닥에서 비트 단위로 발을 디디며 정확한 자리를 찍는 일에 가깝습니다.

이 분업이 설득력 있는 이유는 각 단계의 잘하는 일이 다르기 때문입니다. 연속 탐색은 미분 신호를 이용해 넓은 공간을 빠르게 훑는 데 능합니다. 반면 비트 수준의 반올림 경계나 예외 값 처리처럼 날카로운 조건은 연속 신호만으로 다루기 어렵습니다. 반대로 로컬 탐색은 정확한 규칙을 따지지만, 시작점이 나쁘면 주변을 맴돌다가 시간을 쓰게 됩니다. 좋은 출발점을 받으면 이야기가 달라지죠. 앞 단계가 건네준 후보가 이미 좋은 분지 안에 들어와 있다면, 뒷 단계는 짧은 거리만 이동하고도 정확한 답에 닿을 수 있습니다.

저는 이 숫자보다 그 뒤의 구조가 더 오래 남는다고 봅니다. 2단계라는 말 자체는 흔하지만, 어디서 끊고 어디서 잇는지가 설계의 실력을 드러내기 때문입니다. 연속 탐색이 비트 정확성을 흉내 내려 애쓰기보다, 잘하는 만큼만 하고 넘기는 선택이 오히려 전체 시간을 줄일 수 있습니다. 짧은 다리를 두 개 놓는 편이 긴 다리 하나를 무리해 놓는 것보다 단단할 때가 있죠.

GPU 백엔드와 컴파일, 퓨전이 하는 일

논문은 GPU 가속 PyTorch 백엔드와 함께 symbolic compilation과 operator fusion을 언급합니다. 처음 들으면 장식처럼 들릴 수 있는데요, 실제로는 앞선 설계와 직접 맞물리는 부분입니다. clause마다 기울기를 재고 가중치를 조절하는 과정은 연산 횟수가 많아질 수밖에 없고, 이를 순진하게 구현하면 커널 호출과 메모리 왕복이 쌓여 속도가 깎입니다. 컴파일과 퓨전은 이런 잘게 쪼개진 연산을 묶어 한 번에 처리하도록 돕습니다.

구체적으로 그려보면 이렇습니다. 논리식에서 유도된 완화 연산들을 기호 단위로 묶어 계산 그래프로 올리고, 중간 텐서를 메모리에 썼다 읽는 과정을 줄이며, 커널 런칭 오버헤드를 여러 연산에 나눠 담는 것이죠. 특히 수백 개 clause에 대한 기울기 노름 계산과 가중치 적용은 서로 닮은 연산의 반복이라 묶기 좋습니다. 묶을수록 GPU의 병렬 자원을 채우기 쉬워지고, 메모리 대역폭에 걸리는 시간도 줄어듭니다. 균형을 맞추는 일이 공짜는 아니지만, 실행 방식을 바꾸면 값을 치를 만해진다는 계산이 깔려 있습니다.

여기서는 조금 조심해서 읽을 필요가 있습니다. GPU 가속이라는 말이 모든 SMT 문제에 같은 속도를 보장하는 것은 아닙니다. 식의 구조가 벡터화에 잘 맞을 때와 그렇지 않을 때의 편차가 있고, 컴파일 자체에도 비용이 듭니다. 그럼에도 이 논문의 방향은 분명합니다. 기울기 균형이라는 알고리즘적 선택을, 하드웨어 친화적인 실행과 함께 가져가겠다는 것이죠. 알고리즘과 시스템이 같은 방향을 바라볼 때 전체 파이프라인이 버거워지지 않습니다.

이 설계를 오해하기 쉬운 지점들

표면적으로 보면 단순합니다. 기울기 크기를 맞추고 GPU로 밀면 빨라진다는 이야기처럼 들리기 때문입니다. 실제로는 그렇지 않습니다. 몇 가지 오해를 미리 걷어내는 편이 논의를 정확하게 만듭니다.

먼저 GradNorm이 어려운 clause를 무시하는 장치는 아닙니다. 오히려 반대에 가깝습니다. 어려운 clause의 과도한 신호가 전체를 삼키지 못하게 하면서도, 그 clause 자체의 신호까지 지워버리지는 않기 때문입니다. 음량을 맞춘다고 연주자를 무대에서 내보내는 것은 아니죠. 목표는 모든 clause가 들리는 상태에서 함께 내려가는 궤적입니다.

다음으로 2단계 파이프라인을 연속 탐색이 실패해서 뒷수습을 한다는 뜻으로 읽으면 곤란합니다. 앞 단계의 역할은 처음부터 정확한 비트 할당을 내는 데 있지 않고, 좋은 분지를 찾는 데 있습니다. 요구사항을 다르게 잡은 것이지, 못한 것을 감추는 구조가 아닙니다. 마라톤에서 페이스메이커가 중반까지 끌고 간 뒤 바통을 넘기는 것과 비슷합니다. (물론 여기서는 바통이 부동소수점 비트 패턴이라는 점이 다르지만요.)

마지막으로 멀티태스크 비유가 논리식의 의미를 흐리게 만든다고 걱정할 필요는 없습니다. task라는 말을 빌려왔을 뿐, 검증이 요구하는 엄밀성은 뒷 단계의 비트 정밀 탐색이 지킵니다. 완화된 앞 단계가 답의 후보를 좁히고, 엄밀한 뒷 단계가 참과 거짓을 가르는 식으로 역할이 나뉘어 있습니다. 저는 그래서 이 구조를 완화의 타협이라기보다 완화의 분업이라고 읽었습니다.

제가 앞으로 보고 싶은 것들

그렇다면 이 흐름은 어디에서 더 단단해질 수 있을까요. 그 이야기는 논문이 닫힌 뒤에도 이어집니다. 제가 앞으로 보고 싶은 것은 크게 두 가지입니다.

하나는 기울기 균형의 적응 범위에 대한 이해입니다. GradNorm이 크기 불균형을 다룬다면, 방향 충돌은 어떻게 될까요. 두 clause가 서로 반대 방향을 가리킬 때 크기만 맞춘다고 궤적이 안정될까요. 멀티태스크 학습 쪽에서는 크기와 방향을 함께 다루는 논의가 이어져 왔는데요, SMT의 clause 구조에서도 방향 충돌이 실제로 얼마나 자주 일어나는지, 그리고 그때 궤적이 어떤 모양으로 꼬이는지 궁금합니다. 크기 다음의 질문은 방향이 될 수밖에 없기 때문입니다.

다른 하나는 2단계 사이 인계 품질에 대한 이야기입니다. 연속 탐색이 건네는 후보의 품질이 뒷 단계 시간에 얼마나 직접 연결되는지, 후보가 분지 바깥에 떨어졌을 때 파이프라인이 어떻게 회복하는지가 궁금합니다. 실제 검증 파이프라인에서는 한두 문제의 실패보다 전체 처리량의 꼬리가 뒷맛을 결정하는데요, 앞 단계와 뒷 단계 사이의 주고받기가 매끄럽지 않으면 평균은 빨라 보여도 꼬리가 길어질 수 있습니다. 운영 측면에서 보면 이 차이는 상당히 큽니다. 검증 라인은 가장 어려운 문제 앞에서도 멈추지 않아야 하기 때문입니다.

그렇다면 사람의 역할은 무엇일까요. 저는 솔버를 고르는 일보다 솔버가 실패하는 방식을 읽는 일에 갈수록 무게가 실리고 있다고 봅니다. gradient domination 같은 진단은 벤치마크 숫자 하나로 환원되지 않지만, 시스템을 설계하는 사람에게는 숫자를 해석하는 눈을 줍니다. 다음에 비슷한 궤적 이탈을 마주했을 때, 학습률을 돌리기 전에 clause 사이의 음량부터 확인해 보는 습관 말이죠. 그 습관 하나를 남긴다면, 이 논문은 이미 읽을 값을 했다고 생각합니다.