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

Résumé Technique : Synthèse de Programmes pour l'Arithmétique Réelle Non Linéaire : Aller Au-delà de la Réalisabilité

Définition du Problème
Ce papier aborde le problème de la synthèse de programmes à partir de spécifications dans la théorie sans quantificateurs de l'Arithmétique Réelle Non Linéaire (NRA). Contrairement à la Synthèse Guidée par la Syntaxe (SyGuS) traditionnelle, qui échoue lorsqu'une spécification est « irréalisable » (c'est-à-dire qu'il existe des valeurs d'entrée pour lesquelles aucune sortie ne satisfait la spécification), ce travail propose un nouvel objectif de synthèse. Le but est de synthétiser un programme qui, pour toute entrée rationnelle, produit soit une sortie rationnelle satisfaisant la spécification, soit signale explicitement l'absence d'une telle sortie (notée par $\bot$).

Pour éviter les erreurs d'arrondi inhérentes à l'arithmétique à virgule flottante de précision fixe, qui peuvent faire échouer de vraies solutions réelles lors de leur évaluation avec des approximations, les auteurs restreignent le domaine aux entrées et sorties rationnelles. Cela définit la classe de problèmes RPSQ (Synthèse de Programme Réel avec entrées et sorties rationnelles). Les programmes synthétisés sont autorisés à contenir des boucles, des conditionnelles et des affectations, opérant sur des nombres rationnels.

Difficulté Théorique et Limites
Les auteurs établissent des limites théoriques significatives pour ce problème :

1. Inter-réductibilité avec le Dixième Problème de Hilbert : Ils prouvent que RPSQ est inter-réductible avec le Dixième Problème de Hilbert sur les rationnels ($HTP_{\mathbb{Q}}$). Puisque $HTP_{\mathbb{Q}}$ est un problème ouvert de longue date en théorie des nombres, cela implique qu'un algorithme de synthèse général, sound et complet pour RPSQ, est peu susceptible d'exister.
2. Impossibilité de la Synthèse Sans Boucles : Le papier démontre que RPSQ ne peut pas être résolu en utilisant uniquement des programmes sans boucles. Si une solution sans boucles existait, cela impliquerait que la théorie de l'arithmétique rationnelle admet une élimination des quantificateurs, un résultat connu pour être indécidable (Robinson, 1959).

Méthodologie et Algorithmes
Étant donné l'indécidabilité générale, les auteurs proposent une approche en plusieurs niveaux :

1. Réalisation sur les Réels vs les Rationnels : Ils montrent que si une spécification est réalisable sur les réels, tout programme synthétisé par des outils SyGuS existants (qui opèrent sur les réels) sert également de solution valide pour le cas rationnel, à condition que les entrées et les sorties soient rationnelles. Cependant, cela ne vaut pas dans l'autre sens ; une solution pour les rationnels n'implique pas nécessairement une solution pour les réels.

2. Algorithme Sound et Complet pour une Sortie Unique ($|Y|=1$) : Pour les spécifications avec une seule variable de sortie, les auteurs présentent un algorithme sound et complet (Algorithme 1). Cette approche sépare le problème en deux cas :

   • Inégalités Strictes : Il utilise l'Isolation des Racines Réelles (RRI) pour trouver des intervalles où le signe des polynômes est invariant. En échantillonnant des points rationnels au sein de ces intervalles (exploitant la densité des rationnels dans les réels), il trouve des solutions pour les contraintes strictes.
   • Inégalités Non Strictes : Pour les solutions se trouvant sur la frontière (où les inégalités non strictes deviennent des égalités), l'algorithme emploie le Théorème de la Racine Rationnelle (RRT). Cela permet l'énumération d'un ensemble fini de racines rationnelles candidates pour les équations polynomiales dérivées des conditions aux limites.
     L'algorithme combine ces éléments avec l'élimination des quantificateurs (en utilisant QEPCAD) pour déterminer les préconditions les plus faibles pour l'existence de solutions.

3. Algorithme Sound mais Incomplet pour le Cas Général ($|Y|>1$) : Pour plusieurs variables de sortie, les auteurs proposent l'Algorithme 2 (implémenté dans l'outil NQSynth). Il s'agit d'une procédure sound mais incomplète qui décompose itérativement le problème multi-sorties en sous-problèmes à sortie unique :

   • Il interroge un oracle NRA (Z3) pour trouver une affectation satisfaisante rationnelle (modèle).
   • Il fixe toutes les variables de sortie sauf une sur la base de ce modèle, réduisant le problème à une instance de synthèse à sortie unique résoluble par l'algorithme complet décrit ci-dessus.
   • Il construit une liste de décision (une série de branches if-then-else) où chaque branche correspond à une précondition spécifique dérivée via l'élimination des quantificateurs.
   • Le processus se répète, affinant la spécification en niant les préconditions des solutions trouvées, jusqu'à ce que la spécification devienne insatisfaisable ou qu'un dépassement de temps se produise.

Implémentation et Résultats Expérimentaux
Les auteurs ont implémenté leur approche dans un outil prototype nommé NQSynth. Ils l'ont évalué par rapport à deux approches concurrentes :

• QEPCAD+CVC5 : Un pipeline SyGuS modifié qui calcule d'abord la précondition la plus faible sur les réels, puis synthétise un programme.
• ModEnum : Une approche basée sur l'énumération de modèles, inspirée des travaux de Monniaux sur l'arithmétique linéaire.

L'évaluation a utilisé deux ensembles de benchmarks :

1. Benchmarks NRA : 83 benchmarks adaptés du dépôt SMT-LIB 2024 (familles meti-tarski/Arthan, asin, zankl).
2. Benchmarks Géométriques : 51 spécifications modélisant des relations géométriques 2D et 3D (cercles, régions annulaires, hyperboles).

Résultats Clés :

• NQSynth a résolu 59 des 83 benchmarks NRA et 33 des 51 benchmarks Géométriques dans un délai de 120 secondes.
• En revanche, QEPCAD+CVC5 a résolu 26 benchmarks NRA et 16 benchmarks Géométriques, tandis que ModEnum a résolu 23 benchmarks NRA et 11 benchmarks Géométriques.
• Notamment, NQSynth a réussi à synthétiser des programmes pour de nombreuses spécifications qui étaient irréalisables (ou dont la précondition la plus faible était difficile à calculer), un scénario où les outils SyGuS échouent totalement.
• Les expériences ont mis en évidence que le goulot d'étranglement principal pour NQSynth était l'étape d'élimination des quantificateurs (QEPCAD), en particulier pour les entrées plus volumineuses, plutôt que la logique de synthèse elle-même.

Signification et Revendications
Le papier revendique l'ajout d'une nouvelle technique au répertoire de la synthèse de programmes à partir de spécifications NRA. Sa signification principale réside dans :

1. Gestion de l'Irréalisation : Il fournit une méthode pratique pour synthétiser des programmes qui gèrent élégamment les entrées pour lesquelles aucune solution n'existe, une capacité manquante dans les outils SyGuS de l'état de l'art actuels.
2. Précision Rationnelle : En ciblant les entrées et sorties rationnelles, il évite les erreurs d'arrondi associées à l'arithmétique à virgule flottante, garantissant la correction mathématique pour les applications nécessitant une haute précision.
3. Au-delà de SyGuS : L'approche résout des problèmes hors de portée des outils SyGuS existants, même pour des spécifications réalisables, en exploitant des propriétés de la théorie des nombres (RRT et RRI) plutôt que de compter uniquement sur une recherche syntaxique ou une élimination standard des quantificateurs.

Les auteurs concluent que, bien qu'une solution complète générale soit théoriquement peu probable en raison de la difficulté de $HTP_{\mathbb{Q}}$, leur procédure sound et incomplète offre une solution pratique robuste qui surpasse significativement les méthodes existantes sur un large éventail de benchmarks. Des travaux futurs sont suggérés pour investiguer les conditions dans lesquelles les programmes sans boucles sont suffisants et pour réduire la dépendance aux moteurs lourds d'élimination des quantificateurs.