벤치마크 · math

PutnamBench

2 결과 1 모델

PutnamBench는 대학 경시 수학으로 구성된 형식적 정리 증명 벤치마크로, 시스템이 증명 보조기(Lean 4, Isabelle, Coq) 안에서 Putnam 대회 문제를 몇 개나 증명할 수 있는지를 측정하며, 기계 검증된 증명의 개수 또는 비율로 채점합니다.

예시: 어려운 대학 수준의 Putnam 문제——예컨대 정수론의 가분성 주장, 적분이나 부등식의 한계, 또는 조합론적 항등식——이 형식적 정리 진술로 주어지며, 그 증명은 시스템이 채우도록 `sorry`로 남겨져 있습니다.
채점 방식: 지표는 시스템이 완전한 형식적 증명을 산출한 문제의 개수(또는 백분율)입니다. 증명 보조기가 완전히 검증한 경우에만 그 문제가 인정되며, 부분적 논증이나 비형식적 추론은 0점입니다.
검증 방식: 결과는 대상 증명 보조기의 커널이 `sorry` 없이, 추가 공리 없이, 주어진 진술을 바꾸지 않고 증명 전체를 타입 검사할 때에만 인정됩니다——검증기의 예/아니오만이 유일한 판정자입니다.
왜 중요한가: Putnam 문제는 대학 수학에서 가장 어려운 축에 들고, 기계 검증된 증명은 잘못되거나 '보상 해킹'된 추론의 여지를 남기지 않으므로, PutnamBench는 자동 정리 증명과 수학적 추론에서 MiniF2F를 훨씬 능가하는 엄격하고 어려운 후속 벤치마크가 됩니다.

예제 풀이

문제

(예시용, 단순화.) PutnamBench 형식의 Lean 4 정리로, sorry 없이 증명해야 합니다: ```lean theorem putnam_illustrative (n : ℕ) : ∑ i ∈ Finset.range n, (2 * i + 1) = n ^ 2 := by sorry ```

해답

```lean
theorem putnam_illustrative (n : ℕ) :
    ∑ i ∈ Finset.range n, (2 * i + 1) = n ^ 2 := by
  induction n with
  | zero => simp
  | succ k ih => rw [Finset.sum_range_succ, ih]; ring
```

풀이

처음 n개의 홀수의 합은 n^2이며, 귀납법으로 증명합니다. 기저 단계는 0 = 0으로 귀착되고, 단계에서는 Finset.sum_range_succ를 사용하고 귀납 가정을 적용해 k^2 + (2k+1) = (k+1)^2를 ring으로 마무리합니다. 이것이 통과되는 이유는 Lean 커널이 모든 단계를 받아들이기 때문일 뿐, 실제 PutnamBench 문제는 훨씬 더 어렵습니다.

Leanstral 1.5

타임라인

날짜	모델	점수	출처
2026-07-03	Leanstral 1.5	587.0pts	Mistral, Leanstral-1.5-119B-A6B 출시
2026-07-03	Leanstral 1.5	587.0pts	Leanstral 1.5: 모두를 위한 증명 풍부함