BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Departamento de Computación - ECPv6.15.18//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Departamento de Computación
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:20250101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/Sao_Paulo:20260515T100000
DTEND;TZID=America/Sao_Paulo:20260515T110000
DTSTAMP:20260516T010740
CREATED:20260508T152534Z
LAST-MODIFIED:20260508T152534Z
UID:10605-1778839200-1778842800@www.dc.uba.ar
SUMMARY:Defensa Tesis Licenciatura Martín Amster
DESCRIPTION:Título: El Vínculo entre Entropía Generativa\, Autoevaluación y Correctitud en el uso de LLMs para Métodos Formales\nDirector: Victor Braberman\nJurados: Luciano del Corro y Sebastian Uchitel \nResumen:\nLos LLMs han demostrado grandes capacidades en la generación de código; sin embargo\, su fiabilidad en tareas de razonamiento formal y verificación sigue siendo un desafío abierto. Este trabajo investiga la relación entre la incertidumbre interna del modelo (cuantificada a través de la entropía semántica) y la correctitud de sus salidas dentro del dominio de los métodos formales.\nEvaluamos este vínculo a través de dos tareas estructuralmente distintas: (1) una tarea de auto-formalización que extrae especificaciones (pre/postcondiciones) y (2) una tarea de síntesis de invariantes de bucle\, verificada formalmente mediante Dafny. Si bien una alta concentración semántica se consolida como un predictor estadísticamente significativo de correctitud en ambos dominios\, nuestros hallazgos revelan una asimetría crucial en la tarea de invariantes\, dado que la baja concentración ya no se correlaciona directamente con la incorrección.\nAdemás\, exploramos las capacidades de autoevaluación del modelo contrastando su desempeño como generador frente a su rol como juez. Los resultados revelan un sesgo de origen: a medida que aumenta la complejidad de la tarea\, el modelo evalúa con mayor fiabilidad sus propias generaciones que las especificaciones correctas escritas por humanos. Finalmente\, analizamos cómo interactúan la concentración semántica y la autoevaluación como variables predictoras conjuntas de la correctitud\, mostrando que ambas señales son complementarias y que su combinación supera el uso de cualquiera de las dos de forma aislada.
URL:https://www.dc.uba.ar/event/defensa-tesis-licenciatura-martin-amster/
LOCATION:Aula 1301
CATEGORIES:Agenda
END:VEVENT
END:VCALENDAR