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

Riepilogo Tecnico: Sintesi di Programmi per l'Aritmetica Reale Non Lineare: Oltre la Realizzabilità

Definizione del Problema
Questo articolo affronta il problema della sintesi di programmi a partire da specifiche nella teoria senza quantificatori dell'Aritmetica Reale Non Lineare (NRA). A differenza della Sintesi Guidata dalla Sintassi (SyGuS) tradizionale, che fallisce quando una specifica è "non realizzabile" (ovvero, esistono valori di input per i quali nessun output soddisfa la specifica), questo lavoro propone un nuovo obiettivo di sintesi. L'obiettivo è sintetizzare un programma che, per qualsiasi input razionale, produca o un output razionale che soddisfi la specifica, o segnali esplicitamente la non esistenza di tale output (denotato con $\bot$).

Per evitare errori di arrotondamento intrinseci all'aritmetica in virgola mobile a precisione fissa, che possono causare il fallimento di soluzioni reali valide quando valutate con approssimazioni, gli autori restringono il dominio agli input e agli output razionali. Ciò definisce la classe di problemi RPSQ (Sintesi di Programmi Reali con input e output razionali). I programmi sintetizzati sono autorizzati a contenere cicli, condizionali e assegnazioni, operando su numeri razionali.

Complessità Teorica e Limiti
Gli autori stabiliscono significativi confini teorici per questo problema:

1. Inter-reducibilità con il Decimo Problema di Hilbert: Dimostrano che RPSQ è inter-reducibile con il Decimo Problema di Hilbert sui razionali ($HTP_{\mathbb{Q}}$). Poiché $HTP_{\mathbb{Q}}$ è un problema aperto di lunga data nella teoria dei numeri, ciò implica che è improbabile l'esistenza di un algoritmo di sintesi generale corretto e completo per RPSQ.
2. Impossibilità della Sintesi Senza Cicli: L'articolo dimostra che RPSQ non può essere risolto utilizzando esclusivamente programmi privi di cicli. Se esistesse una soluzione senza cicli, ciò implicherebbe che la teoria dell'aritmetica razionale ammette l'eliminazione dei quantificatori, un risultato noto per essere indecidibile (Robinson, 1959).

Metodologia e Algoritmi
Data l'indeducibilità generale, gli autori propongono un approccio a livelli:

1. Realizzabilità sui Reali vs. sui Razionali: Dimostrano che se una specifica è realizzabile sui reali, qualsiasi programma sintetizzato dagli strumenti SyGuS esistenti (che operano sui reali) funge anche da soluzione valida per il caso razionale, purché gli input e gli output siano razionali. Tuttavia, ciò non vale in senso inverso; una soluzione per i razionali non implica necessariamente una soluzione per i reali.

2. Algoritmo Corretto e Completo per Output Singolo ($|Y|=1$): Per specifiche con una singola variabile di output, gli autori presentano un algoritmo corretto e completo (Algoritmo 1). Questo approccio suddivide il problema in due casi:

   • Disuguaglianze Strette: Utilizza l'Isolamento delle Radici Reali (RRI) per trovare intervalli in cui il segno dei polinomi è invariante. Campionando punti razionali all'interno di questi intervalli (sfruttando la densità dei razionali nei reali), trova soluzioni per vincoli stretti.
   • Disuguaglianze Non Strette: Per le soluzioni che giacciono sul bordo (dove le disuguaglianze non strette diventano uguaglianze), l'algoritmo impiega il Teorema delle Radici Razionali (RRT). Ciò permette l'enumerazione di un insieme finito di candidati di radici razionali per le equazioni polinomiali derivate dalle condizioni al contorno.
     L'algoritmo combina questi metodi con l'Eliminazione dei Quantificatori (utilizzando QEPCAD) per determinare le precondizioni più deboli per l'esistenza di soluzioni.

3. Algoritmo Corretto ma Incompleto per il Caso Generale ($|Y|>1$): Per più variabili di output, gli autori propongono l'Algoritmo 2 (implementato nello strumento NQSynth). Questa è una procedura corretta ma incompleta che scompone iterativamente il problema multi-output in sotto-problemi a output singolo:

   • Interroga un oracolo NRA (Z3) per trovare un'assegnazione soddisfacente razionale (modello).
   • Fissa tutte le variabili di output tranne una basandosi su questo modello, riducendo il problema a un'istanza di sintesi a output singolo risolvibile dall'algoritmo completo descritto sopra.
   • Costruisce una lista di decisioni (una serie di rami if-then-else) dove ogni ramo corrisponde a una specifica precondizione derivata tramite eliminazione dei quantificatori.
   • Il processo si ripete, affinando la specifica negando le precondizioni delle soluzioni trovate, fino a quando la specifica diventa insoddisfacibile o si verifica un timeout.

Implementazione e Risultati Sperimentali
Gli autori hanno implementato il loro approccio in uno strumento prototipale denominato NQSynth. Lo hanno valutato confrontandolo con due approcci concorrenti:

• QEPCAD+CVC5: Una pipeline SyGuS modificata che calcola prima la precondizione più debole sui reali e poi sintetizza un programma.
• ModEnum: Un approccio basato sull'enumerazione di modelli ispirato al lavoro di Monniaux sull'aritmetica lineare.

La valutazione ha utilizzato due set di benchmark:

1. Benchmark NRA: 83 benchmark adattati dal repository SMT-LIB 2024 (famiglie meti-tarski/Arthan, asin, zankl).
2. Benchmark Geometrici: 51 specifiche che modellano relazioni geometriche 2D e 3D (cerchi, regioni anulari, iperboli).

Risultati Chiave:

• NQSynth ha risolto 59 su 83 benchmark NRA e 33 su 51 benchmark Geometrici entro un timeout di 120 secondi.
• Al contrario, QEPCAD+CVC5 ha risolto 26 benchmark NRA e 16 Geometrici, mentre ModEnum ha risolto 23 benchmark NRA e 11 Geometrici.
• In modo notevole, NQSynth ha sintetizzato con successo programmi per molte specifiche che erano non realizzabili (o dove la precondizione più debole era difficile da calcolare), uno scenario in cui gli strumenti SyGuS falliscono completamente.
• Gli esperimenti hanno evidenziato che il collo di bottiglia principale per NQSynth era il passo di eliminazione dei quantificatori (QEPCAD), in particolare per input più grandi, piuttosto che la logica di sintesi stessa.

Significato e Affermazioni
L'articolo afferma di aggiungere una tecnica innovativa al repertorio della sintesi di programmi da specifiche NRA. Il suo significato principale risiede in:

1. Gestione della Non Realizzabilità: Fornisce un metodo pratico per sintetizzare programmi che gestiscono elegantemente gli input per i quali non esiste soluzione, una capacità mancante negli attuali strumenti SyGuS all'avanguardia.
2. Precisione Razionale: Mirando a input e output razionali, evita gli errori di arrotondamento associati all'aritmetica in virgola mobile, garantendo la corretteta matematica per applicazioni che richiedono alta precisione.
3. Oltre SyGuS: L'approccio risolve problemi che sono oltre la portata degli strumenti SyGuS esistenti, anche per specifiche realizzabili, sfruttando proprietà della teoria dei numeri (RRT e RRI) invece di affidarsi esclusivamente alla ricerca sintattica o all'eliminazione standard dei quantificatori.

Gli autori concludono che, sebbene una soluzione completa generale sia teoricamente improbabile a causa della complessità di $HTP_{\mathbb{Q}}$, la loro procedura corretta e incompleta offre una soluzione pratica robusta che supera significativamente i metodi esistenti su un'ampia gamma di benchmark. Viene suggerito un lavoro futuro per investigare le condizioni in cui i programmi senza cicli sono sufficienti e per ridurre la dipendenza da motori pesanti di eliminazione dei quantificatori.