BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Departamento de Computación - ECPv6.15.18//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-ORIGINAL-URL:https://www.dc.uba.ar
X-WR-CALDESC:Eventos para Departamento de Computación
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:America/Sao_Paulo
BEGIN:STANDARD
TZOFFSETFROM:-0300
TZOFFSETTO:-0300
TZNAME:-03
DTSTART:20230101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/Sao_Paulo:20241223T150000
DTEND;TZID=America/Sao_Paulo:20241223T160000
DTSTAMP:20260404T174659
CREATED:20241223T132616Z
LAST-MODIFIED:20241223T132616Z
UID:9661-1734966000-1734969600@www.dc.uba.ar
SUMMARY:Defensa Tesis Licenciatura Gabriel Leclercq
DESCRIPTION:Título: Integración de información cognitiva en modelos de lenguaje\n\n\n\nDirector: Bruno Bianchi\n\nCo-Director: Fermín Travi\n\nJurados: Álvaro Cabana\, Leonardo Pepino \nResumen\n\nLos ojos han probado ser una ventana a una gran variedad de procesos cognitivos\, por ejemplo\, relacionados con la atención y la memoria. Ambas son funciones fundamentales del proceso de lectura y comprensión lectora. Por ello\, el estudio de los movimientos de los ojos durante la lectura ha captado la atención de los neurolingüistas por más de un siglo\, estableciendo al seguimiento ocular como una herramienta fundamental para entender el procesamiento del lenguaje en el cerebro.\nEn paralelo\, en el campo del procesamiento del lenguaje natural\, se han desarrollado herramientas para análisis del texto\, principalmente a través de la tarea de predicción de palabras o de extracción de tópicos\, y\, más recientemente\, junto a la generación de texto se han desarrollado modelos capaces de comprender textos para sostener interacciones fluidas con humanos en el desarrollo de tareas generales. El entrenamiento de estos modelos siempre ha sido a partir de textos escritos\, los cuales generalmente fueron editados\, y el modelo los utiliza como insumo de forma lineal y uniforme tal como le fueron presentados. Sin embargo\, si bien la lectura es generalmente lineal\, existen tanto variaciones en los tiempos de lectura de cada palabra como regresiones a secciones del texto anterior. Estas variaciones en la forma de la lectura están asociadas principalmente a la dificultad o ambigüedad del texto leído.\nEl objetivo de la tesis es cambiar el foco de los modelos de la persona que escribe a la que lee\, incorporando información de los movimientos oculares durante el entrenamiento. A partir de datos experimentales recolectados de 76 personas leyendo cuentos cortos\, se procedió a extraer métricas clásicas sobre seguimiento ocular durante la lectura (como\, por ejemplo\, la duración de la mirada sobre una palabra). Esta información se incorporó a un modelo de lenguaje basado en redes LSTM (Long Short-Term Memory) a través de su predicción y de alimentar al modelo con el texto en el mismo orden que fue leído. Al extraer las representaciones vectoriales de las palabras (embeddings)\, se observó que la distancia coseno entre pares de palabras correlacionaron menos con juicios de similitud humanos sobre esos mismos pares de palabras con respecto a un modelo base de referencia (0.12 frente a 0.19\, con una distancia intercuartil de 0.5 para ambos). No obstante\, la adición de información de movimientos oculares mejoró levemente esta correlación frente a no poseer dicha información (0.13 vs 0.12\, con una distancia intercuartil de 0.5 para ambos).\nEl reentrenamiento con texto bajo el orden leído por las personas no proporcionó mejoras frente a su equivalente con el orden original del texto\, posiblemente debido a su pre entrenamiento con texto de Wikipedia. Por otro lado\, la incorporación de información de movimientos oculares pareciera acercar levemente al espacio vectorial de las palabras a los juicios de similitud humanos. Trabajo a futuro incluye distintas maneras de incorporar esta información\, así como la adición de otras métricas\, y la utilización de tareas más extrínsecas para la evaluación. La presente tesis es una prueba de concepto de los avances que se podrían lograr incorporando más información de la persona que lee\, y escalando a modelos más complejos.\n\n\n 
URL:https://www.dc.uba.ar/event/defensa-tesis-licenciatura-gabriel-leclercq/
LOCATION:Sala 2103
CATEGORIES:Agenda
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=America/Sao_Paulo:20241223T180000
DTEND;TZID=America/Sao_Paulo:20241223T190000
DTSTAMP:20260404T174659
CREATED:20241216T130419Z
LAST-MODIFIED:20241223T130121Z
UID:9633-1734976800-1734980400@www.dc.uba.ar
SUMMARY:Defensa Tesis Licenciatura Manuel Panichelli
DESCRIPTION:Título: PPA – Un asistente de demostración para lógica de primer orden con extracción de testigos usando la traducción de Friedman\nDirector: Pablo Barenbaum\nJurado:\n– Verónica Becher\n– Miguel Pagano (FaMAF\, UNC) \nTransmision: https://youtube.com/live/9uIHpGT4EnI \nResumen:\nLos asistentes de demostración son programas que simplifican la escritura de demostraciones matemáticas\, permitiendo la colaboración masiva o la verificación formal de programas.\nExisten muchos asistentes como Mizar\, Coq e Isabelle\, basados en distintas teorías. Un criterio deseable que pueden cumplir es el de De Bruijn: a partir de demostraciones en un lenguaje de alto nivel se pueden extraer demostraciones en un lenguaje núcleo fácilmente verificable. Esto elimina la necesidad de tener que confiar en la implementación del asistente\, ya que las demostraciones pueden ser verificadas por un programa independiente.\nEn esta tesis se presenta PPA\, un asistente de demostración para lógica clásica de primer orden. Cumple con el criterio de De Bruijn\, generando demostraciones en el sistema lógico de deducción natural a partir de programas escritos en un lenguaje de alto nivel\, cuyo objetivo es ser similar a cómo serían en lenguaje natural. Tiene un mecanismo principal de demostración\, el by\, que por debajo cuenta con un solver heurístico para lógica de primer orden que facilita la escritura de demostraciones. Está inspirado en el mecanismo análogo en Mizar.\nAlgunos asistentes implementan la extracción de testigos de existencial. Dada una demostración de ∃x.p(x)\, se extrae un testigo t tal que cumpla p(t). Es sencillo hacerlo sobre lógica intuicionista por su naturaleza constructiva\, pero un desafío sobre lógica clásica\, que no lo es. Para ello hay dos grandes categorías: directas (mediante técnicas semánticas como realizabilidad clásica) o indirectas (mediante traducciones a otra lógica\, como intuicionista).\nEl aporte principal del trabajo es una implementación práctica de la extracción de testigos. PPA la implementa de forma indirecta usando la traducción de Friedman\, que permite convertir demostraciones clásicas de fórmulas Π2 de la forma ∀y0…∀yn.∃x.φ\, con φ sin cuantificadores\, a demostraciones intuicionistas. Se describe cómo una vez traducidas pueden ser normalizadas usando reglas de reducción bien conocidas\, que se corresponden con las reglas de reducción del cálculo-lambda vistas desde el isomorfismo Curry–Howard. Finalmente\, de una demostración normalizada se podrá extraer un testigo. Identificamos algunos detalles en la implementación práctica de la traducción\, que limitan las fórmulas para las cuales se puede usar (más allá de la limitación teórica de Π2) y también limitan las axiomatizaciones de las teorías que se pueden procesar.
URL:https://www.dc.uba.ar/event/defensa-tesis-licenciatura-manuel-panichelli/
LOCATION:Aula 1113
CATEGORIES:Agenda
END:VEVENT
END:VCALENDAR