Program Synthesis for Non-Linear Real Arithmetic: Going Beyond Realizability

Resumen Técnico: Síntesis de Programas para Aritmética Real No Lineal: Más Allá de la Realizabilidad

Definición del Problema
Este artículo aborda el problema de sintetizar programas a partir de especificaciones en la teoría sin cuantificadores de la Aritmética Real No Lineal (NRA). A diferencia de la Síntesis Guiada por Sintaxis (SyGuS) tradicional, que falla cuando una especificación es "no realizable" (es decir, existen valores de entrada para los cuales ningún resultado satisface la especificación), este trabajo propone un objetivo de síntesis novedoso. El objetivo es sintetizar un programa que, para cualquier entrada racional, produzca una salida racional que satisfaga la especificación o informe explícitamente la inexistencia de dicha salida (denotada por $\bot$).

Para evitar errores de redondeo inherentes a la aritmética de punto fijo de precisión limitada, que pueden hacer que soluciones reales válidas fallen al evaluarse con aproximaciones, los autores restringen el dominio a entradas y salidas racionales. Esto define la clase de problemas RPSQ (Síntesis de Programas Reales con entradas y salidas racionales). Los programas sintetizados pueden contener bucles, condicionales y asignaciones, operando sobre números racionales.

Dureza Teórica y Limitaciones
Los autores establecen límites teóricos significativos para este problema:

1. Interreducibilidad con el Décimo Problema de Hilbert: Demuestran que RPSQ es interreducible con el Décimo Problema de Hilbert sobre los racionales ($HTP_{\mathbb{Q}}$). Dado que $HTP_{\mathbb{Q}}$ es un problema abierto de larga data en la teoría de números, esto implica que es improbable que exista un algoritmo de síntesis general, sonoro y completo para RPSQ.
2. Imposibilidad de Síntesis Sin Bucles: El artículo demuestra que RPSQ no puede resolverse utilizando únicamente programas sin bucles. Si existiera una solución sin bucles, implicaría que la teoría de la aritmética racional admite eliminación de cuantificadores, un resultado conocido por ser indecidible (Robinson, 1959).

Metodología y Algoritmos
Dada la indecidibilidad general, los autores proponen un enfoque por niveles:

1. Realizabilidad sobre Reales vs. Racionales: Muestran que si una especificación es realizable sobre los reales, cualquier programa sintetizado por herramientas SyGuS existentes (que operan sobre reales) también sirve como solución válida para el caso racional, siempre que las entradas y salidas sean racionales. Sin embargo, esto no se cumple a la inversa; una solución para racionales no implica necesariamente una solución para reales.

2. Algoritmo Sonoro y Completo para Salida Única ($|Y|=1$): Para especificaciones con una única variable de salida, los autores presentan un algoritmo sonoro y completo (Algoritmo 1). Este enfoque separa el problema en dos casos:

   • Desigualdades Estrictas: Utiliza Aislamiento de Raíces Reales (RRI) para encontrar intervalos donde el signo de los polinomios es invariante. Al muestrear puntos racionales dentro de estos intervalos (explotando la densidad de los racionales en los reales), encuentra soluciones para restricciones estrictas.
   • Desigualdades No Estrictas: Para soluciones que se encuentran en el límite (donde las desigualdades no estrictas se convierten en igualdades), el algoritmo emplea el Teorema de la Raíz Racional (RRT). Esto permite la enumeración de un conjunto finito de raíces candidatas racionales para las ecuaciones polinómicas derivadas de las condiciones de frontera.
     El algoritmo combina estos métodos con la Eliminación de Cuantificadores (utilizando QEPCAD) para determinar las precondiciones más débiles para la existencia de soluciones.

3. Algoritmo Sonoro pero Incompleto para el Caso General ($|Y|>1$): Para múltiples variables de salida, los autores proponen el Algoritmo 2 (implementado en la herramienta NQSynth). Este es un procedimiento sonoro pero incompleto que descompone iterativamente el problema de múltiples salidas en subproblemas de salida única:

   • Consulta un oráculo NRA (Z3) para encontrar una asignación satisfactoria racional (modelo).
   • Fija todas las variables de salida excepto una basándose en este modelo, reduciendo el problema a una instancia de síntesis de salida única resoluble mediante el algoritmo completo descrito anteriormente.
   • Construye una lista de decisiones (una serie de ramas if-then-else) donde cada rama corresponde a una precondición específica derivada mediante eliminación de cuantificadores.
   • El proceso se repite, refinando la especificación negando las precondiciones de las soluciones encontradas, hasta que la especificación se vuelve insatisfacible o se produce un tiempo de espera.

Implementación y Resultados Experimentales
Los autores implementaron su enfoque en una herramienta prototipo llamada NQSynth. La evaluaron frente a dos enfoques competidores:

• QEPCAD+CVC5: Una pipeline SyGuS modificada que primero calcula la precondición más débil sobre los reales y luego sintetiza un programa.
• ModEnum: Un enfoque basado en enumeración de modelos inspirado en el trabajo de Monniaux sobre aritmética lineal.

La evaluación utilizó dos conjuntos de pruebas:

1. Pruebas NRA: 83 pruebas adaptadas del repositorio SMT-LIB 2024 (familias meti-tarski/Arthan, asin, zankl).
2. Pruebas Geométricas: 51 especificaciones que modelan relaciones geométricas 2D y 3D (círculos, regiones anulares, hipérbolas).

Resultados Clave:

• NQSynth resolvió 59 de las 83 pruebas NRA y 33 de las 51 pruebas Geométricas dentro de un tiempo de espera de 120 segundos.
• En contraste, QEPCAD+CVC5 resolvió 26 NRA y 16 Geométricas, mientras que ModEnum resolvió 23 NRA y 11 Geométricas.
• Cabe destacar que NQSynth sintetizó con éxito programas para muchas especificaciones que eran no realizables (o donde la precondición más débil era difícil de calcular), un escenario donde las herramientas SyGuS fallan por completo.
• Los experimentos destacaron que el principal cuello de botella para NQSynth fue el paso de eliminación de cuantificadores (QEPCAD), particularmente para entradas más grandes, en lugar de la lógica de síntesis en sí misma.

Significado y Afirmaciones
El artículo afirma añadir una técnica novedosa al repertorio de síntesis de programas a partir de especificaciones NRA. Su significado principal radica en:

1. Manejo de la No Realizabilidad: Proporciona un método práctico para sintetizar programas que manejan con elegancia las entradas para las cuales no existe solución, una capacidad que carecen las herramientas SyGuS actuales de vanguardia.
2. Precisión Racional: Al dirigirse a entradas y salidas racionales, evita los errores de redondeo asociados con la aritmética de punto flotante, garantizando la corrección matemática para aplicaciones que requieren alta precisión.
3. Más Allá de SyGuS: El enfoque resuelve problemas que están fuera del alcance de las herramientas SyGuS existentes, incluso para especificaciones realizables, aprovechando propiedades de la teoría de números (RRT y RRI) en lugar de depender únicamente de la búsqueda sintáctica o la eliminación estándar de cuantificadores.

Los autores concluyen que, aunque una solución completa general es teóricamente improbable debido a la dureza de $HTP_{\mathbb{Q}}$, su procedimiento sonoro e incompleto ofrece una solución práctica robusta que supera significativamente a los métodos existentes en una amplia gama de pruebas. Se sugiere trabajo futuro para investigar las condiciones bajo las cuales los programas sin bucles son suficientes y para reducir la dependencia de motores pesados de eliminación de cuantificadores.