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 →
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 →
Corrección de errores cuánticos con estabilizadores
La corrección de errores cuánticos es un aspecto crucial en el escalado de ordenadores cuánticos para poder aprovechar la ventaja cuántica y desarrollar algoritmos de manera fiable. Los principales tipos de errores son el error de inversión de bit, que altera el estado de un qubit de $latex |0\rangle$ a $latex |1\rangle$ (y viceversa), el... Seguir leyendo →
Deep learning y sistemas complejos
El objetivo de este proyecto es desarrollar y divulgar conocimiento de sistemas complejos, ciencia de redes y especialmente relacionar el deep learning y los sistemas complejos. Complementar los modelos de sistemas complejos con deep learning, aplicarlo sobre datos representados en redes tanto para resolver problemas sobre redes (clasificación de nodos, enlaces, propiedades de las redes,... Seguir leyendo →
Graph Neural Networks con PyTorch Geometric
En este post vamos a ver una introducción a las Graph Neural Networks (GNNs) y la librería PyTorch Geometric, que nos permite aplicar el deep learning a datos no estructurados, como grafos, empleando este tipo de modelos. Las GNNs permiten aplicar redes neuronales a grafos, teniendo en cuenta su estructura basada en nodos conectados entre... Seguir leyendo →
Autograd, clave de la flexibilidad de PyTorch
Esta entrada es parte del curso de Deep learning con PyTorch. En los últimos dos años hemos visto como PyTorch, el framework basado en Torch para Deep Learning creado por Facebook, está siendo una alternativa potente a Tensorflow. Una de las principales ventajas de PyTorch es que es un framework imperativo, en el que las... Seguir leyendo →
Spark para Machine learning en Google Colab
Con el incremento en la cantidad de datos y procesamiento en los últimos años, se ha hecho necesario disponer de nuevos paradigmas de computación paralela que permitan repartir la carga de procesamiento en múltiples máquinas mejorando así la eficiencia del proceso. Fruto de esta necesidad surgió MapReduce y Apache Spark, una extensión de este. Spark... Seguir leyendo →
Las GPUs y el machine learning
Uno de los factores que más ha impulsado el deep learning en los últimos años ha sido el uso de las GPUs (graphics processing unit) para acelerar el entrenamiento y despliegue de los algoritmos. Las GPUs son circuitos electrónicos, popularizadas por Nvidia y especializadas en procesado de imágenes y gráficos. Cuentan con una estructura paralela... Seguir leyendo →
