STL: Lógica Sorprendentemente Difícil (para la Validación de Sistemas)

Gran parte del trabajo reciente en el desarrollo de técnicas de métodos formales para especificar o aprender el comportamiento de sistemas autónomos se basa en la creencia de que las especificaciones formales son interpretables y útiles para los humanos al verificar sistemas. Aunque se afirma con frecuencia, esta suposición rara vez se pone a prueba. Realizamos un experimento humano (N=62) con una mezcla de personas que estaban y no estaban familiarizadas con métodos formales previamente, pidiéndoles que validaran si un conjunto de restricciones de lógica temporal de señales (STL) mantendría a un agente fuera de peligro y le permitiría completar una tarea en un entorno de captura de la bandera en un mundo de cuadrícula. La precisión de la validación fue del 45% ± 20% (media desviación estándar). La validez de la especificación de la verdad, la familiaridad de los sujetos con los métodos formales y el nivel educativo de los sujetos resultaron ser factores significativos para determinar la corrección de la validación. Los participantes mostraron un sesgo de afirmación, lo que causó un aumento significativo de la precisión en especificaciones válidas, pero una disminución significativa en especificaciones no válidas. Además, los participantes, particularmente aquellos familiarizados con métodos formales, tendían a ser excesivamente seguros en sus respuestas, y a tener confianza similar independientemente de la corrección real. Nuestros datos no respaldan la creencia de que las especificaciones formales son inherentemente interpretables para los humanos en un grado significativo para la validación de sistemas. Recomendamos mejoras ergonómicas en la presentación de datos y en la formación en validación, que deberían probarse antes de que las afirmaciones de interpretabilidad regresen a la literatura sobre métodos formales.