Бенчмарк · math

PutnamBench

2 результатов 1 моделей

PutnamBench — это бенчмарк формального доказательства теорем на материале студенческой олимпиадной математики: он измеряет, сколько задач олимпиады Putnam система способна доказать внутри пруф-ассистента (Lean 4, Isabelle или Coq), а оценка — это число или доля машинно-проверенных доказательств.

Подробнее

Пример: Сложная студенческая задача Putnam — например, утверждение о делимости из теории чисел, оценка интеграла или неравенства либо комбинаторное тождество — представленная как формулировка формальной теоремы, доказательство которой оставлено как `sorry`, чтобы система его дописала.
Метрика: Метрика — число (или процент) задач, для которых система выдаёт полное формальное доказательство. Задача засчитывается, только если пруф-ассистент полностью её проверяет; частичные или неформальные рассуждения дают ноль.
Приёмка: Результат принимается, только если ядро целевого пруф-ассистента полностью проверяет доказательство без `sorry`, без дополнительных аксиом и без изменения исходной формулировки — единственный судья это вердикт верификатора «да/нет».
Почему важно: Задачи Putnam — одни из самых трудных в студенческой математике, а машинно проверяемые доказательства не оставляют места для ошибочных или «взломанных» рассуждений, что делает PutnamBench строгим и заметно более трудным преемником MiniF2F для автоматического доказательства теорем и математического рассуждения.

Разбор примера

Задача

(Иллюстративно, упрощённо.) Теорема на Lean 4 в формате PutnamBench, которую нужно доказать без 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: Изобилие доказательств для всех