FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?

이 논문은 대학원 수준의 수학 정리를 Lean 4 로 형식적으로 검증 가능한지 평가하기 위해 'FormalProofBench'라는 벤치마크를 제안하고, 최첨단 AI 모델들이 이 작업에서 33.5% 의 정확도를 보이며 도구 사용 및 실패 모드 등에 대한 심층 분석을 제공함을 보여줍니다.

핵심

1. 이 실험의 핵심: "FormalProofBench" (공식 증명 벤치마크)

기존의 수학 시험 (예: MATH, IMO) 은 AI 가 자연어 (영어 등) 로 답을 쓰면, 사람이나 다른 AI 가 "아, 논리적으로 그럴듯하네"라고 채점했습니다. 하지만 AI 가 거짓말을 하거나, 중요한 경우를 빼먹거나, 존재하지 않는 공리를 인용하는 실수를 해도 사람이 눈치채기 어렵습니다. 마치 학생이 "그냥 그렇게 된 거예요"라고 말하면 선생님이 "아, 그렇구나"라고 넘어가는 것과 비슷하죠.

이 논문은 그런 문제를 해결하기 위해 Lean 4라는 '수학용 컴퓨터 언어'를 사용했습니다.

• 비유: AI 가 답을 쓸 때, 사람이 읽는 글이 아니라 컴퓨터가 직접 실행해 볼 수 있는 코드로 답을 써야 합니다.
• 결과: 컴퓨터가 "이 코드는 오류가 있다"고 하면 바로 틀린 것이고, "컴파일 (실행) 성공"이 되어야만 정답입니다. 즉, **거짓말이나 뻔뻔한 추론이 통하지 않는 '완벽한 시험'**을 만든 것입니다.

2. 시험 문제의 난이도: "대학원생도 울고 갈 문제들"

이 벤치마크는 고등학교 수학 경시대회 수준이 아닙니다.

• 문제 출처: 대학원 진학 시험 (Qualifying Exams) 과 전문 수학 교재에서 가져왔습니다.
• 주제: 해석학, 대수학, 확률론, 논리학 등 매우 추상적이고 어려운 분야들입니다.
• 난이도: 수학 전공 박사 과정 학생들도 풀기 힘든 문제들입니다.

3. 실험 방법: "AI 의 40 번의 기회"

AI 에게 문제를 주고 한 번에 답을 내게 하지 않았습니다. 대신 **40 번의 기회 (Turn)**를 주었습니다.

• 도구 사용: AI 는 두 가지 도구를 쓸 수 있습니다.
  1. Lean Loogle (검색): 수학 도서관 (Mathlib) 에서 필요한 공식을 검색합니다.
  2. Lean Executor (실행): 쓴 코드를 컴퓨터에 돌려보고 "오류가 났다"는 피드백을 받습니다.
• 과정: AI 는 코드를 쓰고, 오류가 나면 수정하고, 다시 검색하고, 다시 실행하는 과정을 반복하며 40 번 안에 정답을 찾아야 합니다.

4. 주요 결과: "AI 는 아직 수학자처럼 완벽하지 않다"

최고급 AI 모델들을 시험에 참여시켰는데, 결과는 다음과 같았습니다.

• 최고 점수: 33.5% (Anthropic 의 Claude Opus 4.5 모델이 1 위).
  • 즉, 100 개의 문제 중 33 개 정도만 완벽하게 증명했습니다. 나머지 67 개는 실패했습니다.
• 점수 하락: 1 위 모델 다음으로 점수가 급격히 떨어졌습니다.
• 결론: AI 는 수학 문제를 풀 때 '감'이나 '추측'은 잘하지만, **엄격한 논리 검증 (컴퓨터가 통과하는 증명)**을 해내는 능력은 아직 인간 수학자나 대학원생 수준에 미치지 못합니다.

5. 흥미로운 발견: "검색보다 실행이 중요했다"

가장 흥미로운 점은 성공한 AI 들의 행동 패턴이었습니다.

• 실패한 패턴: 계속 '검색 (Loogle)'만 하다가, 없는 공리를 찾아 헤매거나 막히면 멈춰버렸습니다. (지나친 검색)
• 성공한 패턴: 일단 코드를 **실행 (Run Code)**해보고, 컴퓨터가 주는 "오류 메시지"를 보고 수정하는 과정을 반복했습니다.
• 비유: 수학 문제를 풀 때, 책 (검색) 을 계속 뒤적이는 것보다 연필로 직접 계산을 해보고 (실행), 틀리면 지우개로 고치는 과정을 반복하는 학생이 더 잘 맞춘다는 뜻입니다.

6. 이 연구의 의미: "수학의 새로운 파트너"

이 연구는 AI 가 수학 분야에서 실제 연구자 (수학자) 의 도구로 쓰일 수 있는지 확인하는 첫걸음입니다.

• 현재: AI 가 증명할 수 있는 문제는 아직 많지 않습니다.
• 미래: 이 벤치마크를 통해 AI 의 능력을 측정하고 개선하면, 언젠가 AI 가 수학자가 "이 증명 맞을까?"라고 의심할 때, AI 가 "컴퓨터가 검증했으니 100% 맞습니다"라고 말해주는 날이 올 것입니다.

요약

이 논문은 **"AI 가 수학 문제를 풀 때, 사람이 읽는 글이 아니라 컴퓨터가 검증하는 코드로 답을 내게 했더니, 최고의 AI 도 100 점 만점에 33 점 정도밖에 못 받았다"**는 사실을 밝혔습니다. 하지만 AI 가 **컴퓨터 오류 메시지를 보고 스스로 수정하는 과정 (실행과 반복)**을 잘할수록 성적이 좋아진다는 귀중한 교훈을 남겼습니다.

기술 요약

1. 문제 정의 (Problem)

대규모 언어 모델 (LLM) 은 MATH, AIME 와 같은 자연어 기반 수학 벤치마크에서 뛰어난 성과를 보이고 있지만, 이러한 자연어 해답은 미묘한 논리적 오류를 숨길 수 있습니다. 인간이나 LLM 기반 감점자조차 간과할 수 있는 누락된 경우나 존재하지 않는 보조정리 (lemma) 사용 등의 오류가 발생할 수 있습니다.

이러한 한계를 극복하기 위해 형식적 검증 (Formal Verification) 이 필요하지만, 현재까지의 벤치마크는 고등학교 수준이나 대학 학부 수준의 문제에 국한되거나, 단일 순방향 추론 (one-shot) 에 의존하는 경우가 많았습니다. 본 논문은 대학원 수준의 수학 문제를 대상으로 하며, Lean 4와 같은 형식적 증명 도구를 사용하여 모델이 생성한 증명이 기계적으로 검증 가능한지 (type-checking 통과 여부) 를 평가하는 새로운 벤치마크의 필요성을 제기합니다.

2. 방법론 (Methodology)

2.1 벤치마크 구성 (FormalProofBench)

• 데이터 수집 및 선별: 200 개의 문제를 포함하며, 실해석학, 대수학, 확률론, 논리학 등 대학원 수준 (Qualifying exams 및 표준 교과서) 의 주제를 다룹니다.
• 형식화 (Formalization): 모든 문제는 Lean 4 와 Mathlib 라이브러리를 사용하여 형식화되었습니다. 6 명의 Lean 전문가 (PhD 학생 및 도메인 전문가) 가 문제를 작성하고, 2 차 검토 과정을 통해 형식화 오류 (misformalization) 를 방지했습니다.
• 검증 기준: 모델이 생성한 Lean 증명이 Lean 4 커널에 의해 성공적으로 컴파일되고 검증되어야만 정답으로 간주됩니다. 이는 이진 (Binary) 이며 완전히 자동화된 정답 신호를 제공합니다.

2.2 평가 환경 (Evaluation Harness)

• 에이전트 루프 (Agentic Loop): 모델은 문제를 한 번에 해결하는 것이 아니라, 최대 40 턴 (turns) 에 걸쳐 상호작용하며 증명을 완성합니다.
• 제공 도구:
  • lean_loogle: Mathlib 내의 정리 및 정의 검색 도구.
  • lean_run_code: Lean 코드를 실행하여 오류 메시지, 미해결 목표 (goals), 타입 불일치 등을 피드백받는 도구.
  • submit_proof: 최종 증명을 제출하는 도구.
• 프롬프트: 모델은 자연어 문제와 Lean 형식화 문맥을 제공받으며, Lean 4 문법 규칙과 도구 사용 전략에 대한 시스템 프롬프트를 따릅니다.

3. 주요 기여 (Key Contributions)

1. 새로운 벤치마크 제시: 대학원 수준의 형식적 증명 능력을 평가하는 새로운, 현실적이고, 결정론적이며, 데이터 오염 (contamination) 에 강한 벤치마크인 FormalProofBench를 공개했습니다.
2. 심층 평가: 200 개의 정교하게 형식화된 문제를 통해 최첨단 (Frontier) 모델들의 대학원 수준 형식적 증명 능력을 상세히 평가했습니다.
3. 비용 및 지연 시간 분석: 검색 도구와 코드 실행 도구를 사용하는 다중 턴 에이전트 환경에서의 모델 비용과 지연 시간 (latency) 을 분석했습니다.
4. 도구 사용 패턴 분석: 코드 실행을 통한 반복적 시도 (iteration) 가 성능과 강한 상관관계가 있음을 발견했습니다.

4. 결과 (Results)

4.1 성능 (Accuracy)

• 최고 성능: Anthropic 의 Claude Opus 4.5 (Thinking) 가 **33.5%**의 정확도를 기록하여 1 위를 차지했습니다.
• 성능 하락: 그 다음으로 Gemini 3 Pro (18.5%), Claude Sonnet 4.5 (18.0%), GPT 5 (17.0%) 등이 이어졌으며, 그 이후 모델들의 성능은 급격히 하락했습니다.
• 전반적 난이도: 최상위 모델조차 100% 에 훨씬 미치지 못하는 점수는 대학원 수준 형식적 증명의 난이도를 보여줍니다.

4.2 도구 사용 및 실패 모드 분석

• 코드 실행의 중요성: 성공적인 모델들은 초기에 lean_run_code를 통해 코드를 실행하고 피드백을 받으며 증명을 수정하는 전략을 취했습니다.
• 검색의 함정: 실패하는 모델들은 종종 존재하지 않는 보조정리를 찾기 위해 lean_loogle 을 과도하게 사용하는 "스파이럴 (spiral)" 현상을 보였습니다.
• 상관관계: 코드 실행 호출 횟수와 정확도 사이에는 긍정적이지만 modest 한 상관관계가 관찰되었습니다. (예: GPT 5 는 적은 실행 횟수로 높은 정확도를 보였으나, Grok 4.1 은 많은 실행에도 낮은 정확도를 보임)

4.3 비용 및 지연 시간

• 비용: 테스트당 평균 비용은 약 10 센트에서 1 달러 이상까지 다양했습니다.
• 지연 시간: 모델이 최종 제출을 위해 시도하는 동안 평균 1 시간 이상의 지연 시간이 발생했습니다 (예: Claude Sonnet 4.5 는 약 11,000 초).

5. 의의 및 결론 (Significance)

• 형식적 검증의 중요성: 자연어 해답과 형식적 검증 사이의 격차는 여전히 크지만, AI 모델의 빠른 발전 속도를 고려할 때 수학자들이 실제로 사용할 수 있는 도구에 근접하고 있음을 시사합니다.
• 연구 방향: 형식적 증명은 수학 연구의 표준 도구가 될 잠재력이 있으며, 이 벤치마크는 모델의 진전을 추적하는 데 중요한 기준이 될 것입니다.
• 미래 과제:
  • 검색 도구의 한계를 극복하기 위한 시맨틱 검색이나 로컬 코드베이스 탐색 기능 도입.
  • 자연어 문제 없이 형식적 문장만 제공했을 때의 성능 분석 (번역 능력 vs 증명 능력 분리).
  • Mathlib 의 확장으로 연구 수준의 더 복잡한 정리를 다루는 벤치마크로 확장.

요약하자면, FormalProofBench 는 AI 모델이 대학원 수준의 수학 문제를 형식적으로 증명할 수 있는 능력을 평가하는 엄격하고 자동화된 벤치마크를 제시하며, 현재 최상위 모델조차 33.5% 의 정확도에 그치고 있음을 보여주었습니다. 이는 형식적 수학 증명이 여전히 어려운 과제임을 의미하지만, 코드 실행을 통한 반복적 검증이 성공의 핵심 요소임을 강조합니다.