Título: El Vínculo entre Entropía Generativa, Autoevaluación y Correctitud en el uso de LLMs para Métodos Formales
Director: Victor Braberman
Jurados: Luciano del Corro y Sebastian Uchitel

Resumen:
Los 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.
Evaluamos 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.
Ademá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.