말로 풀리지 않는 부등식을 증명하는 법

IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation은 arXiv에 2610.20681 번호로 공개된 연구로, 언어 모델의 추론과 기호 계산을 함께 엮어 Lean4에서 부등식을 증명하는 에이전트 방식을 제안합니다. 이 방법이 하는 일은 한 문장으로 정리할 수 있는데, 어려운 부등식을 보조정리와 변형된 목표로 나누고 알맞은 계산 엔진을 골라 만든 정확한 증명서를 Lean이 받아들이는 코드로 조립한다는 것입니다. 이 글에서는 그 분업이 왜 필요했는지부터 탐색과 계산과 검증의 연결까지 순서대로 따라가 보겠는데, 원문 논문으로 이어지는 연결은 제목 아래에 걸려 있습니다.

증명은 맞았는데 왜 Lean은 고개를 저을까

안녕하세요, 패트릭입니다.

수학 문제를 풀 때 사람에게는 설득이 통합니다. 칠판 앞에서 흐름을 설명하면 듣는 쪽에서 빈틈을 메워주기도 하고, 계산이 조금 거칠어도 방향이 맞으면 고개를 끄덕여 주거든요. 그런데 Lean 앞에 서면 분위기가 달라집니다. 그렇다면 왜 같은 설명이 사람 앞에서는 통하고 기계 앞에서는 막힐까요?

제가 이 논문에서 가장 먼저 눈이 간 부분은 바로 그 간극을 정면으로 다룬다는 점입니다. 언어 모델은 부등식의 흐름을 말로 풀어내는 데에는 꽤 능숙합니다. 어디를 묶고 어디를 풀어야 할지 감을 잡고, 전에 본 적 있는 형태로 변형하는 일도 잘합니다. 그런데 Lean4는 감으로 넘어가지 않습니다. 모든 단계가 규칙에 맞아야 하고, 계산의 끝자락까지 정확해야 받아주죠. 그래서 말로는 옳아 보이는 증명이 형식 검증 앞에서 자주 무너집니다. 계산 한 줄이 어긋나거나, 자명해 보이는 부등식 하나가 규칙으로 뒷받침되지 않으면 그 자리에서 멈추니까요.

이런 장면을 저는 오답 노트와 닮았다고 느꼈습니다. 학생이 풀이의 방향은 맞았는데 계산에서 틀려 점수를 잃는 경우와 비슷하기 때문입니다. 방향을 잡는 일과 끝까지 계산하는 일은 서로 다른 근육을 쓰는데, 언어 모델은 전자에는 강하고 후자에는 자주 흔들립니다. 그렇다면 두 근육을 한 몸에 넣으려 애쓰기보다, 잘하는 쪽은 살리고 약한 쪽은 다른 도구에 맡기면 어떨까요? 이 질문이 바로 IneqAgent의 출발점처럼 읽혔습니다.

부등식은 왜 말로만 풀리지 않을까

부등식 증명을 조금 들여다보면, 이 문제가 왜 유난히 까다로운지 감이 옵니다. 등식은 변형을 해도 형태가 비교적 또렷하게 남는데, 부등식은 크기를 비교하는 일이라 어림이 들어가기 시작하면 어디서 새는지가 잘 안 보이거든요. 그래서 증명자는 중간에 작은 다리를 여러 개 놓아야 합니다. 이 식이 저 식보다 크다는 보조정리 하나, 저 다리를 건너면 목표가 더 쉬워진다는 변형 하나, 이런 식으로요.

그런데 언어 모델에게 이 과정을 통째로 맡기면 특유의 문제가 생깁니다. 흐름은 매끄럽게 이어가는데, 정작 크기를 가르는 계산에서 미끄러지는 것이죠. 제곱합으로 쓸 수 있는지, 계수가 양수 쪽으로 몰리는지, 치환을 반복하면 차수가 떨어지는지 같은 판단은 손으로 셈해봐야 아는 것들이라 말의 유창함만으로는 버티기 어렵습니다. 그리고 Lean은 그 미끄러짐을 그냥 넘기지 않습니다. 사람이면 넘어갈 만한 어림도 규칙 위반으로 찍어내죠.

여기서 재미있는 질문이 생깁니다. 모델이 틀리는 지점이 매번 비슷하다면, 그 지점만 따로 떼어낼 수 있지 않을까요? 실제로 증명에서 막히는 곳은 대부분 계산이 몰린 목입니다. 방향을 고르는 일은 모델이 하고, 크기를 확정하는 일은 셈에 강한 엔진이 하면 서로의 약점을 가릴 수 있습니다. 저는 이 구분이 마음에 들었습니다. 모든 걸 한 모델이 잘하게 만들려는 욕심을 버리고, 막히는 목을 정확히 지목했기 때문입니다.

생각하는 일과 계산하는 일을 나누면 뭐가 달라질까

IneqAgent의 그림을 한마디로 그리면 분업입니다. 언어 모델은 전체를 조망하면서 무엇을 증명할지 정하고, 기호 계산 백엔드는 맡은 조각을 정확한 증명서로 바꿔줍니다. 그리고 Lean이 그 결과를 받아들이는지 확인하면서 다음 수를 정하죠. 이렇게 말하면 단순해 보이지만, 실제로는 그렇지 않습니다. 분업이 돌아가려면 누가 언제 무엇을 맡을지 정하는 지휘자가 필요하기 때문입니다.

이 연구가 그 자리에 둔 것이 보조정리 단위의 몬테카를로 트리 탐색입니다. 탐색이라는 말을 들으면 바둑이 떠오르실 텐데, 느낌이 비슷합니다. 지금 목표에서 갈 수 있는 다음 수로 보조정리 만들기, 목표 다시 쓰기, 계산 엔진 고르기를 펼쳐두고, 유망해 보이는 가지를 따라가 보는 것이죠. 한 번에 정답을 맞히려 하지 않고, 여러 갈래를 조금씩 두들겨 보면서 길이 열리는 쪽에 시간을 더 쓰는 방식입니다. 그래서 실패한 시도가 헛수고로 끝나지 않고, 어디가 막혔는지를 알려주는 정보로 남습니다.

저는 여기서 멈칫했습니다. 탐색을 쓴다고 하면 보통 토큰을 많이 쓰는 무식한 방법부터 떠올리기 때문입니다. 그런데 이 설계는 탐색을 계산 엔진과 붙여서 씁니다. 말이 되는 조각만 계산기에 넘기고, 계산기가 뱉은 정확한 결과를 다시 탐색의 발판으로 삼으니까요. 탐색이 막연한 헤매임이 아니라 계산으로 확인되는 발걸음이 되는 셈입니다. 밤늦게 증명을 붙잡고 씨름해본 분이라면 이 감각을 아실 겁니다. 혼자 끙끙대기보다, 셈이 빠른 친구를 옆에 두고 번갈아 가며 푸는 편이 훨씬 빨리 풀리니까요.

자동 증명기라고 부르면 오해가 생기는 이유

이름만 보면 IneqAgent를 버튼 하나 누르면 증명이 나오는 기계로 오해하기 쉽습니다. 그런데 논문을 조금 더 들여다보면 진짜로 중요한 부분은 자동이라는 말이 아니라 에이전트라는 말에 있습니다. 정해진 순서대로 도구를 돌리는 파이프라인이 아니라, 상황에 따라 다음 행동을 고르는 주체에 가깝기 때문입니다.

파이프라인과 에이전트의 차이는 실패 앞에서 드러납니다. 파이프라인은 정해진 단계 중 하나라도 어긋나면 그대로 멈춥니다. 반면 이 시스템은 보조정리가 틀리면 버리고 다른 보조정리를 만들고, 목표 변형이 어색하면 다른 변형을 시도하고, 고른 엔진이 막히면 다른 엔진을 불러옵니다. Lean이 뱉은 오류 메시지도 다음 수를 고르는 단서로 씁니다. 저는 이 대목에서 일하는 방식이 사람과 닮았다고 느꼈습니다. 증명을 잘하는 사람은 처음 계획이 틀리면 계획을 고치지, 같은 계산을 반복하지 않으니까요.

그래서 이 시스템을 평가할 때도 정답률만 보면 반만 본 셈입니다. 물론 숫자는 뒤에서 다룹니다. 다만 그 전에 봐야 할 것은 실패를 다루는 태도입니다. 보조정리를 만들고, 목표를 고치고, 엔진을 고르는 세 가지 행동이 서로 맞물리면서 막힌 길을 돌아가게 만들었는지가 먼저입니다. 정답률은 그 맞물림이 돌아간 결과로 따라오는 것이죠. 저희가 새로운 AI 구조를 볼 때도 숫자만 보지는 않습니다. 실제로 무엇이 바뀌었고, 그 변화가 다음 실패를 다루는 방식을 어떻게 바꾸는지를 함께 보는데, 이 연구는 그 기준에서 읽을 거리가 많은 편입니다.

보조정리를 바둑돌처럼 두는 탐색은 어떻게 돌아갈까

이제 탐색의 내부를 조금 더 구체적으로 따라가 보겠습니다. 출발점은 원래 부등식입니다. 에이전트는 여기서 바로 정면 돌파를 시도하지 않습니다. 대신 작은 명제를 하나 제안합니다. 이 보조정리가 참이면 원래 목표가 쉬워진다는 식의 다리죠. 이어서 원래 목표를 보조정리에 맞게 다시 씁니다. 목표를 나누거나, 대칭성을 이용해 경우를 줄이거나, 치환으로 형태를 고르는 식의 손질이 여기에 들어갑니다. 그리고 손질된 조각을 어떤 계산 엔진에 맡길지 고릅니다.

이 세 가지 선택이 트리의 한 수가 됩니다. 탐색은 이런 수를 여러 갈래로 펼쳐두고, 각 갈래가 얼마나 유망한지 조금씩 시험해봅니다. 계산 엔진이 정확한 증명서를 내주면 그 가지는 점수를 얻고, Lean이 중간 단계를 받아주면 또 점수를 얻는 식입니다. 점수가 쌓인 가지는 더 깊이 파고들고, 막힌 가지는 일찍 접습니다. 언뜻 보면 돌아가는 길처럼 보이지만, 부등식에서는 돌아가는 길이 종종 지름길입니다. 정면에서는 안 풀리는 식도 보조정리 하나만 잘 놓으면 계산기가 알아서 마무리해주기 때문입니다.

여기서 드는 practical한 질문이 있습니다. 좋은 보조정리는 어떻게 알아볼까요? 연구가 택한 답은 머릿속 상상이 아니라 바깥의 반응입니다. 계산기가 증명서를 내줬는지, Lean이 고개를 끄덕였는지를 보고 판단하는 것이죠. 저는 이 태도가 운영 관점에서 마음에 들었습니다. 모델의 자신감 점수만 믿고 밀어붙이면 헛된 가지에 시간을 쏟기 쉬운데, 바깥에서 확인되는 신호로 가지치기를 하면 허탕이 줄기 때문입니다. (참고로 이런 바깥 신호를 쓰는 탐색은 정답을 미리 아는 게 아니라, 검증기가 주는 반응을 다음 수의 재료로 쓰는 것에 가깝습니다.)

계산기 세 개를 나란히 둔 이유가 있다

탐색이 길을 고르는 일이라면, 계산 엔진은 그 길 끝에서 도장을 찍는 일입니다. 이 연구는 그 도장으로 제곱합과 Bernstein 방법과 연속 차분 치환이라는 세 가지를 나란히 둡니다. 이름이 낯설 수 있는데, 각각의 감각은 일상과 멀지 않습니다.

제곱합은 식을 제곱들의 합으로 풀어내는 방식입니다. 제곱은 음수가 되지 않으니, 합으로 쓸 수만 있다면 그 식이 0보다 작지 않다는 게 바로 확정되죠. 마치 여러 개의 작은 저울을 나란히 두고 전부 양수 쪽으로 기울었다고 보여주는 셈입니다. Bernstein 방법은 구간 안에서 다항식이 어떻게 움직이는지를 계수로 가둬서 판단합니다. 울타리를 쳐두고 그 안에서만 움직이게 만든 뒤, 울타리의 위치를 보고 부등식을 확정하는 것이죠. 연속 차분 치환은 변수를 차분 형태로 바꿔가며 식을 점점 다루기 쉬운 꼴로 몰아가는 방법입니다. 엉킨 실타래를 한 가닥씩 풀어서 매듭을 푸는 모습과 비슷합니다.

그런데 왜 하필 세 개일까요? 이유를 생각해보면 생각보다 분명합니다. 어떤 부등식은 제곱합으로 잘 풀리고, 어떤 부등식은 구간을 가두는 쪽이 편하고, 어떤 부등식은 치환을 반복해야 열리기 때문입니다. 하나만 들고 가면 잘 맞는 문제에서는 빠르겠지만, 어긋나는 문제에서는 영영 막힙니다. 세 개를 나란히 두면 각자 잘하는 모양이 달라서 서로의 빈틈을 메워줍니다. 저는 이 선택에서 욕심보다 정직함을 읽었습니다. 만능 엔진 하나를 내세우는 대신, 모양이 다른 도구들을 모아두고 상황에 맞게 고르겠다는 선언이니까요.

여기서 놓치기 쉬운 대목이 하나 더 있습니다. 이 엔진들은 단순히 참과 거짓만 알려주지 않습니다. Lean이 받아들일 수 있는 정확한 증명서를 함께 만들어줍니다. 계산 결과가 맞다는 말만 던져주고 끝나면 Lean 쪽에서 다시 막히는데, 이 시스템은 Lean 안에서 재현 가능한 형태로 결과를 포장해서 넘기죠. 그래서 계산과 검증 사이의 틈이 줄어듭니다.

계산 결과가 Lean 코드가 되기까지 무슨 일이 생길까

계산기가 증명서를 내줬다고 증명이 끝난 것은 아닙니다. 그 종이를 Lean이 읽을 수 있는 문장으로 옮겨 적어야 하죠. 이 옮겨 적기가 생각보다 까다롭습니다. 기호 엔진의 세계와 Lean의 세계는 쓰는 문법이 다르고, 생략을 허용하는 범위도 다르거든요. 사람이 증명을 옮겨 적을 때도 여기서 자주 미끄러집니다. 계산은 맞았는데 Lean 문법에 맞게 쓰는 과정에서 오류가 나는 경우 말이죠.

IneqAgent는 이 구간을 언어 모델이 메우게 합니다. 엔진이 만든 증명서를 받아서 Lean의 전술과 단계로 풀어내고, Lean에 직접 돌려보면서 고쳐나갑니다. Lean이 오류를 뱉으면 그 메시지를 읽고 코드를 손봅니다. 닫히지 않은 목표가 남으면 보조정리를 보태거나 목표 변형을 다시 시도합니다. 그리고 마지막에는 원래 정리 문장에 그대로 맞춰 전체 증명을 확인합니다. 이 마지막 확인이 은근히 중요합니다. 중간 조각이 각각 맞았어도 원래 문제와 어긋나면 소용이 없기 때문입니다.

실제 시스템 관점에서 보면 다음 질문이 바로 생깁니다. 이렇게 쓰고 돌리고 고치는 반복이 비용이 많이 들지 않을까요? 답은 뒤에서 숫자와 함께 다룹니다. 다만 구조만 놓고 보면 이 반복은 헛도는 반복이 아닙니다. 매번 Lean이라는 엄격한 심판의 판정을 받으면서 좁혀가기 때문에, 시행착오가 다음 시도의 정확도를 올리거든요. 저는 그래서 이 부분을 읽으면서 증명을 쓰는 행위가 아니라 증명을 기르는 과정에 가깝다고 느꼈습니다. 한 번에 완성하는 대신, 검증의 반응을 먹이 삼아 조금씩 자라게 하는 것이죠.

186문제 중 175문제라는 숫자를 어떻게 읽어야 할까

이제 숫자를 볼 차례입니다. 논문이 보고한 장면에서 IneqAgent는 DeepSeek-V4-Flash를 등에 업고 네 가지 벤치마크에 걸쳐 186문제 중 175문제를 풀었다고 합니다. 비율로 쓰면 94.09퍼센트죠. 처음 이 숫자를 보면 꽤 시원하게 느껴집니다. 부등식이라는 까다로운 영역에서, 그것도 Lean처럼 엄격한 검증 아래에서 이런 적중률이 나왔다는 건 분명히 눈에 띄니까요.

하지만 저는 이 숫자보다 그 뒤의 구조가 더 중요하다고 봅니다. 같은 뼈대 모델을 쓰는 직접 시도와 견줄 때, IneqAgent는 언어 모델 호출 비용이 낮은 구간에서 더 높은 성공률을 보였다고 하기 때문입니다. 네 가지 뼈대 모델에서 비슷한 그림이 나왔다는 대목도 함께 읽어야 합니다. 이 말은 단순히 큰 모델을 오래 돌려서 푼 게 아니라, 적은 시도 안에 풀리는 문제의 밀도가 달라졌다는 뜻이거든요. 탐색과 계산 분업이 헛걸음을 줄였다는 해석과 잘 맞물립니다.

여기서는 조금 조심해서 읽을 필요가 있습니다. 겉으로 보이는 적중률이 높다고 해서 모든 부등식이 쉬워졌다는 뜻은 아닙니다. 벤치마크 186문제라는 울타리 안에서 나온 결과이고, 울타리 밖에 있는 더 어렵거나 더 지저분한 문제에서는 그림이 달라질 수 있기 때문입니다. 또한 직접 시도와의 비교는 같은 뼈대를 썼다는 조건 아래에서 의미를 가지는데, 뼈대가 바뀌면 비용과 성공률의 위치도 함께 움직입니다. 그럼에도 불구하고 낮은 비용 구간에서의 우위는 가볍게 넘길 일이 아닙니다. 실제 운영에서는 무제한으로 시도할 수 없고, 적은 호출로 얼마나 건지는지가 체감 효율을 가르니까요. 밤사이 배치를 돌려 증명을 모으는 상황을 떠올리면, 같은 예산으로 더 많은 정리를 닫는 구조가 얼마나 실용적인지 바로 감이 옵니다.

묵은 추측을 건드렸다는 말의 무게

벤치마크 숫자 바깥에서 제가 오래 머문 대목은 따로 있습니다. 이 연구가 Dittert 추측의 강화된 형태를 4차원과 5차원에서 Lean으로 검증했다는 보고, 그리고 Holens-Djokovic의 (4, 4) 부등식을 인증하면서 4차원에서의 Merris 추측으로 이어졌다는 대목입니다. 이런 문장은 처음 보면 그저 실적 한 줄처럼 보입니다. 그런데 수학에서의 무게는 적중률과 다릅니다. 묵은 추측을 건드렸다는 건 남이 세워둔 문제를 푸는 일을 넘어, 그 분야의 지도에 선을 하나 긋는 일에 가깝기 때문입니다.

생각해보면 사람도 비슷하게 배웁니다. 교과서 문제를 빨리 푸는 실력과, 오래 열린 문제를 조금이라도 앞으로 미는 실력은 다른 종류의 능력입니다. 전자는 속도와 정확도의 문제이고, 후자는 어디를 파야 열리는지를 아는 감각의 문제죠. 보조정리를 놓고 목표를 고쳐가며 계산기를 부르는 이 방식이 후자 쪽에 닿았다는 점이 그래서 눈에 띕니다. 단순히 답을 맞히는 기계가 아니라, 증명의 중간 지형을 바꾸는 도구가 되었다는 뜻이니까요.

물론 여기서도 과장하지 않고 읽어야 합니다. 강화된 형태를 검증했다는 말이 그 추측 전체를 닫았다는 뜻은 아닙니다. 차원이 한정되어 있고, 조건이 붙은 성취죠. 하지만 Lean으로 검증됐다는 꼬리표가 붙었다는 점은 가볍지 않습니다. 사람의 손으로 쓴 증명은 나중에 빈틈이 발견되기도 하는데, Lean을 통과했다는 건 적어도 규칙 안에서는 빈틈이 없다는 확인을 받았다는 뜻이기 때문입니다. 저는 이 지점에서 기계 증명의 묘한 매력을 느꼈습니다. 빠르게 푸는 것을 넘어, 오래 남는 형태로 남긴다는 점 말이죠.

그래서 다음에 보고 싶은 장면은 무엇일까

지금까지의 이야기를 한 줄로 모으면 이렇습니다. 말로 방향을 잡고, 셈으로 확정하고, Lean으로 도장을 받는 분업이 실제로 돌아갔다는 것이죠. 그런데 글을 덮기 전에 남는 질문이 있습니다. 이 분업은 어디까지 넓어질 수 있을까요?

제가 앞으로 보고 싶은 것은 세 가지입니다. 하나는 부등식을 넘어선 모습입니다. 지금의 분업이 보조정리와 목표 변형과 엔진 선택의 맞물림이라면, 비슷한 맞물림이 다른 수학 영역에서도 통할지 궁금합니다. 다른 하나는 실패의 기록입니다. 186문제 중 풀지 못한 문제들은 어떤 모양이었을까요? 계산기가 없어서 막혔는지, 보조정리가 빗나가서 막혔는지, Lean 옮겨 적기에서 막혔는지를 알면 다음 설계의 방향이 보일 겁니다. 마지막 하나는 사람의 자리입니다. 이런 에이전트가 증명의 초안을 Lean이 받는 형태로 뽑아준다면, 사람은 그 다음에 무엇을 해야 할까요? 증명을 읽고 가르치는 일, 어디가 왜 열리는지를 설명하는 일은 여전히 사람의 몫으로 남을까요?

그렇다면 사람의 역할은 무엇일까요. 저는 답을 미리 정하고 싶지 않습니다. 다만 한 가지는 분명해 보입니다. 증명을 손으로만 쓰던 시대에는 셈의 끝까지 책임지는 것이 미덕이었는데, 셈을 잘하는 동료가 생긴 뒤에는 어디에 다리를 놓고 무엇을 물을지가 더 큰 실력이 됩니다. 좋은 보조정리를 고르는 눈, 목표를 잘게 나누는 솜씨, 계산기에 무엇을 맡길지 정하는 판단이 앞으로의 증명 실력에 더해지는 것이죠. 이 글을 읽는 분이라면, 다음에 부등식 앞에서 막힐 때 이런 질문을 함께 던져보셔도 좋겠습니다. 지금 막힌 곳이 생각의 문제인지, 셈의 문제인지, 그리고 그 셈을 누구에게 맡기면 Lean이 고개를 끄덕일지 말이죠.