Resumen:Presentamos una herramienta para la verificación rigurosa y automatizada de políticas basadas en modelos de lenguaje grande (LLM) en tareas de toma de decisiones secuenciales sin memoria. Dado un proceso de decisión de Markov (MDP) que representa la tarea secuencial de toma de decisiones, una política de LLM y un requisito de seguridad expresado como una fórmula PCTL, nuestro enfoque construye incrementalmente solo la parte alcanzable del MDP guiado por las acciones elegidas por el LLM. Cada estado se codifica como un mensaje de lenguaje natural, la respuesta del LLM se analiza en una acción y los estados sucesores alcanzables por la política se expanden. El modelo formal resultante se verifica con Storm para determinar si la política satisface la propiedad de seguridad especificada. En experimentos con puntos de referencia mundiales de grillas estándar, mostramos que los LLM de código abierto a los que se accede a través de Ollama se pueden verificar cuando se siembran de manera determinista, pero generalmente tienen un rendimiento inferior al de las líneas base de aprendizaje por refuerzo profundo. Nuestra herramienta se integra de forma nativa con Ollama y admite tareas especificadas por PRISM, lo que permite una evaluación comparativa continua en tareas secuenciales de toma de decisiones especificadas por el usuario y sienta una base práctica para verificar formalmente LLM cada vez más capaces.
Publicado originalmente en export.arxiv.org el 8 de octubre de 2025.
Ver fuente original
