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

Technische Samenvatting: Programmasynthese voor Niet-Lineaire Reële Arithmetica: Voorbij Realiseerbaarheid

Probleemdefinitie
Dit artikel behandelt het probleem van het synthetiseren van programma's uit specificaties in de quantielvrije theorie van Niet-Lineaire Reële Arithmetica (NRA). In tegenstelling tot traditionele Syntax-Guided Synthesis (SyGuS), dat faalt wanneer een specificatie "niet realiseerbaar" is (d.w.z. er bestaan invoerwaarden waarvoor geen uitvoer aan de specificatie voldoet), stelt dit werk een nieuwe synthese-Doelstelling voor. Het doel is een programma te synthetiseren dat, voor elke rationale invoer, ofwel een rationale uitvoer produceert die aan de specificatie voldoet, ofwel expliciet meldt dat een dergelijke uitvoer niet bestaat (aangeduid met $\bot$).

Om afrondingsfouten inherent aan vaste precisie zwevend-kommawiskunde te vermijden, die kunnen leiden tot het falen van geldige reële oplossingen bij evaluatie met benaderingen, beperken de auteurs het domein tot rationale invoer en uitvoer. Dit definieert de probleemklasse RPSQ (Real Program Synthesis with Rational inputs and outputs). De gegenereerde programma's mogen loops, conditionals en toewijzingen bevatten, die opereren op rationale getallen.

Theoretische Moeilijkheid en Beperkingen
De auteurs stellen aanzienlijke theoretische grenzen voor dit probleem vast:

1. Onderlinge Reduceerbaarheid met Hilberts Tiende Probleem: Zij bewijzen dat RPSQ onderling reduceerbaar is met Hilberts Tiende Probleem over de rationale getallen ($HTP_{\mathbb{Q}}$). Aangezien $HTP_{\mathbb{Q}}$ een langdurig open probleem is in de getaltheorie, impliceert dit dat een algemeen correct en volledig synthese-algoritme voor RPSQ onwaarschijnlijk bestaat.
2. Onmogelijkheid van Loop-Vrije Synthese: Het artikel demonstreert dat RPSQ niet kan worden opgelost met uitsluitend loop-vrije programma's. Als een loop-vrije oplossing zou bestaan, zou dit impliceren dat de theorie van rationale arithmetica quantieleliminatie toestaat, een resultaat waarvan bekend is dat het onbeslisbaar is (Robinson, 1959).

Methodologie en Algoritmen
Gezien de algemene onbeslisbaarheid stellen de auteurs een gefaseerde aanpak voor:

1. Realiseerbaarheid over Reële versus Rationale Getallen: Zij tonen aan dat als een specificatie realiseerbaar is over de reële getallen, elk programma dat door bestaande SyGuS-tools wordt gegenereerd (die werken over de reële getallen), ook dient als een geldige oplossing voor het rationale geval, mits de invoer en uitvoer rationaal zijn. Dit geldt echter niet omgekeerd; een oplossing voor rationale getallen impliceert niet noodzakelijk een oplossing voor reële getallen.

2. Correct en Volledig Algoritme voor Eén Uitvoer ($|Y|=1$): Voor specificaties met één uitvoervariabele presenteren de auteurs een correct en volledig algoritme (Algoritme 1). Deze aanpak splitst het probleem op in twee gevallen:

   • Strikte Ongelijkheden: Het maakt gebruik van Real Root Isolation (RRI) om intervallen te vinden waar het teken van polynomen invariant is. Door rationale punten binnen deze intervallen te bemonsteren (benutten van de dichtheid van rationale getallen in de reële getallen), worden oplossingen gevonden voor strikte constraints.
   • Niet-Strikte Ongelijkheden: Voor oplossingen die op de grens liggen (waar niet-strikte ongelijkheden gelijkheden worden), hanteert het algoritme de Rational Root Theorem (RRT). Dit maakt het mogelijk een eindige verzameling kandidaat-rationale wortels te enumereren voor de polynoomvergelijkingen die zijn afgeleid uit de randvoorwaarden.
     Het algoritme combineert deze methoden met Quantieleliminatie (met behulp van QEPCAD) om de zwakste precondities voor het bestaan van oplossingen te bepalen.

3. Correct maar Onvolledig Algoritme voor Algemeen Geval ($|Y|>1$): Voor meerdere uitvoervariabelen stellen de auteurs Algoritme 2 voor (geïmplementeerd in het gereedschap NQSynth). Dit is een correct maar onvolledige procedure die het meer-uitvoerprobleem iteratief ontleedt tot sub-problemen met één uitvoer:

   • Het vraagt een NRA-orakel (Z3) om een rationale vervullende toewijzing (model) te vinden.
   • Het fixeert alle uitvoervariabelen behalve één op basis van dit model, waardoor het probleem wordt gereduceerd tot een synthese-instantie met één uitvoer die oplosbaar is met het hierboven beschreven volledige algoritme.
   • Het construeert een beslissingslijst (een reeks if-then-else-takken) waarbij elke tak overeenkomt met een specifieke preconditie die via quantieleliminatie is afgeleid.
   • Het proces herhaalt zich, waarbij de specificatie wordt verfijnd door de precondities van gevonden oplossingen te negëren, totdat de specificatie onvoldoende wordt of een time-out optreedt.

Implementatie en Experimentele Resultaten
De auteurs hebben hun aanpak geïmplementeerd in een prototype-tool genaamd NQSynth. Zij hebben deze geëvalueerd tegenover twee concurrerende benaderingen:

• QEPCAD+CVC5: Een aangepaste SyGuS-pijplijn die eerst de zwakste preconditie over de reële getallen berekent en vervolgens een programma synthetiseert.
• ModEnum: Een op model-enumeratie gebaseerde aanpak, geïnspireerd door het werk van Monniaux over lineaire arithmetica.

De evaluatie gebruikte twee benchmarksets:

1. NRA Benchmarks: 83 aangepaste benchmarks uit de SMT-LIB 2024 repository (meti-tarski/Arthan, asin, zankl families).
2. Geometrische Benchmarks: 51 specificaties die 2D- en 3D-geometrische relaties modelleren (cirkels, ringvormige gebieden, hyperbolen).

Belangrijkste Resultaten:

• NQSynth loste 59 van de 83 NRA-benchmarks en 33 van de 51 geometrische benchmarks op binnen een time-out van 120 seconden.
• Daarentegen loste QEPCAD+CVC5 26 NRA- en 16 geometrische benchmarks op, terwijl ModEnum 23 NRA- en 11 geometrische benchmarks oploste.
• Opmerkelijk is dat NQSynth succesvol programma's synthetiseerde voor veel specificaties die niet realiseerbaar waren (of waarbij de zwakste preconditie moeilijk te berekenen was), een scenario waar SyGuS-tools volledig falen.
• De experimenten benadrukten dat de primaire bottleneck voor NQSynth de stap van quantieleliminatie (QEPCAD) was, met name voor grotere invoer, en niet de synthese-logica zelf.

Betekenis en Claims
Het artikel claimt een nieuwe techniek toe te voegen aan het arsenaal van programmasynthese uit NRA-specificaties. De primaire betekenis ligt in:

1. Omgaan met Niet-Realiseerbaarheid: Het biedt een praktische methode om programma's te synthetiseren die op een elegante manier omgaan met invoer waarvoor geen oplossing bestaat, een capaciteit die ontbreekt in de huidige state-of-the-art SyGuS-tools.
2. Rationale Precisie: Door te richten op rationale invoer en uitvoer, worden afrondingsfouten geassocieerd met zwevend-kommawiskunde vermeden, waardoor wiskundige correctheid wordt gewaarborgd voor toepassingen die hoge precisie vereisen.
3. Voorbij SyGuS: De aanpak lost problemen op die buiten het bereik van bestaande SyGuS-tools liggen, zelfs voor realiseerbare specificaties, door gebruik te maken van getaltheoretische eigenschappen (RRT en RRI) in plaats van uitsluitend te vertrouwen op syntactische zoekopdrachten of standaard quantieleliminatie.

De auteurs concluderen dat hoewel een algemeen volledige oplossing theoretisch onwaarschijnlijk is vanwege de moeilijkheid van $HTP_{\mathbb{Q}}$, hun correcte en onvolledige procedure een robuuste praktische oplossing biedt die bestaande methoden op een breed scala aan benchmarks aanzienlijk overtreft. Voor toekomstig werk wordt voorgesteld om de omstandigheden te onderzoeken waaronder loop-vrije programma's voldoende zijn en om de afhankelijkheid van zware quantieleliminatie-engines te verminderen.