En Julio de 2026, Anthropic introdujo una nueva técnica de interpretabilidad, las J-lens, para identificar en un LLM lo que en neurociencias se llama el espacio de trabajo (workspace), el conjunto de representaciones internas disponibles para comunicación, razonamiento y modulación. Serían los pensamientos accesibles frente al procesamiento inconsciente. Consideramos el vector de la corriente residual... Seguir leyendo →
Mathlib en Lean 4. Componentes y tácticas
Mathlib es la biblioteca matemática comunitaria para Lean 4. Se trata de un proyecto colaborativo masivo, con millones de líneas de código, cuyo objetivo es formalizar de manera unificada las matemáticas, desde la lógica básica hasta el álgebra, el análisis y la teoría de números. Tiene una estructura de grafo acíclico dirigido (DAG) de archivos... Seguir leyendo →
Reglas de eliminación de los tipos inductivos en Lean 4
En el post sobre Lean como lenguaje de tipos vimos que los tipos inductivos son la construcción para definir nuevos tipos de datos y que se especifican enumerando sus constructores, que son las formas básicas de construir elementos del tipo. Además, cuentan con las reglas de eliminación, que son el mecanismo fundamental que permite definir... Seguir leyendo →
GRPO paso a paso para ajustar LLMs
GRPO (Group Relative Policy Optimization) es un algoritmo de aprendizaje por refuerzo para afinar LLMs, creado por DeepSeek. Es clave en DeepSeek-R1. Es una variante de PPO (Proximal Policy Optimization) que elimina la necesidad de un modelo crítico (value network). Para cada prompt genera un grupo de respuestas, cada una recibe una recompensa (usando una... Seguir leyendo →
Demostraciones hacia atrás (backward) y hacia adelante (forward) en Lean 4
En Lean 4 existen dos enfoques principales para construir demostraciones: el enfoque hacia atrás (backward) y hacia adelante (forward). Ambos son formas de construir el mismo término de prueba, pero difieren en la dirección en que razona el demostrador. En ocasiones, es útil usar un enfoque híbrido que combine los dos enfoques. BACKWARD PROOFS (PRUEBAS... Seguir leyendo →
Introducción a Lean 4 como lenguaje de tipos para las matemáticas
Lean 4 es un lenguaje de programación funcional y un asistente de pruebas interactivo basado en la teoría de tipos dependientes. Su fundamento lógico es el cálculo de construcciones con una jerarquía de universos e tipos inductivos . La idea central es que en matemáticas, cada objeto (un número, una función, una demostración) tiene un... Seguir leyendo →
Reward hacking, problema inherente de la IA avanzada sin solución estructural
Historia En los inicios de los LLMs, estos se entrenaban solo con aprendizaje semisupervisado prediciendo el siguiente token en gigantescos corpus de texto de Internet. Este paradigma permitía al modelo aprender gramática, hechos y estructuras lingüísticas complejas, pero carecía de capacidad de acción. El modelo simplemente replicaba los patrones estadísticos de los datos de entrenamiento.... Seguir leyendo →
IA, las matemáticas y Navier-Stokes
En los últimos días, después del anuncio de OpenAI de la resolución de varios de los casos del problema de Navier-Stokes (NS), hemos visto discusiones sobre la capacidad de la IA en las matemáticas y el futuro de las matemáticas. Es necesario recalcar, como hemos ido defendiendo en este sitio , las capacidades de los... Seguir leyendo →
El residual stream en un LLM basado en Transformers
Como vimos en el post de interpretabilidad mecanicista, uno de sus objetivos es rastrear el flujo de información a través de un modelo. El residual stream (flujo residual) es uno de los conceptos más importantes para entender cómo funcionan internamente los modelos basados en Transformers. En lugar de ver al Transformer como una serie de... Seguir leyendo →
Interpretabilidad mecanicista con TransformerLens
En un post pasado vimos una introducción a la interpretabilidad mecanicista y como intenta extraer información de los pesos y activaciones de los LLMs. Una de las librerías más usadas en interpretabilidad mecanicista es TransformerLens, que permite cargar un LLM open source y explorar y transformar las activaciones del modelo. Vamos a ver un ejemplo... Seguir leyendo →
