Interactive theorem provers: theory and practice

Demostradores interactivos de teoremas: teoría y práctica

Paige Randall North

Utrecht University, Países Bajos

Horario:

Idioma: Inglés

Breve resumen de la materia

Existen diversas técnicas para la verificación formal del software. Una de ellas es programar en un lenguaje – por ejemplo, Coq, Agda y Lean – basado en la teoría de tipos de Martin-Löf. Esto ofrece la posibilidad de incluir pruebas de corrección en los programas. Tales lenguajes también se utilizan para verificar pruebas complejas de importantes teoremas matemáticos.

En este curso, proporcionaremos a los estudiantes una introducción a la teoría de tipos de Martin-Löf y sus implementaciones, en particular Coq. Exploraremos la expresividad de esta teoría y cómo los distintos asistentes de prueba y sus bibliotecas limitan esta expresividad al imponer axiomas adicionales, lo que lleva a una teoría de tipos extensional o a una teoría de tipos de homotopías (o algo intermedio). Veremos cuándo es apropiado imponer tales axiomas; por ejemplo, veremos que la teoría de tipos de homotopías proporciona un entorno para la verdadera independencia de representación de los tipos de datos.

Abstract

There are various techniques for formal verification of software. One technique is to program in a language – e.g. Coq, Agda, and Lean – based on Martin-Löf type theory. This offers the ability to include proofs of correctness in one’s programs. Such languages are also used to check complex proofs of important mathematical theorems.

In this course, we will provide students with an introduction to Martin-Löf type theory and implementations, in particular Coq. We will explore the expressiveness of this theory, and how the various proof assistants and their libraries limit this expresiveness by imposing additional axioms, leading to either extensional type theory or homotopy type theory (or something in between). We will see when it is appropriate to impose such axioms; for instance, we will see that homotopy type theory provides a setting for true representation independence of data types.

Objetivos del curso

Los objetivos de aprendizaje de este curso son los siguientes: 

  1. Conocer qué es la teoría de tipos dependientes y cuándo es útil.
  2. Familiarizarse con la programación en Coq y la biblioteca UniMath.
  3. Comprender las diferencias entre las distintas implementaciones de la teoría de tipos dependientes (es decir, Lean, Coq, Agda, Cubical Agda).
  4. Saber cuándo se pueden o deben aplicar axiomas como el Axioma K o el Axioma de Univalencia. 
  5. Comprender y programar con tipos inductivos y tipos inductivos superiores.

Objectives of the Course

The learning objectives for this course are the following.

  1. Know what dependent type theory is and when it is useful
  2. Become familiar with programming in Coq and the UniMath library
  3. Understand the differences between different implementations of dependent type theory (i.e. Lean, Coq, Agda, Cubical Agda)
  4. Know when one can or should apply axioms such as Axiom K or the Univalence Axiom
  5. Understand and program with inductive types and higher inductive types

Programa

  • Teoría de tipos de Martin-Löf (MLTT): tipos dependientes, tipos inductivos
  • Programación en Coq
  • Uso de la biblioteca UniMath
  • Axiomas en MLTT: K, univalencia
  • Semántica de MLTT: lógica (correspondencia Curry-Howard), conjuntos, espacios
  • Aspectos extensionales y de homotopía de MLTT: transporte, functorialidad del tipo identidad, grupoide de tipos
  • Verificación formal de las matemáticas en MLTT, utilizando diferentes axiomas
  • Independencia de representación mediante univalencia
  • Biblioteca UniMath

Brief Index

  • Martin-Löf type theory (MLTT): dependent types, inductive types
  • Programming in Coq
  • Using the UniMath library
  • Axioms in MLTT: K, univalence
  • Semantics of MLTT: logic (Curry-Howard correspondence), sets, spaces
  • Extensional and homotopy aspects of MLTT: transport, functoriality of identity type, groupoid of types
  • Formal verification of mathematics in MLTT, using different axioms
  • Representation independence using univalence
  • UniMath library

Prerrequisitos

Experiencia en programación funcional

Preferred Background

Experience in functional programming

Bibliografía/Bibliography

Introducción a la computación cuántica

Rolando Somma

Google, Estados Unidos

Horario:

Idioma: Español

Breve resumen de la materia

El objetivo del curso es la formación de estudiantes avanzados y graduados del ámbito de computación y ciencias informáticas en temas relacionados al área de la computación cuántica. Este campo se dedica al estudio de problemas que pueden ser resueltos con computadoras que utilizan los efectos físicos cuánticos en forma mucho más rápida que las computadoras clásicas o convencionales. 

El curso será una introducción al tema, con énfasis en los modelos de computación cuántica y algoritmos cuánticos. También se discutirán posibles realizaciones físicas para las computadoras cuánticas y técnicas de corrección de errores cuánticos.

Objetivos del curso

El objetivo del curso es la formación de estudiantes avanzados y graduados del ámbito de computación y ciencias informáticas en temas relacionados al área de la computación cuántica. Este campo se dedica al estudio de problemas que pueden ser resueltos con computadoras que utilizan los efectos físicos cuánticos en forma mucho más rápida que las computadoras clásicas o convencionales.

Programa

  1. Introducción a la física cuántica y a la teoría computación cuánticaFísica cuántica: breve repaso y postulados
    1. Álgebra lineal y notación de Dirac
    2. Bits cuánticos, compuertas cuánticas y mediciones
    3. Modelos de computación cuántica
    4. Circuitos cuánticos
    5. Complejidad
  2. Algoritmos cuánticos y clases de complejidad
    1. Algoritmo de Deutsch-Josza
    2. Transformada de Fourier cuántica
    3. Algoritmos para la estimación de autovalores
    4. Algoritmo de Shor
    5. Algoritmo de Grover y amplificación de amplitudes
    6. Caminata cuántica
    7. Algoritmos para álgebra lineal
    8. Clases de complejidad: BQP
  3. Simulación de sistemas cuánticos
    1. Problema de simular la dinámica de sistemas cuánticos
    2. Fórmulas producto
    3. Métodos basados en la serie de Taylor
    4. Métodos basados en la transformada cuántica de valores singulares
    5. Aplicaciones
  4. Teoría de corrección de errores cuánticos
    1. Teoría de corrección de errores clásicos
    2. Modelos de errores cuánticos
    3. Códigos estabilizadores
    4. Computación cuántica tolerante a fallos
  5. Realizaciones físicas y experimentos de supremacía cuántica
    1. Trampas de iones
    2. Qubits superconductores
    3. NISQ: Experimentos de simulación cuántica
    4. Supremacía cuántica: Circuitos aleatorios

Prerrequisitos

Nociones elementales previas de álgebra lineal y la física cuántica son deseables aunque no necesarias para seguir el curso, ya que se introducirán los conceptos requeridos gradualmente. El curso es autocontenido.

Bibliografía

Quantum computation and quantum information, M. Nielsen and I. Chuang, Cambridge University Press (2000).

Classical and quantum computation, AY Kitaev, AH Shen, MN Vyalvi, Graduate studies in Mathematics 47, American Mathematical Society, R.I. (2002)

An introduction to quantum computing, P Kaye, R Laflamme, M Mosca, Oxford University Press (2007)

Building quantum computers: A practical introduction, S Majidy, C Wilson, R Laflamme, Cambridge University Press (2024).

Análisis Probabilístico de Algoritmos

Pablo Rotondo

Université Gustave Eiffel, Francia

Horario:

Idioma: Español

Breve resumen de la materia

Este curso introductorio está diseñado para estudiantes avanzados de licenciatura en Informática. Su objetivo es explorar el análisis probabilístico de algoritmos y la combinatoria analítica, áreas esenciales en el diseño y análisis de algoritmos y estructuras de datos eficientes.

El análisis probabilístico de algoritmos ha permitido modelar el rendimiento y el comportamiento de algoritmos en situaciones realistas, donde las entradas son aleatorias o extremadamente complicadas. Iniciado por Donald Knuth, este enfoque ha tenido un profundo impacto en la Informática, explicando el comportamiento eficaz de ciertos algoritmos fundamentales, como Quicksort, tablas de hash y arrays dinámicos, al revelar cómo la naturaleza de los datos puede influir en el desempeño. La combinatoria analítica, desarrollada en gran medida por Philippe Flajolet, ha proporcionado herramientas matemáticas precisas para analizar sistemáticamente estructuras combinatorias y algoritmos mediante técnicas de funciones generatrices y análisis complejo.

Este curso ofrece una introducción al análisis probabilístico de algoritmos y a la combinatoria analítica. A lo largo de cinco clases, se cubrirán tres módulos principales: primero, los métodos probabilísticos que permiten modelar el rendimiento promedio de algoritmos clásicos, además de su aplicación en temas recientes como la predicción de Branching, modelando en parte el comportamiento del procesador. En el segundo módulo, los estudiantes descubrirán las técnicas de la combinatoria analítica para describir sistemáticamente y con precisión el comportamiento asintóticamente de estructuras y algoritmos, mediante el uso de funciones generatrices y análisis complejo. Finalmente, el tercer módulo abordará métodos avanzados para la generación aleatoria de estructuras combinatorias, con especial énfasis en los Boltzmann Samplers. El curso combina teoría y aplicaciones prácticas, con un enfoque en aplicaciones reales que demuestran el impacto de estos métodos en la informática moderna.

Objetivos del curso

  • Introducir los métodos probabilísticos y su aplicación en el estudio de algoritmos.
  • Comprender la influencia clave del modelo de los datos de entrada, así como otros relacionados al procesador, sobre el rendimiento de un algoritmo.
  • Descubrir los métodos de combinatoria analítica y sus aplicaciones en algoritmos y estructuras de datos.
  • Aplicar estos métodos en problemas tanto clásicos como recientes, en particular a la generación aleatoria de estructuras combinatorias.

Programa

Tema 1: Métodos Probabilísticos en Algoritmos

  1. Repaso y Fundamentos de Probabilidad en Algoritmos
  2. Modelos de Entrada Realistas y Aplicaciones Modernas

Tema 2: Combinatoria Analítica y Aplicaciones

  1. Introducción a la Combinatoria Analítica
  2. Aplicaciones Clásicas y Modernas

Tema 3: Generación Aleatoria de Estructuras Combinatorias

  1. Métodos clásicos: generación rescursiva, cadenas de Markov
  2. Boltzmann Samplers y Generación Aleatoria de Tamaño Controlado

Prerrequisitos

Los estudiantes deberán tener conocimientos básicos en algorítmica, probabilidad y matemática discreta.

Bibliografía

  1. Martínez C., Nebel M. y Wild S.: Analysis of branch misses in quicksort.
  2. Martínez C., Nicaud C. y Rotondo P.: A probabilistic model revealing shortcomings in Lua’s hybrid tables.
  3. Flajolet, P. y Sedgewick, R.: Analytic Combinatorics.
  4. Duchon, P., Flajolet, P., Louchard G. y Schaeffer G.: Boltzmann samplers for the random generation of combinatorial structures.
  5. Auger, N., Nicaud, C., y Pivoteau, C.: Good predictions are worth a few comparisons.
  6. Knuth, D. E.: The Art of Computer Programming.

The Evolution of Blockchain Technologies

La evolución de las tecnologías de blockchain

Andrea Vitaletti

University of Rome “La Sapienza”, Italia

Horario:

Idioma: Inglés

Breve resumen de la materia

El paradigma dominante para ofrecer servicios a través de Internet es el modelo Cliente/Servidor. A pesar de ser muy efectivo, presenta algunos problemas, entre los cuales se incluyen un único punto de falla, la falta de resistencia a la censura y la dependencia de terceros de confianza. El modelo P2P (Peer-to-Peer) ha surgido en el pasado como una alternativa para abordar estos problemas. En octubre de 2008, Satoshi Nakamoto escribió el whitepaper sobre Bitcoin, la primera criptomoneda descentralizada. Los nodos en la red P2P de Bitcoin verifican las transacciones mediante criptografía y las registran en un libro mayor público y distribuido, llamado blockchain, sin supervisión central. El consenso entre los nodos se logra mediante un proceso computacionalmente intensivo basado en la prueba de trabajo, conocido como minería, que asegura la blockchain de Bitcoin.

Desde entonces, la tecnología Blockchain ha evolucionado para soportar cómputo general más allá de las criptomonedas (es decir, contratos inteligentes) y actualmente está surgiendo el concepto de Web3.0, es decir, una Web descentralizada. A pesar de la impresionante tecnología y la promesa de impactar muchos aspectos de nuestra vida, las Tecnologías de Registros Distribuidos aún deben demostrar su impacto más allá de las criptomonedas.

El curso se basa en la experiencia adquirida durante varios años de enseñanza de Tecnologías Blockchain en la Universidad Sapienza de Roma.

Abstract

The dominant paradigm for providing services over the Internet is Client/Server. Despite being very effective, it suffers from some problems, among them being a single point of failure, being not censorresistant, and relying on trusted third-parties. P2P has emerged in the past as an alternative approach to deal with those problems. In October 2008, Sathosi Nakamoto, wrote the whitepaper on Bitcoin, the first decentralized cryptocurrency. Nodes in the peer-to-peer bitcoin network verify transactions through cryptography and record them in a public distributed ledger, called a blockchain, without central oversight. Consensus between nodes is achieved using a computationally intensive process based on proof of work, called mining, that secures the bitcoin blockchain.

Since that time, the Blockchain technology evolved to support general computation beyond the cryptocurrency (i.e. smart contracts) and nowadays the concept of Web3.0, namely a decentralized Web is emerging. Despite the beautiful technology and the promise to impact in many aspects of our life, Distributed Ledger Technologies still have to demonstrate their impact beyond cryptocurrency.

The course is based on the experience made in some years of teaching Blockchain Technologies at Sapienza University of Rome.

Objetivos del curso

El curso sobre la evolución de las Tecnologías Blockchain está diseñado para proporcionar una comprensión inicial de los principales conceptos más allá de la Blockchain, el desarrollo de contratos inteligentes y aplicaciones descentralizadas (dApps).

Al finalizar el curso, los asistentes deberían ser capaces de diseñar y desarrollar una aplicación descentralizada simple que interactúe con un contrato inteligente escrito en Solidity. Los asistentes deberán ser capaces de comprender claramente los pros y los contras del desarrollo de tales aplicaciones e identificar los casos de uso en los que la Blockchain puede ser, de hecho, un factor decisivo.

Objectives of the Course

The course on the evolution fo Blockchain Technologies is designed to give a first understanding of the main concepts beyond the Blockchain, the development of smart contracts and Decentralized applications (dApps).

At the end of the course, attendees should be able to design and develop a simple Decentralized Application interacting with a Smart Contract written in Solidity. Attendees should be able to clearly understand the pros and cons of developing such applications and to identify the use cases where the Blockchain can be indeed a game changer.

Programa

  • Introducción a las Tecnologías de Registros Distribuidos (DLT). Redes distribuidas fomentando una gobernanza descentralizada. La evolución de DLT desde las transacciones, pasando por los contratos inteligentes, hasta llegar a las aplicaciones descentralizadas (dApps). Tipos de Blockchain. 
  • Ingredientes técnicos de la Blockchain: Fundamentos de los elementos criptográficos. Funciones hash y árboles de Merkle. Redes distribuidas. Estructura de datos de Blockchain. Consenso. 
  • La evolución del Consenso: El problema de los generales bizantinos. Prueba de trabajo (Proof of Work). Prueba de participación (Proof of Stake). Prueba de participación pura (Pure Proof of Stake). El Trilema de la Blockchain: seguridad, escalabilidad y descentralización. 
  • Contratos inteligentes: De las transacciones a las máquinas de estado. Contratos inteligentes. Ethereum. Fundamentos de programación en Solidity. 
  • Aplicaciones descentralizadas (dApps): De la Web 2.0 a la Web 3.0. La estructura básica de una dApp y su integración con los contratos inteligentes.

Brief Index

  • Introduction to Distributed Ledger Technologies. Distributed networking fostering a decentralized governance. The evolution of DLT from transactions, to smart contracts and finally to Decentralized applications (dApps). Types of Blockchain.
  • Blockchain Technical Ingredients: Basics of crypto ingredients. Hash functions and Merkle Trees. Distributed Networks. Blockchain data structure. Consensus
  • The evolution of Consensus: Byzantine Generals Problem. Proof of Work. Proof of Stake. Pure Proof of Stake. The Blockchain Trilemma: security, scalability, and decentralization.
  • Smart Contracts: From transactions to state machines. Smart Contracts. Ethereum. Basics of coding in Solidity.
  • Decentralized applications (dApps): From Web 2.0 to Web 3.0. The skeleton of a dApps and the integration with the smart contracts.

Prerrequisitos

No se requiere ningún conocimiento específico, aun cuando algún conocimiento básico acerca de redes informáticas y criptografía podría ser útil.

Preferred Background

No specific background is needed, even if a basic knowledge of networking and cryptography can help.

Bibliografía

  • Mastering Bitcoin. Programming the Open Blockchain By Andreas M. Antonopoulos, David A. Harding 2023 https://github.com/bitcoinbook/bitcoinbook
  • Mastering Ethereum: Building Smart Contracts and DApps. by Andreas Antonopoulos, Gavin Wood Ph.D. https://github.com/ethereumbook/ethereumbook
  • Hussein, Z., Salama, M.A. & El-Rahman, S.A. Evolution of blockchain consensus algorithms: a review on the latest milestones of blockchain consensus algorithms. Cybersecurity 6, 30 (2023). https://doi.org/10.1186/s42400-023-00163-y
  • Foundations of Distributed Consensus and Blockchains by Elaine Shi http://elaineshi.com/docs/blockchain-book.pdf
  • Bitcoin: A Peer-to-Peer Electronic Cash System https://bitcoin.org/bitcoin.pdf

Introduction to Column Generation and VRPSolver

Introducción a la Generación de Columnas y el VRPSolver

Teobaldo Bulhões

Universidade Federal da Paraíba, Brasil

Horario:

Idioma: Inglés

Breve resumen de la materia

Muchos problemas de optimización del mundo real pueden modelarse utilizando programación lineal entera y resolverse con paquetes de optimización disponibles en varios lenguajes de programación. Sin embargo, para ciertos problemas, especialmente en logística de transporte, los modelos más eficientes tienen un número exponencial de variables y no pueden resolverse de manera eficiente con paquetes tradicionales. En estos casos, se emplean técnicas de generación de columnas para manejar las variables de manera implícita. Este curso ofrece una introducción a esta técnica y a VRPSolver, un solver moderno que permite a los usuarios construir y resolver modelos con un gran número de variables en tan solo unas pocas líneas de código utilizando el lenguaje de programación Julia.

Abstract

Many real-world optimization problems can be modeled using integer linear programming and solved with optimization packages available in several programming languages. However, for certain problems, especially in transportation logistics, the most efficient models have an exponential number of variables and cannot be solved efficiently with traditional packages. In these cases, column generation techniques are employed to handle the variables implicitly. This course offers an introduction to this technique and to VRPSolver, a modern solver that allows users to build and solve models with a large number of variables in just a few lines of code using the Julia programming language.

Objetivos del curso

  • Introducir la técnica de generación de columnas
  • Demostrar ejemplos de modelos que pueden resolverse de manera eficiente mediante esta técnica
  • Presentar un paquete de optimización moderno que proporciona acceso transparente a la técnica para los usuarios.

Objectives of the Course

  • To introduce the column generation technique
  • To demonstrate examples of models that can be efficiently solved by the technique
  • To present a modern optimization package that provides transparent access to the technique for users.

Programa

  • Modelado matemático con programación lineal entera y el método de branch and bound. 
  • Método simplex revisado y dualidad de la programación lineal. 
  • Generación de columnas y descomposición de Dantzig-Wolfe para problemas de programación lineal.  
  • Introducción a VRPSolver y ejemplos de VRPSolver.

Brief Index

  • Mathematical modeling with integer linear programming and the branch-and-bound method.
  • Revised simplex method and linear programming duality.
  • Column generation and Dantzig-Wolfe decomposition for linear programming.
  • Introduction to VRPSolver and VRPSolver examples

Prerrequisitos

Programación Lineal, Método Simplex, Modelado con Programación Lineal Entera

Preferred Background

Linear Programming, Simplex, Modeling with Integer Linear Programming

Bibliografía

  • Uchoa, E., Pessoa, A., Moreno, L. Optimizing with Column Generation: Advanced Branch-Cut-and-Price Algorithms (Part I). Cadernos do LOGIS-UFF, Universidade Federal Fluminense, Engenharia de Produção, Report No. L-2024-3 (2024). Available at https://optimizingwithcolumngeneration.github.io
  • Pessoa, A., Sadykov, R., Uchoa, Vanderbeck, F. A generic exact solver for vehicle routing and related problems. Mathematical Programming, 183, 483–523 (2020). https://doi.org/10.1007/s10107-020-01523-z
  • Hillier, F. S., Lieberman, G. J. Introduction to Operations Research (11th ed.). New York: McGraw-Hill Education, 2021.

AI for Immersive Technologies: Enhancing Virtual and Augmented Realities

IA para tecnologías inmersivas: mejorando la realidades virtual y aumentada

Francesco Strada

Politecnico di Torino, Italia

Horario:

Idioma: Inglés

Breve resumen de la materia

A medida que la inteligencia artificial (IA) transforma las industrias a nivel mundial, su integración con las tecnologías de realidad virtual (VR) y realidad aumentada (AR) abre nuevas posibilidades para experiencias inmersivas. Las aplicaciones de VR/AR impulsadas por IA ofrecen niveles sin precedentes de compromiso, realismo y adaptabilidad en áreas como la educación, la salud y el entretenimiento. Este curso ofrece una introducción profunda a la poderosa intersección de la IA con VR y AR, proporcionando a los participantes perspectivas sobre el vasto potencial y los desafíos emergentes en este dinámico campo.

Comenzando con los conceptos fundamentales, el curso explora cómo la IA habilita entornos inmersivos, abordando tanto el potencial como las complejidades de VR y AR. A través de conferencias interactivas, estudios de caso y ejemplos prácticos, los participantes aprenderán cómo la IA transforma las experiencias VR/AR al mejorar el realismo, la capacidad de respuesta, la personalización y la interactividad. Los temas clave incluyen el papel de la IA en la creación de entornos adaptables e inteligentes que soportan la capacidad de respuesta contextual y contenido dinámico dirigido por el usuario. Al finalizar el curso, los participantes sintetizarán su aprendizaje en una tarea final, diseñando una experiencia conceptual de VR/AR, demostrando su comprensión de los principios fundamentales de la IA y las estrategias de aplicación en tecnologías inmersivas.

Abstract

As AI reshapes industries worldwide, its integration with virtual (VR) and augmented reality (AR) technologies unlocks new possibilities for immersive experiences. AI-driven VR/AR applications offer unprecedented levels of engagement, realism, and adaptability in education, healthcare, and entertainment. This course provides an in-depth introduction to the powerful intersection of AI with VR and AR, equipping participants with insights into the vast potential and emerging challenges in this dynamic field. 

Beginning with foundational concepts, the course explores how AI enables immersive environments, addressing both the potential and complexities of VR and AR. Through interactive lectures, case studies, and practical examples, participants will learn how AI transforms VR/AR experiences by enhancing realism, responsiveness, personalization, and interactivity. Key topics include AI’s role in creating adaptable, intelligent environments that support context-aware responsiveness and dynamic, user-driven content. By the course’s end, participants will synthesize their learning in a take-home assignment to design a conceptual VR/AR experience, demonstrating their grasp of core AI principles and application strategies in immersive technologies.

Objetivos del curso

El objetivo principal de este curso es proporcionar a los participantes las habilidades y conocimientos necesarios para proponer y diseñar aplicaciones de VR/AR mejoradas con IA. El curso comienza estableciendo una base sólida en los conceptos de VR y AR para lograr esto, ayudando a los participantes a comprender los desafíos y oportunidades que presentan estas tecnologías inmersivas. Sobre esta base, los participantes explorarán cómo la IA transforma los entornos VR/AR, habilitando experiencias adaptativas e interactivas mediante técnicas avanzadas como la generación de contenido, el procesamiento de lenguaje natural en tiempo real, el reconocimiento de emociones y el análisis del comportamiento del usuario. El curso también analizará diversas aplicaciones de la IA dentro de VR/AR, incluidos entornos adaptativos, humanos virtuales e interactividad impulsada por IA, fomentando que los participantes consideren el papel de la IA en la creación de experiencias de usuario inmersivas y atractivas. A través de estudios de caso, obtendrán una visión de experiencias innovadoras de VR/AR y el impacto práctico de la IA en la creación de contenido y el diseño inmersivo. Finalmente, el curso integrará consideraciones éticas, haciendo hincapié en el desarrollo responsable de aplicaciones de VR/AR mejoradas con IA y preparando a los participantes para abordar las necesidades de los usuarios y las dimensiones éticas en sus diseños.

Objectives of the Course

The primary objective of this course is to equip participants with the skills and knowledge needed to propose and design AI-enhanced VR/AR applications. The course begins by establishing a solid foundation in VR and AR concepts to achieve this, helping participants understand the challenges and opportunities these immersive technologies present. Building on this foundation, participants will explore how AI transforms VR/AR environments, enabling adaptive and interactive experiences through advanced techniques such as content generation, real-time natural language processing, emotion recognition, and user behavior analysis. The course will also analyze diverse AI applications within VR/AR, including adaptive environments, virtual humans, and AI-driven interactivity, encouraging participants to consider AI’s role in creating immersive, engaging user experiences. Through case studies, they will gain insight into innovative VR/AR experiences and the practical impact of AI in content creation and immersive design. Finally, the course will integrate ethical considerations, emphasizing the responsible development of AI-enhanced VR/AR applications and preparing participants to address user needs and ethical dimensions in their designs.

Programa

Introducción a las Tecnologías Inmersivas 

  1. Visión general de VR, AR, MR (Realidad Mixta) y XR (Realidad Extendida)
  2. Aplicaciones clave y tendencias industriales en VR/AR en diversos sectores (por ejemplo, educación, salud, entretenimiento)
  3. Desafíos y oportunidades en el desarrollo de tecnologías inmersivas 

Fundamentos de la Inteligencia Artificial 

  1. Breve introducción a los principios de la IA relevantes para VR/AR
  2. Visión general de la interactividad impulsada por IA: procesamiento de lenguaje natural, visión por computadora y aprendizaje automático en entornos inmersivos 

El Papel de la IA en la Mejora de los Entornos Inmersivos

  1. Creación de entornos VR/AR adaptativos y responsivos
  2. IA contextual para una respuesta en tiempo real
  3. Estudio de caso: aplicaciones VR/AR mejoradas con IA que muestran entornos adaptativos 

Generación de Contenido e IA en VR/AR

  1. Generación procedural de modelos 3D, texturas y entornos interactivos
  2. Herramientas de IA para automatizar la creación de contenido en VR/AR
  3. Ejemplos prácticos de flujos de trabajo para la creación de contenido en VR/AR 

Humanos Virtuales e Interacción Humano-Computadora

  1. El papel de los humanos virtuales en la simulación de interacciones y comportamientos realistas
  2. Técnicas de IA en procesamiento de lenguaje natural, reconocimiento de gestos y reconocimiento de emociones 
  3. Estudios de caso: humanos virtuales en VR social, simulaciones de entrenamiento y servicio al cliente 

Personalización y Diseño Centrado en el Usuario en VR/AR

  1. Personalización impulsada por IA: perfiles de usuario, contenido adaptativo y experiencias personalizadas
  2. Mejora del compromiso del usuario a través de retroalimentación y interacciones personalizadas impulsadas por IA
  3. Ética de la personalización: preocupaciones sobre privacidad y consideraciones de datos 

Ética e Implicaciones Sociales de la IA en VR/AR

  1. Equilibrando la innovación con la responsabilidad ética
  2. Abordando la privacidad, autenticidad e impacto social de las tecnologías inmersivas
  3. Discusión: Directrices éticas para el desarrollo responsable en VR/AR 

Futuras Direcciones en VR/AR Mejorado por IA

  1. Tendencias emergentes y tecnologías en IA y tecnologías inmersivas
  2. Especulando sobre aplicaciones futuras y el rol en evolución de la IA en VR/AR
  3. Preparación para el aprendizaje y desarrollo continuos en el campo Preparación y 

Orientación para el Proyecto Final

  1. Visión general de la tarea final
  2. Pasos para diseñar un esquema de experiencia VR/AR, con enfoque en las necesidades del usuario y características de IA
  3. Sesión de preguntas y respuestas y retroalimentación para apoyar el desarrollo del proyecto

Brief Index

Introduction to Immersive Technologies

  1. Overview of VR, AR, MR (Mixed Reality), and XR (Extended Reality)
  2. Key applications and industry trends in VR/AR across sectors (e.g., education, healthcare, entertainment)
  3. Challenges and opportunities in immersive technology development

Fundamentals of Artificial Intelligence

  1. Brief introduction to AI principles relevant to VR/AR
  2. Overview of AI-driven interactivity: natural language processing, computer vision, and machine learning in immersive settings

AI’s Role in Enhancing Immersive Environments

  1. Creating adaptive and responsive VR/AR environments
  2. Context-aware AI for real-time responsiveness
  3. Case study: AI-enhanced VR/AR applications that showcase adaptive environments

Content Generation and AI in VR/AR

  1. Procedural generation of 3D models, textures, and interactive environments
  2. AI tools for automating content creation in VR/AR
  3. Practical examples of content creation workflows in VR/AR

Virtual Humans and Human-Computer Interaction

  1. Role of virtual humans in simulating realistic interactions and behaviors
  2. AI techniques in natural language processing, gesture recognition, and emotion recognition
  3. Case studies: Virtual humans in social VR, training simulations, and customer service

Personalization and User-Centric Design in VR/AR

  1. AI-driven personalization: user profiling, adaptive content, and custom experiences
  2. Enhancing user engagement through tailored, AI-driven feedback and interactions
  3. Ethics of personalization: privacy concerns and data considerations

Ethics and Societal Implications of AI in VR/AR

  1. Balancing innovation with ethical responsibility
  2. Addressing privacy, authenticity, and the social impact of immersive technologies
  3. Discussion: Ethical guidelines for responsible development in VR/AR

Future Directions in AI-Enhanced VR/AR

  1. Emerging trends and technologies in AI and immersive tech
  2. Speculating on future applications and the evolving role of AI in VR/AR
  3. Preparing for continued learning and development in the field

Capstone Project Preparation and Guidance

  1. Overview of the take-home assignment
  2. Steps for designing a VR/AR experience outline, with a focus on user needs and AI features
  3. Q&A and feedback session to support project development

 

Prerrequisitos

El curso está destinado a estudiantes con formación en Ciencias de la Computación. Además, contar con conocimientos fundamentales en IA o Aprendizaje Automático (por ejemplo, cursos introductorios de Inteligencia Artificial o Aprendizaje Automático) y/o familiaridad con la Interacción Humano-Computadora o Medios Digitales (por ejemplo, cursos en HCI o Medios Interactivos) mejorará la comprensión y el compromiso con el material.

Preferred Background

The course is intended for students with a Computer Science background. Additionally, foundational knowledge in AI or Machine Learning (e.g., introductory courses in Artificial Intelligence or Machine Learning) and/or familiarity with Human-Computer Interaction or Digital Media (e.g., courses in HCI or Interactive Media) will further enhance understanding and engagement with the material.

Bibliografía

  • Hirzle, T., Müller, F., Draxler, F., Schmitz, M., Knierim, P. and Hornbæk, K., 2023, April. When XR and AI meet-a scoping review on extended reality and artificial intelligence. In Proceedings of the 2023 CHI Conference on Human Factors in Computing Systems (pp. 1-45).
  • Liberatore, M.J. and Wagner, W.P., 2021. Virtual, mixed, and augmented reality: a systematic review for immersive systems research. Virtual Reality, 25(3), pp.773-799.
  • Ribeiro de Oliveira, Tainã, Brenda Biancardi Rodrigues, Matheus Moura da Silva, Rafael Antonio N. Spinassé, Gabriel Giesen Ludke, Mateus Ruy Soares Gaudio, Guilherme Iglesias Rocha Gomes et al. «Virtual reality solutions employing artificial intelligence methods: A systematic literature review.» ACM Computing Surveys 55, no. 10 (2023): 1-29.
  • Soliman, M.M., Ahmed, E., Darwish, A. and Hassanien, A.E., 2024. Artificial intelligence powered Metaverse: analysis, challenges and future perspectives. Artificial Intelligence Review, 57(2), p.36.
  • Suzuki, R., Gonzalez-Franco, M., Sra, M. and Lindlbauer, D., 2023, October. XR and ai: AI-enabled virtual, augmented, and mixed reality. In Adjunct Proceedings of the 36th Annual ACM Symposium on User Interface Software and Technology (pp. 1-3).
  • Xu, X., Yu, A., Jonker, T.R., Todi, K., Lu, F., Qian, X., Evangelista Belo, J.M., Wang, T., Li, M., Mun, A. and Wu, T.Y., 2023, April. Xair: A framework of explainable ai in augmented reality. In Proceedings of the 2023 CHI Conference on Human Factors in Computing Systems (pp. 1-30).

De la planificación no determinista a la síntesis y planificación generalizada

From Non-deterministic Planning to Synthesis and Generalized Planning

Sebastián Sardina

RMIT Universtiy, Australia

Horario:

Idioma: Español

Breve resumen de la materia

En este curso, analizaremos una elaborada pero muy significativa extensión del modelo clásico de planificación en IA, a saber, la planificación Totalmente Observable No Determinista (FOND, por sus siglas en inglés), y su relación con otros problemas importantes como la síntesis reactiva y las formas generalizadas de planificación. 

La planificación en IA es un enfoque para el comportamiento autónomo, donde el comportamiento del agente se deriva automáticamente a partir de un modelo simbólico. En la planificación FOND, las acciones pueden ser no deterministas, es decir, pueden tener un conjunto finito de efectos posibles que son conocidos a priori, pero cuya realización real se observa después de su ejecución. Por ejemplo, un robot que agarra un vaso puede resultar en que el agarre sea exitoso o que el vaso permanezca en la mesa. Aunque es una simple extensión de la planificación clásica, el marco de trabajo FOND ha surgido como un paradigma computacional altamente versátil que puede usarse para resolver otros tipos de problemas desafiantes.

Es importante señalar que se ha demostrado una fuerte conexión entre la planificación FOND y la síntesis reactiva a partir de especificaciones lógicas, lo que vincula la IA con los métodos formales. El curso introducirá el problema de planificación FOND desde cero, así como las técnicas algorítmicas y los solvers de última generación desarrollados hasta ahora, antes de abordar su importancia en la planificación generalizada y la síntesis en Ciencias de la Computación.

Objetivos del curso

El curso tiene como objetivo proporcionar a estudiantes avanzados de pregrado y posgrado (Maestría y Doctorado) una visión general de un área activa de investigación en Planificación en IA, que también tiene vínculos con otras áreas fundamentales de la Ciencia de la Computación, como métodos formales y verificación en Ingeniería de Software, teoría de la computación y control.

Al finalizar este curso, se espera que el estudiante comprenda: 

  1. La planificación automatizada como subcampo de la IA, su rol histórico en el estado actual y el panorama de trabajo. 
  2. Planificación con acciones no deterministas: por qué los planes lineales simples ya no son suficientes y cómo se necesitan representaciones más expresivas del comportamiento de los agentes (incluidos los planes con bucles). 
  3. Las principales técnicas algorítmicas para encontrar soluciones a problemas FOND, incluyendo búsqueda heurística, técnicas basadas en SAT y enfoques basados en verificación de modelos. 
  4. La relación entre la planificación bajo no determinismo y la síntesis reactiva en métodos formales. 
  5. Cómo la planificación FOND puede utilizarse para resolver formas generalizadas de planificación, como la planificación LTL (Lógica Temporal Lineal) o la Planificación Numérica Cualitativa.

Programa

  • Planificación clásica para la toma de decisiones secuenciales. 
  • Acciones no deterministas en la planificación automatizada. 
  • Conceptos de solución en la planificación FOND: soluciones débiles, fuertes, y fuertemente cíclicas. 
  • Supuestos de equidad. 
  • Solvers para la planificación FOND: búsqueda heurística, SAT, verificación de modelos.
  • Juegos de dos jugadores y síntesis de controladores – relación con la planificación FOND.
  • Planificación generalizada, planificación numérica cualitativa y programas de planificación de agentes.

Prerrequisitos

  • Matematica discreta (conjuntos; grafos y árboles; lógica básica).
  • Algoritmos (e.g., recorrido de árboles; programación dinámica; notación O).
  • Mejor pero no obligatorio: conocimientos introductorios de IA, teoría de autómatas.

Bibliografía

  1. Geffner, H., & Bonet, B. (2013). A Concise Introduction to Models and Methods for Automated Planning. Morgan-Claypool.
  2. Ghallab, M., Nau, D., Traverso P.: Automated planning – theory and practice. Elsevier 2004.
  3. Daniele, M., Traverso, P., & Vardi, M. Y. (1999). Strong cyclic planning revisited. In Proceedings of the European Conference on Planning (ECP) , Vol. 1809 of LNCS, pp. 35–48. Springer.
  4. Cimatti, A., Pistore, M., Roveri, M., & Traverso, P. (2003). Weak, strong, and strong cyclic planning via symbolic model checking. Artificial Intelligence, 147(1-2), 35–84.
  5. Muise, C., McIlraith, S. A., & Beck, J. C. (2012). Improved non-deterministic planning by exploiting state relevance. In Proc. of the Int. Conf. on Automated Planning and Scheduling (ICAPS), 172–180
  6. Sebastian Sardiña, Nicolás D’Ippolito: Towards Fully Observable Non-Deterministic Planning as Assumption-based Automatic Synthesis. IJCAI 2015: 3200-3206
  7. Camacho, A., Bienvenu, M., & McIlraith, S. A. (2019). Towards a unified view of AI planning and reactive synthesis. In Proc. of the National Conference on Artificial Intelligence (AAAI), pp. 58–67.
  8. Giuseppe De Giacomo, Alfonso Gerevini, Fabio Patrizi, Alessandro Saetti, and Sebastian Sardina (2016). Agent planning programs. Artificial Intelligence, 231:64–106.
  9. Ivan D. Rodriguez, Blai Bonet, Sebastian Sardiña, Hector Geffner: Flexible FOND Planning with Explicit Fairness Assumptions. Journal of Artificial Intelligence Research 74 (2022)
  10. Bonet, B., & Geffner, H. (2020). Qualitative Numeric Planning: Reductions and complexity. Journal of Artificial Intelligence Research (JAIR), 69, 923–961.
  11. Srivastava, S., Immerman, N., & Zilberstein, S. (2011a). A new representation and associated algorithms for generalized planning. Artificial Intelligence, 175(2), 615–647.

Modelos generativos de imágenes basados en redes profundas

Pablo Musé

Universidad de la República, Uruguay

Horario:

Idioma: Español

Breve resumen de la materia

Este curso explora las técnicas y modelos más avanzados de inteligencia artificial utilizados para generar muestras realistas a partir de un conjunto de datos. Estos modelos aprenden la distribución subyacente de los datos, de forma explícita o implícita, y generan nuevas muestras de acuerdo a esta distribución. La parametrización de los modelos generativos mediante redes neuronales profundas ha permitido aprender estas distribuciones para datos en espacio de muy alta dimensión, dando lugar a métodos capaces de sintetizar muestras realistas de datos complejos como imágenes, audio y texto. Hoy en día, modelos generativos como los modelos de difusión, han transformado la creación visual al permitir que las máquinas generen imágenes, desde arte hasta retratos foto-realistas, sin intervención humana directa. Estos avances están redefiniendo industrias como el diseño gráfico, la moda, los videojuegos, la medicina, y la publicidad.

En este curso estudiaremos los fundamentos de los modelos generativos profundos y su entrenamiento mediante técnicas de optimización estocástica. Trabajaremos sobre los modelos autorregresivos, los auto-encoders variacionales, los normalizing flows, los modelos de difusión y las redes generativas antagónicas. Presentaremos también algunas aplicaciones a problemas de visión por computadora y restauración de imágenes.

Objetivos del curso

  • Desarrollar una comprensión profunda de los fundamentos matemáticos y probabilísticos de los modelos generativos profundos.
  • Entender las diferencias, las ventajas y las limitaciones de los distintos modelos generativos profundos.
  • Entender las dificultades vinculadas al entrenamiento de estos modelos.
  • Diseñar e implementar modelos generativos utilizando frameworks populares como PyTorch.

Programa

  1. Repaso de aprendizaje profundo: redes convolucionales, redes recurrentes.
  2. Modelos generativos autorregresivos: Pixel-RNN, Pixel-CNN, WaveNet.
  3. Auto-encoders y auto-encoders variacionales.
  4. Normalizing flows: RealNVP, Glow.
  5. Modelos de difusión: DDPM, DDIM.
  6. Restauración de imágenes con modelos de difusión: Classifier guidance, DDRM, DPS, PiGDM.

Prerrequisitos

  • Cálculo diferencial e integral, álgebra lineal, probabilidad y estadística (nivel de grado para carreras de ingeniería, computación o licenciatura en matemática).
  • Curso introductorio de aprendizaje automático y/o aprendizaje profundo.
  • Programación en Python.

Bibliografía

  • Bishop, C. M., & Bishop, H. (2023). Deep learning: Foundations and concepts. Springer Nature.
  • Murphy, K. P. (2023). Probabilistic machine learning: Advanced topics. MIT press.
  • Tomczak, J. M. (2024). Deep Generative Modeling. Springer Cham.
  • Dhariwal, P., & Nichol, A. (2021). Diffusion models beat gans on image synthesis. Advances in neural information processing systems, 34, 8780-8794.
  • Kawar, B., Elad, M., Ermon, S., & Song, J. (2022). Denoising diffusion restoration models. Advances in Neural Information Processing Systems, 35, 23593-23606.
  • Chung, H., Kim, J., McCann, M. T., Klasky, M. L., & Ye, J. C. (2023). Diffusion Posterior Sampling for General Noisy Inverse Problems. In The Eleventh International Conference on Learning Representations.
  • Song, J., Vahdat, A., Mardani, M., & Kautz, J. (2023, May). Pseudoinverse-guided diffusion models for inverse problems. In International Conference on Learning Representations.
  • Tailanian, M., Pardo, Á., & Musé, P. (2024). U-flow: A u-shaped normalizing flow for anomaly detection with unsupervised threshold. Journal of Mathematical Imaging and Vision, 1-19.

Procesamiento de imágenes con aplicación a la biomedicina

Federico Lecumberry

Universidad de la República, Uruguay

Horario:

Idioma: Español

Breve resumen de la materia

Procesamiento de imágenes con aplicación a la biomedicina es un curso corto dirigido a investigadores y estudiantes de las áreas de la informática y de ciencias de la vida (carreras en biología, medicina, bioquímica, biología humana, etc.) con conocimientos de programación (preferentemente Python) que se interesen por el procesamiento de imágenes por computadora y las aplicaciones a las bioimágenes.

En el curso se introducen los conceptos principales del procesamiento de imágenes por computadora con especial énfasis en su aplicación de ciencias de la vida como ser imágenes de microscopía o las imágenes médicas. Se abarcan los distintos aspectos de un área muy extensa de manera de dejar claros los conceptos generales subyacentes y abrir la puerta a un estudio más detallado por parte del estudiante.

Objetivos del curso

Al finalizar el curso el estudiante comprenderá los fundamentos del procesamiento de imágenes por computadora, tendrá experiencia en la programación y el uso de software que implementa algoritmos de procesamiento de imágenes y podrá encarar proyectos de aplicación en esta área, en diálogo con personal más experimentado.

Programa

  1. Fundamentos de las bioimágenes. Procesamiento de imágenes: problemas y aplicaciones. Relaciones con disciplinas vecinas. Pasos fundamentales en el procesamiento de imágenes: Esquema general de un sistema de visión por computador.
  2. Representación y visualización de imágenes. Arreglos de datos multidimensionales. Imágenes vectoriales. Discretización espacio-temporal. Cuantificación. Visualización de imágenes 2D, 3D, 3D+t. Formatos de almacenamiento.
  3. Histogramas y operaciones de píxeles. Histogramas, operaciones con histogramas, ecualización de histograma, modificación brillo y contraste, cuantificación, umbralización global y local.
  4. Macros y scripts. Registro y ejecución de secuencias de comandos (macros). Modificación de macros. Comandos de entrada y salida. Ejecución en lotes (batch processing)
  5. Sistemas lineales y filtrado de señales. Filtros lineales, convolución. Filtros no lineales. Filtros en el espacio y en frecuencia. Difusión isotrópica y anisotrópica.
  6. Análisis frecuencial. Teoría de Fourier. Descomposición en senos y cosenos. FFT. Transformada de Fourier. Propiedades. Ancho de banda. Módulo y fase. Teorema de convolución. Filtrado en el espacio y en frecuencia.
  7. Restauración de ruido y degradaciones. Modelo de la degradación: desenfoque, borroneo, ruido. Métodos de restauración. Filtro adaptivo. Filtro inverso. Medidas de desempeño.
  8. Fundamentos del Aprendizaje Automático (AA). Planteo y diagrama de un sistema de AA. Tipos de problemas de AA. Etapas de desarrollo. Medidas de desempeño. Optimización y búsqueda de parámetros. Sobre-ajuste y medidas para evitarlo. Aplicación a la clasificación de píxeles y objetos. Entrenamientos de clasificadores. Medida de desempeño.
  9. Análisis de imágenes a color y textura. Teoría del color. Espacios de representación de color. Texturas estructurales y estadísticas. Métricas para texturas. Conceptos básicos de Aprendizaje Automático para clasificación de texturas.
  10. Seguimiento de objetos y partículas. Seguimiento de objetos (células, spots) en secuencias de imágenes. Planteo del diagrama detección-seguimiento. Métodos de AA en detección.
  11. Análisis de formas. Análisis de objetos detectados en imágenes. Factor de forma. Medidas geométricas Medidas estadísticas.
  12. Buenas prácticas en el uso de imágenes científicas. Aspectos éticos de la aplicación del AA. Consideraciones para las publicaciones científicas con métodos de AA, y la relación con la Inteligencia Artificial.

Prerrequisitos

Conocimientos básicos de Cálculo, Álgebra lineal, Probabilidad, y Programación

Bibliografía

  1. Gonzalez, R. C., & Woods, R. E. (2018). Digital image processing. Pearson.
  2. Burger, Wilhelm, Burge, Mark J. (2011). Principles of Digital Image Processing: Fundamental Techniques. Springer. ISBN: 978-1848001909.
  3. Burger, Wilhelm, Burge, Mark J. (2007). Digital Image Processing: An Algorithmic Introduction using Java. Springer.