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

Resumo Técnico: Síntese de Programas para Aritmética Real Não-Linear: Indo Além da Realizabilidade

Definição do Problema
Este artigo aborda o problema de sintetizar programas a partir de especificações na teoria livre de quantificadores da Aritmética Real Não-Linear (NRA). Ao contrário da Síntese Guiada por Sintaxe (SyGuS) tradicional, que falha quando uma especificação é "irrealizável" (ou seja, existem valores de entrada para os quais nenhuma saída satisfaz a especificação), este trabalho propõe um novo objetivo de síntese. O objetivo é sintetizar um programa que, para qualquer entrada racional, produza uma saída racional que satisfaça a especificação ou reporte explicitamente a inexistência de tal saída (denotada por $\bot$).

Para evitar erros de arredondamento inerentes à aritmética de ponto flutuante de precisão fixa, que podem fazer com que soluções reais válidas falhem ao serem avaliadas com aproximações, os autores restringem o domínio a entradas e saídas racionais. Isso define a classe de problemas RPSQ (Síntese de Programas Reais com entradas e saídas racionais). Os programas sintetizados são permitidos a conter loops, condicionais e atribuições, operando sobre números racionais.

Dureza Teórica e Limitações
Os autores estabelecem limites teóricos significativos para este problema:

1. Inter-reduzibilidade com o Décimo Problema de Hilbert: Eles provam que o RPSQ é inter-reduzível com o Décimo Problema de Hilbert sobre os racionais ($HTP_{\mathbb{Q}}$). Como $HTP_{\mathbb{Q}}$ é um problema em aberto de longa data na teoria dos números, isso implica que é improvável que exista um algoritmo de síntese geral, correto e completo para o RPSQ.
2. Impossibilidade de Síntese sem Loops: O artigo demonstra que o RPSQ não pode ser resolvido usando apenas programas sem loops. Se uma solução sem loops existisse, isso implicaria que a teoria da aritmética racional admite eliminação de quantificadores, um resultado conhecido por ser indecidível (Robinson, 1959).

Metodologia e Algoritmos
Dada a indecidibilidade geral, os autores propõem uma abordagem em camadas:

1. Realizabilidade sobre Reais vs. Racionais: Eles mostram que, se uma especificação for realizável sobre os reais, qualquer programa sintetizado por ferramentas SyGuS existentes (que operam sobre os reais) também serve como uma solução válida para o caso racional, desde que as entradas e saídas sejam racionais. No entanto, isso não se mantém no sentido inverso; uma solução para racionais não implica necessariamente uma solução para os reais.

2. Algoritmo Correto e Completo para Saída Única ($|Y|=1$): Para especificações com uma única variável de saída, os autores apresentam um algoritmo correto e completo (Algoritmo 1). Esta abordagem separa o problema em dois casos:

   • Desigualdades Estritas: Utiliza Isolamento de Raízes Reais (RRI) para encontrar intervalos onde o sinal dos polinômios é invariante. Ao amostrar pontos racionais dentro desses intervalos (explorando a densidade dos racionais nos reais), encontra soluções para restrições estritas.
   • Desigualdades Não-Estritas: Para soluções que residem na fronteira (onde desigualdades não-estritas tornam-se igualdades), o algoritmo emprega o Teorema da Raiz Racional (RRT). Isso permite a enumeração de um conjunto finito de candidatos a raízes racionais para as equações polinomiais derivadas das condições de fronteira.
     O algoritmo combina esses métodos com Eliminação de Quantificadores (usando QEPCAD) para determinar as pré-condições mais fracas para a existência de soluções.

3. Algoritmo Correto mas Incompleto para o Caso Geral ($|Y|>1$): Para múltiplas variáveis de saída, os autores propõem o Algoritmo 2 (implementado na ferramenta NQSynth). Este é um procedimento correto mas incompleto que decompõe iterativamente o problema de múltiplas saídas em sub-problemas de saída única:

   • Consulta um oráculo NRA (Z3) para encontrar uma atribuição satisfatória racional (modelo).
   • Fixa todas as variáveis de saída, exceto uma, com base neste modelo, reduzindo o problema a uma instância de síntese de saída única solucionável pelo algoritmo completo descrito acima.
   • Constrói uma lista de decisão (uma série de ramificações if-then-else) onde cada ramo corresponde a uma pré-condição específica derivada via eliminação de quantificadores.
   • O processo se repete, refinando a especificação negando as pré-condições das soluções encontradas, até que a especificação se torne insatisfatível ou ocorra um tempo limite.

Implementação e Resultados Experimentais
Os autores implementaram sua abordagem em uma ferramenta protótipo chamada NQSynth. Eles a avaliaram contra duas abordagens concorrentes:

• QEPCAD+CVC5: Um pipeline SyGuS modificado que primeiro calcula a pré-condição mais fraca sobre os reais e depois sintetiza um programa.
• ModEnum: Uma abordagem baseada em enumeração de modelos inspirada no trabalho de Monniaux sobre aritmética linear.

A avaliação utilizou dois conjuntos de benchmarks:

1. Benchmarks NRA: 83 benchmarks adaptados do repositório SMT-LIB 2024 (famílias meti-tarski/Arthan, asin, zankl).
2. Benchmarks Geométricos: 51 especificações modelando relações geométricas 2D e 3D (círculos, regiões anulares, hipérboles).

Resultados Chave:

• O NQSynth resolveu 59 dos 83 benchmarks NRA e 33 dos 51 benchmarks Geométricos dentro de um tempo limite de 120 segundos.
• Em contraste, o QEPCAD+CVC5 resolveu 26 benchmarks NRA e 16 Geométricos, enquanto o ModEnum resolveu 23 benchmarks NRA e 11 Geométricos.
• Notavelmente, o NQSynth sintetizou com sucesso programas para muitas especificações que eram irrealizáveis (ou onde a pré-condição mais fraca era difícil de calcular), um cenário onde as ferramentas SyGuS falham completamente.
• Os experimentos destacaram que o principal gargalo para o NQSynth foi a etapa de eliminação de quantificadores (QEPCAD), particularmente para entradas maiores, e não a própria lógica de síntese.

Significado e Alegações
O artigo afirma adicionar uma técnica nova ao repertório de síntese de programas a partir de especificações NRA. Seu significado principal reside em:

1. Tratamento da Irrealizabilidade: Fornece um método prático para sintetizar programas que lidam graciosamente com entradas para as quais nenhuma solução existe, uma capacidade ausente nas ferramentas SyGuS atuais de última geração.
2. Precisão Racional: Ao visar entradas e saídas racionais, evita os erros de arredondamento associados à aritmética de ponto flutuante, garantindo correção matemática para aplicações que exigem alta precisão.
3. Além do SyGuS: A abordagem resolve problemas que estão além do alcance das ferramentas SyGuS existentes, mesmo para especificações realizáveis, ao explorar propriedades da teoria dos números (RRT e RRI) em vez de depender exclusivamente de busca sintática ou eliminação de quantificadores padrão.

Os autores concluem que, embora uma solução completa geral seja teoricamente improvável devido à dureza de $HTP_{\mathbb{Q}}$, seu procedimento correto e incompleto oferece uma solução prática robusta que supera significativamente os métodos existentes em uma ampla gama de benchmarks. Trabalhos futuros são sugeridos para investigar condições sob as quais programas sem loops são suficientes e para reduzir a dependência de motores pesados de eliminação de quantificadores.