Un test construido con investigación, no con ejercicios
Un grupo de la Universidad Tsinghua, Moonshot AI y el Instituto Shanghai Qizhi ha publicado TCSExam, un test que pide a agentes de modelos de lenguaje hacer informática teórica en lugar de responder preguntas sobre ella. El artículo apareció en arXiv el 5 de noviembre; entre sus autores están Zhilin Yang, de Moonshot AI, y Andrew Chi-Chih Yao, de Tsinghua.
El conjunto completo son 100 tareas revisadas por expertos en cuatro vías. Veinte son teoremas de investigación que deben demostrarse en Lean 4, donde el núcleo decide si la entrega cuenta. Treinta son problemas de ingeniería de solucionadores, donde el agente entrega un programa reutilizable que se ejecuta sobre familias de instancias. Veinte son construcciones, puntuadas frente a récords documentados. Las últimas treinta son conjeturas abiertas: demostrar el enunciado o su negación, y nada por debajo de una demostración completa cuenta como resolución.
La tabla
Ocho agentes se ejecutaron sobre el conjunto completo. GPT-6 Astra lidera el índice TCSExam con 71,9, por delante de Kimi K3.1 Pro con 57,4, Kimi K3 con 46,8, la versión de octubre de DeepSeek V4.1 Flash con 46,0, GLM-5.3 con 45,5, Qwen3.8 Max con 44,8, Grok 4.6 con 40,5 y la versión de septiembre de DeepSeek con 40,4.
Un subconjunto Lite de 20 tareas, cinco por vía, reduce el número de intentos en un 80% con el mismo presupuesto por intento. Nueve agentes se ejecutaron sobre él, y Opus 5.5 — que no se ejecutó sobre el conjunto completo — lo encabeza con 72,3, por delante del 67,0 de GPT-6 Astra. Los dos conjuntos ordenan a los ocho agentes comunes casi igual, con una rho de Spearman de 0,93.
Nadie cerró una conjetura
La vía de conjeturas abiertas es donde el test resulta más útil y menos halagador. Los autores no registran ninguna solución completa aceptada a ninguna conjetura abierta.
Se aceptaron dos entregas, y el artículo es explícito sobre lo que eran. Kimi K3.1 Pro y la versión de octubre de DeepSeek recuperaron contraejemplos y demostraciones en Lean que OpenAI ya había publicado para la conjetura de Ryser y la conjetura modificada de redondeo entero, y las adaptaron a las definiciones de las tareas. El artículo señala que las tareas se escribieron antes de la publicación de OpenAI.
El único resultado genuinamente nuevo es más estrecho y está mejor respaldado. GPT-6 Astra demostró la conjetura de Alon–Jaeger–Tarsi sobre el cuerpo de cinco elementos para todo n hasta 9, usando identidades de conteo y un certificado entero exacto para descartar un contraejemplo mínimo. El artículo dice que una verificación independiente en Lean lo confirma usando solo axiomas estándar, y que amplía resultados previos que llegaban a n ≤ 7 y n ≤ 8. En el apéndice hay cuatro casos particulares verificados más.
Lee la línea de autoría
Las puntuaciones son del propio equipo del test, y dos de los autores trabajan en Moonshot AI, cuyos modelos Kimi ocupan el segundo y el tercer puesto del conjunto completo. Opus 5.5 solo aparece en Lite, así que su 72,3 no puede compararse con el 71,9 de GPT-6 Astra en el conjunto completo.
Conviene no confundir lo que el test mide. Una demostración de un caso particular verificada en Lean es una contribución comprobable; recuperar un contraejemplo publicado y reformatearlo no es lo mismo, y TCSExam es de las pocas evaluaciones que distingue ambas cosas por escrito.
