Tengo que admitir: estoy leyendo la
revista ACM . Me convierte en un "nerd", incluso para los estándares de los programadores. Entre otras cosas, aprendí de esta revista sobre "pruebas metamórficas". Nunca había oído hablar de él antes, como todas las personas que le pregunté. Pero la literatura científica sobre este tema es sorprendentemente voluminosa: hay muchos ejemplos increíblemente exitosos de su aplicación en campos de investigación completamente diferentes. Entonces, ¿por qué no hemos oído hablar de él antes? Solo hay
un artículo para personas ajenas a la comunidad científica. Ahora que haya dos de ellos.
Breve antecedentes
La mayoría de las pruebas escritas usan
oráculos . Es decir, conoce la respuesta y verifica explícitamente si los cálculos dan la respuesta correcta.
def test_dist(): p1 = (0, 3) p2 = (4, 0) assert dist(p1, p2) == 5
Además de las pruebas de oráculo, también hay pruebas manuales. El probador se sienta en la computadora y compara los datos de entrada con los resultados. A medida que los sistemas se vuelven más complejos, las pruebas manuales son cada vez menos útiles. Cada uno de ellos verifica solo un punto en un espacio de estado mucho más grande, y necesitamos algo que explore todo el espacio de estado.
Esto nos lleva a
pruebas generativas : escribir pruebas que cubran un conjunto aleatorio en un espacio de estado. El estilo más popular de prueba generativa es la
prueba basada en propiedades , o PBT. Encontramos la "propiedad" de la función, y luego generamos los valores de entrada y verificamos si los valores de salida coinciden con esta propiedad.
def test_dist(): p1 = random_point() p2 = random_point() assert dist(p1, p2) >= 0
La ventaja de PBT es que cubre más espacio. Su desventaja es la pérdida de especificidad. ¡Esto ya no
es una prueba de oráculo! No sabemos cuál debería ser la respuesta, y la función puede ser errónea, pero de una manera que tiene la misma propiedad. Aquí confiamos en la heurística.
Un problema grave con PBT es encontrar buenas propiedades. La mayoría de las funciones tienen propiedades simples, generales y propiedades complejas y específicas.
Las propiedades generales se pueden aplicar a una gran cantidad de funciones, pero no nos brindan mucha información. Las propiedades más específicas brindan más información, pero son más difíciles de encontrar y son aplicables solo en áreas de tareas limitadas. Si tiene una función que determina si un gráfico es acíclico, ¿qué pruebas de propiedad escribirá? ¿Le darán confianza de que la función es correcta?
Motivación
Ahora considere una tarea más compleja. Imagine que desea escribir un convertidor de voz a texto (STT) para inglés. Recibe un archivo de sonido y muestra el texto. ¿Cómo lo probarías?
La forma más fácil de usar un oráculo de mano. Dicte la oración y verifique si el texto de salida coincide. ¡Pero esto ni siquiera está lo suficientemente cerca! El rango del habla humana
es enorme . Sería mejor probar 1,000 o incluso 10,000 archivos de sonido diferentes. Los oráculos de mano con transcripción serían demasiado costosos. Esto significa que tenemos que usar pruebas basadas en propiedades en su lugar.
Pero, ¿cómo generamos aportes? Por ejemplo, podemos crear líneas aleatorias, pasarlas a través de un convertidor de texto a voz (texto a voz, TTS) y luego asegurarnos de que nuestro STT produzca el mismo texto. Pero esto nuevamente nos da un rango muy limitado de voz humana. ¿Puede TTS crear cambios en la entonación, "tragar" palabras, imitar un acento fuerte? Si no podemos tratar con ellos, ¿el STT será particularmente útil? Es mejor usar textos arbitrarios, por ejemplo, grabaciones de la radio, de podcasts y videos en línea.
Ahora surge un nuevo problema. Cuando usamos TTS, comenzamos con texto escrito. En el caso de archivos de sonido arbitrarios, no lo tenemos, y al mismo tiempo no queremos transcribirlo manualmente. En cambio, estamos limitados a usar propiedades. ¿Qué propiedades necesitamos probar? Ejemplos de las propiedades más simples: "el programa no se bloquea con ningún dato entrante" (una buena propiedad) o "no convierte la música acústica en palabras" (¿tal vez?). Estas propiedades no cubren muy bien la verificación de la tarea principal del programa y aumentan ligeramente la confianza en su calidad.
Entonces, tenemos dos tareas. Primero, necesitamos una gran cantidad de información en forma de discurso. En segundo lugar, debemos entender cómo convertirlos en pruebas útiles sin pasar largas horas transcribiendo manualmente las voces en oráculos.
Prueba metamórfica
Por todo esto, la salida se considera por separado. ¿Qué pasa si los incorporamos en un contexto más amplio? Por ejemplo, si un clip de sonido se transcribe en la salida,
siempre deberíamos
out con:
- Subir volumen doble
- Frecuencia creciente
- Aumentar el ritmo
- Agregar ruido de fondo
- Agregar ruido del vehículo
- Cualquier combinación de lo anterior.
Todas estas son transformaciones "simples" que podemos probar fácilmente. Por ejemplo, para una prueba con "ruido del vehículo", podemos tomar 10 muestras de ruido del automóvil, ponerlas en un clip de sonido y verificar si los resultados de reconocimiento de las 11 versiones coinciden. Podemos duplicar o aumentar el volumen, convirtiendo 11 versiones en 33 versiones, y luego duplicar el ritmo para obtener 66 versiones. Este principio se puede aplicar a cada clip de sonido en nuestra base de datos, ampliando significativamente el espacio de datos entrantes.
La presencia de 66 versiones para comparación es bastante conveniente. Pero eso no es todo: todavía no necesitamos saber cuál debería ser el resultado. Si las 66 conversiones regresan, entonces la prueba pasó con éxito, si al menos una devuelve algo más, entonces la prueba falló. En ningún momento debemos verificar lo que contiene. Esto es extremadamente importante. Por lo tanto, aumentamos significativamente el espacio de prueba con muy poca participación humana. Por ejemplo, podemos descargar un episodio de la serie, realizar conversiones y verificar si todos los resultados de su conversión a texto
1 coinciden. Obtuvimos pruebas útiles
sin escuchar el clip de voz . ¡Ahora podemos generar pruebas complejas y profundas sin usar un oráculo!
Dos conjuntos de datos de entrada, así como sus datos de salida están conectados entre sí. Dicha propiedad relacionada con el conjunto de datos entrantes / salientes se denomina
enlace metamórfico 2 . Las pruebas que aplican esta propiedad se llaman
pruebas metamórficas . En sistemas complejos, las relaciones metamórficas interesantes se pueden encontrar más fácilmente que las propiedades interesantes de los datos entrantes / salientes individuales.
Digámoslo un poco más formalmente: si tenemos
x y
f(x) , entonces podemos realizar algunas transformaciones de
x para obtener
x2 f(x2) . En el caso de STT, solo verificamos
f(x) = f(x2) , pero podemos usar cualquier relación entre los dos conjuntos de datos. Puede haber relaciones metamórficas como
f(x2) > f(x) o "es
f(x2)/f(x) un valor entero". De manera similar, este principio puede extenderse a varios conjuntos de datos de entrada utilizando
f(x) f(x3) . Un ejemplo de esto es comparar los resultados de un motor de búsqueda sin filtros con los resultados de un motor con uno o dos filtros. En la mayoría de las descripciones de casos de uso que leí, solo se usan dos conjuntos de datos de entrada, porque incluso son suficientes para encontrar errores locos.
Ejemplos de uso
Hablando de casos de uso: ¿qué tan efectivas son las pruebas metamórficas en la práctica? Una cosa es hablar de una técnica de manera abstracta o dar ejemplos artificiales. Los estudios de caso son útiles por tres razones. En primer lugar, muestra si el método realmente funciona. En segundo lugar, de ellos puede aprender sobre las posibles dificultades al usar MT. Tercero, los ejemplos nos muestran
cómo podemos usar la técnica. Cualquier conexión metamórfica utilizada en el ejemplo de uso puede intentarse para adaptarse a la solución de nuestros problemas.
Pruebas metamórficas: una revisión de desafíos y oportunidades proporciona una lista de muchos estudios, pero todos son artículos científicos. A continuación se presentan los más interesantes. Los artículos marcados con
(pdf) se presentan, como puede suponer, en PDF.
El problema
Oh, entonces
todas estas fuentes están en PDF.
Me llevó varias horas encontrar todos estos artículos. Y este problema está asociado con el mayor obstáculo para el desarrollo de MT: todos los enlaces anteriores son
preimpresiones o primeros borradores de futuros artículos científicos. Cuando empiezo a comprender técnicas poco conocidas, en primer lugar me hago la pregunta: "¿por qué son poco conocidas?" A veces la razón es obvia, a veces es un conjunto complejo de pequeñas razones, a veces el problema es simplemente que la metodología está "fuera de suerte".
En el caso de MT, el problema es obvio.
Casi toda la información está oculta detrás del muro de pago científico. Si desea estudiar MT, necesita acceso a la revista o debe pasar varias horas buscando preimpresiones
3 .
Estudio adicional
El inventor de MT es
Ty Chen . Se convirtió en la fuerza impulsora de muchos estudios. Otros investigadores en esta área son
Zhi Quan Zhou y
Sergio Segura ; ambos publicaron todas sus preimpresiones en Internet. La mayor parte del trabajo de investigación es realizado por una de estas personas.
Probablemente el mejor lugar para comenzar es con las
pruebas metamórficas: una revisión de desafíos y oportunidades y
una encuesta sobre pruebas metamórficas . Aunque este artículo está escrito sobre
pruebas metamórficas, los investigadores también aplicaron las relaciones metamórficas en general a una amplia variedad de otras disciplinas, por ejemplo, la verificación formal de códigos y la depuración. Todavía no he estudiado estas áreas de aplicación de la técnica en detalle, pero probablemente valga la pena mirarlas también.
Desde el punto de vista de la aplicabilidad, en teoría puede ser posible adaptar la mayoría de las bibliotecas PBT para verificar las propiedades metamórficas. De hecho, el primer ejemplo en
Quickcheck es probar la EM, y en
este ensayo sobre PBT, la EM se aplica indirectamente.
En general, me parece que la mayoría de las investigaciones de PBT se centran en generar y recortar datos de manera eficiente, y la investigación de MT se centra principalmente en determinar lo que realmente necesitamos probar. En consecuencia, es probable que estas técnicas se complementen entre sí.
Gracias a Brian Ng por su ayuda en la investigación.Postdata: solicitud
De hecho, no es sorprendente que nunca antes haya oído hablar de esta técnica. Existen muchas técnicas realmente interesantes y útiles que no pueden dejar su pequeña burbuja. Descubrí MTs por suerte en lugar de búsquedas activas.
Si sabe algo que vale la pena usar,
escríbame .
- Bueno, puede haber problemas obvios: puede haber música en el podcast, fragmentos de discurso en otros idiomas, etc. Pero la teoría es confiable: si podemos obtener muestras de voz, podemos usarlas como parte de las pruebas sin una transcripción / marcado manual preliminar.
- En especificaciones, la idea correspondiente son las hiperpropiedades , propiedades de conjuntos de comportamientos, en lugar de comportamientos individuales. La mayoría de los estudios hiperespecíficos están relacionados con la seguridad de HS. Según tengo entendido, su HS es un superconjunto de MS.
- Tenía una segunda hipótesis, ahora refutada: dado que la mayoría de los principales investigadores de China y Hong Kong, tal vez esta técnica sea más conocida en las comunidades de programadores que se comunican en mandarín, en lugar de en inglés. Brian Eun probó esta hipótesis por mí, pero no encontró ningún signo significativo del uso de la técnica por parte de los chinos.