Benchmark · math

PutnamBench

2 resultados 1 modelos

PutnamBench é um benchmark de prova formal de teoremas construído a partir de matemática de competição universitária: mede quantos problemas da Competição Putnam um sistema consegue provar dentro de um assistente de provas (Lean 4, Isabelle ou Coq), pontuado como o número ou a fração de provas verificadas por máquina.

Saiba mais

Exemplo: Um problema difícil de Putnam de nível universitário — por exemplo, uma afirmação de divisibilidade de teoria dos números, um limite de uma integral ou desigualdade, ou uma identidade combinatória — apresentado como o enunciado de um teorema formal cuja prova é deixada como `sorry` para o sistema completar.
Pontuação: A métrica é o número (ou porcentagem) de problemas para os quais o sistema produz uma prova formal completa. Um problema só conta se o assistente de provas o verifica por inteiro; argumentos parciais ou raciocínio informal pontuam zero.
Verificação: Um resultado é aceito somente quando o núcleo do assistente de provas alvo faz a checagem de tipos de toda a prova sem `sorry`, sem axiomas extras e sem alterar o enunciado dado — o sim/não do verificador é o único juiz.
Por que importa: Os problemas de Putnam estão entre os mais difíceis da matemática universitária, e provas verificadas por máquina não deixam espaço para raciocínio incorreto ou manipulado, tornando o PutnamBench um sucessor rigoroso e muito mais difícil do MiniF2F para prova automática de teoremas e raciocínio matemático.

Exemplo resolvido

Tarefa

(Ilustrativo, simplificado.) Um teorema em Lean 4 no formato do PutnamBench, a ser provado sem sorry: ```lean theorem putnam_illustrative (n : ℕ) : ∑ i ∈ Finset.range n, (2 * i + 1) = n ^ 2 := by sorry ```

Solução

```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
```

Explicação

A soma dos primeiros n números ímpares é n^2; prova-se por indução: o caso base reduz-se a 0 = 0, e o passo usa Finset.sum_range_succ, aplica a hipótese de indução e fecha k^2 + (2k+1) = (k+1)^2 com ring. Ele passa apenas porque o núcleo do Lean aceita cada passo — um item real do PutnamBench é bem mais difícil.

Leanstral 1.5

Linha do tempo

Data	Modelo	Pontuação	Fonte
2026-07-03	Leanstral 1.5	587.0pts	Mistral lançou Leanstral-1.5-119B-A6B
2026-07-03	Leanstral 1.5	587.0pts	Leanstral 1.5: Abundância de Provas para Todos