Investigadores de Google publicaron Stellar Colosseum, un sistema de múltiples agentes que reparte la inferencia entre tareas de investigación en matemáticas y ciencias de la computación teórica, y reportan un 71.0% de precisión en un benchmark de demostración de teoremas de nivel de investigación extraído de artículos de FOCS, STOC y SODA. El artículo, firmado por un equipo que incluye a Honghao Lin, David P. Woodruff y Vahab Mirrokni, describe un sistema agnóstico al modelo por diseño que ya fue incorporado a Google Antigravity.
El punto de partida es un modo de fallo conocido. Los modelos de lenguaje producen demostraciones cortas plausibles, pero se degradan en los problemas de horizonte largo, donde el avance depende de una cadena de decisiones inciertas e interdependientes y una sola mala elección temprana envenena todo lo que viene después. La respuesta de Colosseum es dejar de tratar una demostración como una única trayectoria.
Puntos clave
- Stellar Colosseum obtiene un 71.0% en TCS-Bench, un conjunto de tareas de demostración de teoremas de nivel de investigación tomadas de artículos de FOCS, STOC y SODA, con Gemini 3.1 Pro emparejado con Gemini 3.7 Flash.
- En una evaluación aparte sobre Codeforces con Gemini 3.1 Pro, la tubería orientada a demostraciones con retroalimentación de ejecución resolvió 218 de 222 problemas.
- El flujo de trabajo ya viene dentro del marco Teamwork de Google Antigravity como el patrón Long Proof, disponible como comando en vista previa en los planes de pago.
En qué gasta el cómputo
Colosseum recorre varias etapas antes de comprometerse a escribir una demostración. Primero explora estrategias alternativas en lugar de lanzarse por la primera que parece prometedora, y luego aplica una compuerta de madurez que decide si una ruta dada está lo bastante desarrollada como para descomponerla. Solo entonces representa el plan de la demostración como un conjunto de subproblemas interdependientes a nivel de sección.
La verificación está conectada de vuelta a esa estructura. Cuando un verificador señala un problema, el hallazgo se enruta a la parte concreta del argumento que afecta, en vez de obligar a empezar de cero. En todas las etapas el sistema genera candidatos en paralelo, los ataca con falsación dirigida y fusiona los candidatos y sus críticas en un único artefacto de investigación mediante lo que los autores llaman agregación en árbol por muestreo aleatorio solapado.
Es una apuesta distinta a la de ampliar el contexto de un solo agente y dejarlo pensar más tiempo. Se parece más a operar un pequeño grupo de investigación adversarial, salvo que aquí el recurso caro que se planifica es la inferencia y no el tiempo de los investigadores.
Qué dicen las cifras del benchmark
TCS-Bench es un objetivo más duro que los conjuntos de matemática de competencia que dominan los anuncios de modelos, porque sus tareas provienen de artículos aceptados en tres de las principales conferencias teóricas del campo. El 71.0% surge de una configuración mixta: Gemini 3.1 Pro junto al más económico Gemini 3.7 Flash, lo que sugiere que el sistema recupera calidad mediante coordinación y no derivando todo al modelo más grande.
El resultado de Codeforces es más acotado pero llamativo: 218 de 222 problemas resueltos con retroalimentación de ejecución en el bucle. Ambas cifras provienen de la evaluación de los propios autores y ninguna ha sido reproducida de forma independiente. La advertencia sobre benchmarks que corresponde a todo artículo de andamiaje de agentes aplica también aquí: estos resultados son notoriamente sensibles a detalles de prompts y herramientas que rara vez sobreviven a una reimplementación.
Del artículo al producto
A diferencia de la mayoría de los andamiajes de investigación, este ya tiene una superficie de producto. Google afirma que el flujo de Colosseum está integrado en el marco Teamwork de Antigravity como el patrón Long Proof, uno de los cinco entre los que el sistema elige, y que Teamwork ha producido siete resultados sobre problemas abiertos, entre ellos una cuestión de optimización convexa dispersa de un artículo de JMLR y la conjetura de los ciclos de Knuth, verificada en Lean.
El artículo sostiene haber obtenido resultados nuevos sobre problemas abiertos planteados en trabajos de FOCS y JMLR. Esa es una afirmación de naturaleza muy distinta a la precisión en un benchmark, y es la que el campo examinará con mayor dureza, como ocurrió con el intento de OpenAI sobre Navier-Stokes con 10.000 agentes, donde los asteriscos pesaron más que el titular. La verificación formal en Lean le da a Google una base más firme al menos en parte de esa afirmación.
Preguntas frecuentes
¿Qué es TCS-Bench?
TCS-Bench es un benchmark de tareas de demostración de teoremas de nivel de investigación tomadas de artículos publicados en FOCS, STOC y SODA, tres conferencias de referencia en ciencias de la computación teórica. Apunta a problemas de investigación abiertos y no a ejercicios de competencia. Stellar Colosseum reporta un 71.0% de precisión sobre él usando Gemini 3.1 Pro con Gemini 3.7 Flash.
¿Stellar Colosseum depende de Gemini?
No. Los autores describen el sistema como agnóstico al modelo: es una capa de planificación y agregación sobre cualquier modelo que atienda las llamadas. Las evaluaciones publicadas usan Gemini 3.1 Pro y Gemini 3.7 Flash, así que las cifras reportadas corresponden a esos modelos y no a la arquitectura en sí.
¿Pueden usarlo hoy los desarrolladores?
De forma indirecta. El flujo de Colosseum está disponible dentro del marco Teamwork de Google Antigravity como el patrón Long Proof, ofrecido como comando en vista previa en los planes de pago. El artículo en sí es una preimpresión en arXiv y no ha sido revisado por pares.
