El auge de la IA generativa en programación exige métodos formales que garanticen que los sistemas automáticos produzcan las soluciones realmente deseadas. Esos métodos requieren especificaciones matemáticas, un terreno que la mayoría de programadores domina peor que el código. Investigadores del blog Brown PLT proponen una herramienta llamada PICK para cerrar la brecha entre la intención humana, expresada en lenguaje natural, y una especificación formal verificable.
El problema central es cómo pasar de lo informal a lo formal. Confiar en un LLM para traducir directamente la prosa del usuario a lógica matemática reproduce los errores, ambigüedades y malentendidos del propio usuario, sin forma de detectarlos. Piling on more LLMs no resuelve el fallo: los modelos comparten datos de entrenamiento, sesgos y misconceptions, por lo que叠加 más modelos aporta más acuerdo, pero no redundancia independiente.
PICK adopta un enfoque diferente: pide al LLM varios candidatos de especificación y, a partir de las diferencias entre ellos, genera ejemplos concretos donde los candidatos discrepan. El usuario vota cada ejemplo, y sus aceptaciones y rechazos funcionan como testigo independiente de su intención. La especificación que sobrevive a esos votos es la que mejor refleja lo que el usuario quería decir. El algoritmo se ha aplicado ya a expresiones regulares, lógica temporal lineal (LTL) y control de acceso basado en atributos (ABAC), dominios muy distintos que comparten cierre bajo negación e intersección y posibilidad de muestrear contraejemplos.
Los autores destacan que la aportación clave de PICK no es solo validar, sino recuperar un testigo de la intención del usuario que la síntesis —incluida la síntesis con LLM— tiende a borrar. Si programa y especificación nacen del mismo modelo, los dos pueden equivocarse de la misma manera. Los votos humanos reintroducen la independencia que la verificación siempre necesitó.