HorizonMath: 자동 검증을 통한 수학적 발견을 향한 AI 진전 측정

기존 AI 수학 벤치마크는 이미 답이 알려진 문제만 다루어 모델의 진정한 연구 능력을 평가하기 어려웠습니다. HorizonMath는 실제 학계의 미해결 난제를 자동 검증 체계로 평가함으로써, AI가 단순한 문제 풀이 도구를 넘어 스스로 새로운 과학적 지식을 창출하는 연구 에이전트로 진화하고 있음을 입증합니다.

기존의 수학 데이터셋은 정답이 인터넷에 공개되어 있어 모델이 학습 과정에서 답을 암기했을 가능성이 크다. HorizonMath는 이 문제를 해결하기 위해 아직 아무도 답을 모르는 미해결 난제들을 평가 지표로 삼는다. 이는 AI가 단순히 기존 지식을 재구성하는 것이 아니라, 새로운 수학적 진리를 탐구할 수 있는지 확인하는 장치이다.

핵심 원리는 '생성-검증 격차(Generator-Verifier Gap)'에 있다. 복잡한 수학적 상수를 수식으로 찾아내거나 최적의 기하학적 구조를 설계하는 것은 매우 어렵지만, 일단 제안된 결과값이 특정 수치와 일치하는지 혹은 제약 조건을 만족하는지 확인하는 것은 컴퓨터 연산으로 매우 쉽고 정확하게 수행할 수 있다.

이 벤치마크는 AI에게 Python 코드로 해법을 제출하게 한 뒤, 이를 샌드박스 환경에서 실행하여 검증한다. 이를 통해 AI가 인간 연구자의 보조 도구를 넘어, 스스로 가설을 세우고 검증 가능한 결과물을 내놓는 독립적인 연구 주체로 거듭나고 있음을 정량적으로 보여준다.

벤치마크는 닫힌 형식(Closed-form)의 상수 발견, 이산적 구조 구성, 최적화 문제 등 세 가지 유형으로 설계되었다. 모든 문제는 Python 함수 def proposed_solution()을 통해 결과값을 반환해야 하며, 이는 자동화된 검증 파이프라인을 통과해야 한다.

수치적 검증 과정은 [모델이 생성한 symbolic 수식을 입력으로] → [mpmath 라이브러리를 통해 100자리 이상의 정밀도로 수치화하고 참조값과 비교하여] → [최소 20자리의 유효 숫자가 일치하는지 확인하고] → [일치할 경우 해당 수식을 유효한 추측으로 간주하는 방식]으로 진행된다.

최적화 문제의 경우 [모델이 생성한 기하학적 구조나 수치 리스트를 입력으로] → [문제별 Validator가 면적이나 상한선 등의 지표를 계산하여] → [기존 문헌에 발표된 최적값(Baseline)보다 개선되었는지 확인하고] → [개선된 경우에만 성공으로 판정하는 구조]를 갖는다. 모든 과정은 LLM 기반의 Admissibility Checker를 통해 수치적 편법이나 금지된 함수 사용 여부를 사전에 필터링한다.

GPT 5.4 Pro, Gemini 3.1 Pro, Claude Opus 4.6을 대상으로 평가한 결과, 대부분의 모델이 미해결 문제에서 0%에 가까운 점수를 기록하여 현재 AI 기술의 한계를 드러냈다. 하지만 GPT 5.4 Pro는 전체 데이터셋에서 7%의 정답률을 보이며 유의미한 진전을 나타냈다.

특히 GPT 5.4 Pro는 두 가지 난제에서 기존 학계 기록을 경신했다. 'Thin-Triangle Kakeya' 문제에서는 기존 AlphaEvolve가 달성한 면적 0.11481을 0.10915로 약 4.93% 개선했다. 또한 'Diagonal Ramsey Numbers'의 상한선 상수 c를 기존 3.7992에서 3.6961로 낮추는 데 성공했다.

보정용으로 포함된 기해결 문제(Level 0)에서는 GPT 5.4 Pro가 50%, 나머지 모델들이 30%의 정답률을 기록했다. 이는 모델들이 기본적인 수학적 추론 능력은 갖추고 있으나, 실제 연구 수준의 난제를 해결하기 위해서는 더 고도화된 추론 능력이 필요함을 시사한다.

HorizonMath는 LLM의 출력을 결정론적 검증기(Deterministic Verifier)와 결합하여 환각 문제를 해결한다. 수치적 발견 문제에서는 mpmath를 사용하여 고정밀 참조값과 비교함으로써 AI가 제안한 수식이 우연히 일치할 확률을 극도로 낮춘다.

아키텍처 측면에서 이 벤치마크는 'Admissibility Checker'를 도입하여 모델이 수치적 근사치나 금지된 라이브러리를 사용하여 검증 시스템을 우회하는 것을 방지한다. 폐쇄형 수식은 반드시 허용된 연산자(유리수, 기본 초월함수, 특수 함수 등)의 유한한 조합으로만 구성되어야 한다.

최적화 문제 검증 시에는 구간 산술(Interval Arithmetic)과 엄밀한 기하학적 적분 알고리즘을 사용하여 AI가 제안한 해법이 수학적으로 결함이 없는지 확인한다. 이는 AI가 제시한 결과가 단순한 수치적 근사가 아닌, 실제 수학적 구조로서 가치가 있음을 보장한다.

수치적 일치가 해당 수식의 수학적 엄밀한 증명을 의미하지는 않으며, 최종 확정을 위해서는 전문가의 검토가 필요하다. 또한 LLM 기반의 Admissibility Checker가 드물게 유효한 해법을 오판하거나 정교한 편법을 놓칠 가능성이 존재한다.