Resumen: Introducimos un marco novedoso para evaluar la alineación entre los planes de lenguaje natural y su comportamiento esperado convirtiéndolos en estructuras Kripke y lógica temporal lineal (LTL) utilizando modelos de lenguaje grande (LLM) y realizando la verificación del modelo. Evaluamos sistemáticamente este marco en una versión simplificada del conjunto de datos de verificación del plan PlanBench e informamos sobre métricas como exactitud, precisión, recuperación y puntuaciones F1. Nuestros experimentos demuestran que GPT-5 logra un excelente rendimiento de clasificación (puntuación F1 de 96,3%) y casi siempre produce representaciones formales sintácticamente perfectas que pueden actuar como garantías. Sin embargo, la síntesis de modelos formales semánticamente perfectos sigue siendo un área para exploración futura.
Publicado Originalme en export.arxiv.org El 6 de octubre de 2025.
Ver Fuente Original
