Resumen:Presentamos Sentinel, el primer marco para evaluar formalmente la seguridad física de agentes incorporados en el modelo de lenguaje grande (LLM) en los niveles semántico, de plan y de trayectoria. A diferencia de los métodos anteriores que se basan en reglas heurísticas o juicios subjetivos de LLM, Sentinel basa los requisitos prácticos de seguridad en la semántica de lógica temporal formal (TL) que puede especificar con precisión invariantes de estado, dependencias temporales y restricciones de tiempo. Luego emplea un proceso de verificación de múltiples niveles donde (i) en el nivel semántico, los requisitos intuitivos de seguridad del lenguaje natural se formalizan en fórmulas TL y se prueba la comprensión del agente LLM de estos requisitos para alinearlos con las fórmulas TL; (ii) a nivel de plan, los planes de acción de alto nivel y los subobjetivos generados por el agente LLM se verifican con las fórmulas TL para detectar planes inseguros antes de su ejecución; y (iii) a nivel de trayectoria, se fusionan múltiples trayectorias de ejecución en un árbol de cálculo y se verifican de manera eficiente con especificaciones TL físicamente detalladas para una verificación final de seguridad. Aplicamos Sentinel en VirtualHome y ALFRED, y evaluamos formalmente múltiples agentes incorporados basados en LLM frente a diversos requisitos de seguridad. Nuestros experimentos muestran que al basar la seguridad física en la lógica temporal y aplicar métodos de verificación en múltiples niveles, Sentinel proporciona una base rigurosa para evaluar sistemáticamente agentes incorporados basados en LLM en entornos físicos, exponiendo violaciones de seguridad pasadas por alto por métodos anteriores y ofreciendo información sobre sus modos de falla.
Publicado originalmente en export.arxiv.org el 15 de octubre de 2025.
Ver fuente original
