Resumen: Logic proporciona un banco de pruebas controlado para evaluar razonadores basados en LLM, sin embargo, los puntos de referencia estándar estilo SAT a menudo combinan la dificultad superficial (longitud, redacción, orden de las cláusulas) con los fenómenos estructurales que realmente determinan la satisfacibilidad. Introducimos un punto de referencia de diagnóstico para 2-SAT construido a partir de familias parametrizadas de fórmulas estructuradas de 2-CNF, donde la satisfacibilidad se caracteriza por el gráfico de implicaciones y se puede ajustar a lo largo de ejes interpretables. Nuestros generadores aíslan distintas competencias y modos de falla: (i) núcleos UNSAT de ciclo de contradicción con tamaño y desequilibrio controlables, (ii) instancias SAT con una fracción prescrita de variables libres para controlar la multiplicidad de la solución, (iii) columnas vertebrales plantadas que modulan la propagación, (iv) cláusulas puente tardías que acoplan regiones que de otro modo serían monótonas para sondear la sensibilidad al ordenamiento y la revisión, y (v) variantes de simetría/duplicación que prueban la abstracción bajo cambio de nombre y estructura redundante. Evaluamos razonadores basados en LLM en cuanto a la precisión de las decisiones y la validez de la asignación, y cuantificamos la robustez bajo perturbaciones que preservan la semántica, como el reordenamiento de cláusulas, cláusulas de relleno y cambio de nombre de variables. En todos los modelos, observamos transiciones bruscas en el desempeño bajo intervenciones estructurales específicas, incluso cuando las estadísticas superficiales se mantienen fijas, lo que revela regímenes de fragilidad que son invisibles para la precisión agregada del SAT.
Publicado originalmente en export.arxiv.org el 15 de febrero de 2026.
Ver fuente original
