Benchmark · math

PutnamBench

2 resultados 1 modelos

PutnamBench es un benchmark de demostración formal de teoremas construido con matemática de competición universitaria: mide cuántos problemas de la Competición Putnam puede demostrar un sistema dentro de un asistente de pruebas (Lean 4, Isabelle o Coq), y se puntúa como el número o la fracción de pruebas verificadas por máquina.

Ejemplo: Un problema difícil de Putnam de nivel universitario — por ejemplo, una afirmación de divisibilidad de teoría de números, una cota de una integral o desigualdad, o una identidad combinatoria — presentado como el enunciado de un teorema formal cuya prueba se deja como `sorry` para que el sistema la complete.
Puntuación: La métrica es el número (o porcentaje) de problemas para los que el sistema produce una prueba formal completa. Un problema cuenta solo si el asistente de pruebas lo verifica por completo; los argumentos parciales o el razonamiento informal puntúan cero.
Verificación: Un resultado se acepta solo cuando el núcleo del asistente de pruebas objetivo verifica por tipos toda la prueba sin `sorry`, sin axiomas adicionales y sin alterar el enunciado dado; el sí/no del verificador es el único juez.
Por qué importa: Los problemas de Putnam están entre lo más difícil de la matemática universitaria, y las pruebas verificadas por máquina no dejan margen para razonamientos incorrectos o manipulados, lo que convierte a PutnamBench en un sucesor riguroso y mucho más difícil de MiniF2F para la demostración automática de teoremas y el razonamiento matemático.

Ejemplo resuelto

Tarea

(Ilustrativo, simplificado.) Un teorema en Lean 4 con el formato de PutnamBench, para demostrar sin sorry: ```lean theorem putnam_illustrative (n : ℕ) : ∑ i ∈ Finset.range n, (2 * i + 1) = n ^ 2 := by sorry ```

Solución

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

Explicación

La suma de los primeros n números impares es n^2; se demuestra por inducción: el caso base se reduce a 0 = 0, y el paso usa Finset.sum_range_succ, aplica la hipótesis de inducción y cierra k^2 + (2k+1) = (k+1)^2 con ring. Se aprueba solo porque el núcleo de Lean acepta cada paso; un ítem real de PutnamBench es mucho más difícil.

Leanstral 1.5

Cronología

Fecha	Modelo	Puntuación	Fuente
2026-07-03	Leanstral 1.5	587.0pts	Mistral lanzó Leanstral-1.5-119B-A6B
2026-07-03	Leanstral 1.5	587.0pts	Leanstral 1.5: Abundancia de pruebas para todos