Antes de pedirle a una IA que piense, prueba a limpiar primero su entrada

Una fórmula lógica y una consulta de razonamiento no son lo mismo, pero en muchos pipelines de IA viajan juntas: una base de conocimiento expresada en forma normal conjuntiva (CNF) se compila en un circuito compacto, y ese circuito responde preguntas sobre sus modelos. Durante décadas, los profesionales han debatido si preprocesar primero la CNF y, en caso afirmativo, qué simplificaciones son seguras. Un estudio publicado por investigadores del CRIL, un laboratorio conjunto del CNRS y la Universidad de Artois, ofrece una respuesta clara: los preprocesadores que preservan los conteos de modelos y retienen las definiciones de las variables eliminadas desbloquean ganancias de rendimiento significativas, mientras que aquellos que solo preservan la satisfacibilidad son inútiles para el muestreo y la enumeración.

El panorama del preprocesamiento

El artículo, liderado por Jean Marie Lagniez y Emmanuel Lonca, examina tres familias de técnicas de preprocesamiento: las que preservan la equivalencia lógica (vivificación, detección de backbone, reducción de ocurrencias), las que solo preservan la satisfacibilidad (eliminación de variables, eliminación de cláusulas bloqueadas) y las que preservan el conteo de modelos eliminando variables definidas. Para tareas como el muestreo uniforme, el acceso directo (devolver el k-ésimo modelo bajo un orden lexicográfico) y la enumeración de modelos, la distinción importa profundamente.

Los autores demuestran que las técnicas que preservan la satisfacibilidad, como la eliminación de variables y la eliminación de cláusulas bloqueadas, son fundamentalmente incompatibles con estas consultas. En un contraejemplo simple, la fórmula a ∨ b se reduce a ⊤ bajo ambos métodos, perdiendo toda la información sobre los modelos originales. "A partir de Φ' es imposible recuperar los modelos de Φ", escriben, confirmando una limitación conocida también para el conteo de modelos.

Más sorprendente es el hallazgo de que incluso las técnicas que preservan el conteo de modelos, eliminar variables que están implícita o explícitamente definidas por otras variables, no se pueden aplicar directamente. La fórmula preprocesada por sí sola carece del mapeo necesario para reconstruir los modelos originales. Sin embargo, cuando las definiciones de las variables eliminadas se almacenan en una función de evaluación compatible, el enfoque se vuelve viable para el muestreo uniforme y la enumeración completa de modelos.

El acceso directo exige orden

Las consultas de acceso directo, donde un usuario solicita el k-ésimo modelo bajo un orden de variables lexicográfico específico, añaden una restricción adicional. Los autores definen un "orden compatible" que coloca todas las variables eliminadas después de sus variables definitorias. Esto garantiza que el k-ésimo modelo de la fórmula preprocesada, cuando se extiende con la función de evaluación, se corresponda exactamente con el k-ésimo modelo original. Surgen dos estrategias: o el paso de preprocesamiento fija la cola del orden de variables, o restringe la eliminación a variables cuyos definidores aparecen todos antes en el orden dado. La primera elimina más variables; la segunda le da al usuario total libertad.

La enumeración parcial de modelos es donde el enfoque encuentra un límite difícil. Los investigadores muestran un ejemplo donde eliminar una variable definida por un XOR conduce a una brecha exponencial entre el número de modelos parciales en las fórmulas original y simplificada: la función de paridad no tiene representación compacta, por lo que el preprocesamiento destruye efectivamente la estructura necesaria para la enumeración parcial.

Evidencia experimental de 1425 puntos de referencia

El equipo realizó extensos experimentos utilizando el preprocesador B+E y el compilador de conocimiento d4 en puntos de referencia de estudios previos de muestreo uniforme. Probaron cuatro configuraciones: sin preprocesamiento, solo preservación de equivalencia (equiv), equivalencia más eliminación de variables explícitamente definidas (#equiv-explicit) y esta última con orden compatible impuesto (#equiv-explicit-ordered).

El gráfico cactus revela una jerarquía clara. El preprocesamiento solo equiv ofrece ganancias marginales, resolviendo solo ocho instancias más que sin preprocesamiento. #equiv-explicit-ordered maneja 47 instancias más que la línea base, una mejora sustancial, mientras que #equiv-explicit resuelve 55 más, aunque no puede responder directamente consultas de acceso directo sin restricciones de orden. Para el muestreo uniforme y la enumeración, los autores informan reducciones significativas en el tiempo de ejecución, con los circuitos preprocesados superando constantemente a sus contrapartes sin procesar.

El trabajo subraya un principio práctico para los ingenieros de IA: si la tarea descendente implica conteo de modelos, muestreo o enumeración, invierta en preprocesadores que preserven los conteos de modelos y lleven las definiciones de variables hacia adelante. La sobrecarga de rastrear esas definiciones es mínima en comparación con el tiempo de compilación ahorrado.