Measuring Progress in Reasoning Toward Mathematical Discovery with Automatic Verification

Motivation

• Known: FunSearch, AlphaEvolve, 그리고 여러 human-AI 협업 사례들은 LLM 기반 시스템이 조합론, 기하학, 정수론 등에서 기존 최고 기록(best-known bounds)을 개선하거나 미해결 Erdős 문제를 해결하는 등 수학적 발견에 기여할 수 있음을 보여주었다. 또한 FrontierMath, IMProofBench, First Proof 등 연구 수준(research-level) 벤치마크들이 미해결 문제에 대한 AI 성능을 측정하려는 시도로 등장하고 있다.
• Gap: 기존 수학 벤치마크(GSM8K, MATH, GPQA, Olympiad 계열 등)는 대부분 정답이 알려진 문제 해결(problem-solving) 능력만 평가하여 인간 지식 수준이라는 자연스러운 한계를 넘어서지 못하고, novel discovery를 측정할 수 없다. 반면 기존 research-level 벤치마크(FrontierMath, IMProofBench, First Proof 등)는 formal proof 검증이나 전문가 수작업 검토에 의존해 확장성이 떨어지고, 검증기가 비공개이거나 재현이 어렵다는 한계가 있다.
• Why: AI가 실제로 새로운 수학적 지식을 창출할 수 있는지 여부는 자율적 과학 발견이라는 AI 연구의 궁극적 목표(north star)와 직결되며, 이를 표준화되고 확장 가능하며 오염(contamination)에 강건한 방식으로 측정할 수 있는 방법론이 시급히 필요하다.
• Approach: 해가 알려지지 않았지만 후보 답을 계산적으로 손쉽게 검증할 수 있는 generator-verifier gap을 갖는 문제 유형(수치적 검증이 가능한 closed-form, construction/optimization, existence 문제)을 식별하여, 자동 검증 스크립트와 함께 113개의 미해결 문제로 구성된 벤치마크 HorizonMath를 구축한다.

Achievement

Figure 4. Model performance on HorizonMath across six frontier models: Kimi K2.6, GLM 5.1, DeepSeek V4 Pro, Claude Opus

1. 오염에 강건한 미해결 문제 벤치마크 구축: 여덟 개 수학·수리과학 분야에 걸쳐 113개의 대부분 미해결된 문제로 구성된 데이터셋을 제시하며, 정답이 존재하지 않으므로 데이터 오염(data contamination)에 면역이다.
2. 완전 자동화된 검증 프레임워크 제공: 고정밀 수치 비교와 결정론적 제약 조건 검사기를 이용해 인간 검토 없이 빠르고 객관적으로 정답 여부를 판별할 수 있는 오픈소스 검증 파이프라인을 공개한다.
3. 실제 수학적 발견 사례 확인: GPT 5.4 Pro가 3개 문제에서 기존에 알려지지 않았던 novel solution을 제시하여 미해결 질문을 해결하거나 기존 최고 기록을 개선함을 실증했다.
4. 최신 모델들의 성능 격차 규명: 여섯 개 frontier 모델 대부분이 HorizonMath에서 거의 0%에 가까운 점수를 기록하는 등, 현재 LLM의 진정한 연구 능력과 문제 해결 능력 간의 큰 격차를 드러냈다.

How

Figure 3. HorizonMath’s automated evaluation pipeline. A model generates a proposed solution, which is screened by a com

• 문제 유형 3가지 정의: (1) closed-form 해가 미지수이나 고정밀 수치 참조값과 비교 가능한 문제, (2) 최적성이 증명되지 않은 baseline을 개선하는 construction/optimization 문제, (3) 아직 발견되지 않은 대상 객체가 필요한 모든 속성을 만족하는지 검증하는 existence 문제.
• 난이도 계층 분류: Level 0(Calibration)부터 Level 3(Likely unsolvable)까지 4단계로 문제를 분류하여 벤치마크의 난이도 스펙트럼을 구성.
• 자동 평가 파이프라인 구축: 모델이 제안(proposal)을 생성하면 결정론적 검증 스크립트가 이를 검사하는 end-to-end 파이프라인을 설계.
• 모델 비교 실험: GPT 5.4 Pro를 포함한 여섯 개 frontier 모델(Kimi K2.6, GLM 5.1 등)에 대해 벤치마크 성능과 추론 효율성(reasoning efficiency), 추론 궤적(reasoning trace) 행동을 비교 분석.

Originality

• 기존 연구가 formal proof 검증이나 전문가 수작업 리뷰에 의존한 것과 달리, generator-verifier gap이라는 개념을 명시적으로 활용해 완전 자동화되고 확장 가능한 검증 체계를 제안한 점이 독창적이다.
• 문제와 검증기를 모두 공개하는 오픈소스 정책은 FrontierMath 등 비공개 검증기를 사용하는 기존 벤치마크와 대비되는 재현성 및 커뮤니티 확장성을 제공한다.
• 단순 벤치마크 제안에 그치지 않고 실제로 GPT 5.4 Pro가 미해결 문제를 해결하는 사례를 발굴함으로써 벤치마크의 실효성을 실증적으로 입증했다.

Limitation & Further Study

• 고정밀 수치 비교는 closed-form 표현이 엄밀하게(formally) 정확함을 증명하지 못하며, 저자들도 이를 인정하고 있어 완전한 수학적 엄밀성 확보에는 한계가 있다.
• 113개라는 비교적 작은 문제 규모와 subjective한 solvability level 분류(저자 판단에 의존)는 벤치마크의 대표성과 객관성에 제약을 줄 수 있다.
• 발견된 3개의 novel solution 사례가 실제로 학계에 의해 검증·인정받는 과정(peer review 등)이 아직 이루어지지 않아, "진정한 발견"이라는 주장의 최종 확증에는 시간이 필요하다.
• 향후에는 벤치마크 문제 수와 도메인을 확장하고, 커뮤니티 기여를 통한 지속적 문제 추가 및 검증기 신뢰성 강화 등의 후속 연구가 필요하다.

Evaluation

총평: AI의 진정한 수학적 발견 능력을 측정하기 위한 새롭고 실용적인 접근을 제시하며, 실제 미해결 문제 해결 사례까지 확보한 점에서 임팩트가 크다.다만 수치적 검증의 엄밀성 한계와 상대적으로 작은 벤치마크 규모는 향후 보완이 필요한 지점이다.