Saltar al contenido principal

Una publicación etiquetados con "TTRL"

Ver Todas las Etiquetas

Stanford CS329A (Ep 14): AlphaProof & Mathematical Reasoning — Verificación formal, Lean 4, AlphaGeometry y Gemini Deep Think

· 9 min de lectura
Jaybee
AI & Robotics Engineer

En la lección anterior sobre Razonamiento en LLMs, analizamos cómo la técnica de Cadena de Pensamiento (Chain-of-Thought, CoT) y la decodificación por Autoconsistencia (Self-Consistency) encendieron la chispa del razonamiento causal multietapa en redes neuronales. Sin embargo, en fronteras críticas —como la verificación de protocolos criptográficos, software de control orbital o demostraciones matemáticas de élite mundial— el texto en lenguaje natural adolece de una debilidad intrínseca:

"Por más elocuente y convincente que parezca una cadena de razonamiento en lenguaje natural generada por un LLM, sigue siendo una secuencia estocástica de tokens probabilísticos. Un único error sutil de signo, una premisa circular o un lema alucinado desmorona por completo el sistema. En las matemáticas rigurosas, una demostración correcta al 99% equivale a una demostración correcta al 0%."

Bienvenidos a la Lección 14 de Stanford CS329A: Self-Improving AI Agents, correspondiente a la Parte 4: Fronteras (Frontiers in Reasoning & Autonomy). Inspirados en los avances pioneros dirigidos por el Dr. Thang Luong (Director Sénior de Investigación en Google DeepMind), examinamos cómo la inteligencia artificial trascendió la predicción estocástica de palabras para transformarse en deducción matemática mecánica e infalible, culminando en históricas medallas en la Olimpiada Internacional de Matemáticas (IMO):

  • AlphaGeometry (Nature 2024): Síntesis neuro-simbólica que fusiona motores deductivos deterministas con transformadores generativos para construcciones geométricas auxiliares.
  • AlphaProof (DeepMind, Nature 2025): Redefinición de la demostración formal de teoremas como un juego de tablero estilo AlphaZero utilizando Lean 4, autoformalización y Aprendizaje por Refuerzo en Tiempo de Prueba (TTRL).
  • Gemini Deep Think (IMO 2025): Triunfo del razonamiento puro en lenguaje natural y pensamiento paralelo (Parallel Thinking), obteniendo la primera Medalla de Oro oficial en la IMO (35/42) dentro del límite humano de 4.5 horas.
  • Verificación formal en LLMs y razonamiento matemático: Comparación técnica entre núcleos formales compilados por máquina y modelos de lenguaje basados en refuerzo no restringido.