Resumo Técnico: Aprendizado Ativo de Autômatos Ponderados Baseado em SMT

Declaração do Problema

O aprendizado ativo de autômatos, pioneiro no algoritmo $L^\star$ de Angluin, tornou-se uma técnica padrão para inferir modelos de componentes desconhecidos na verificação formal. Embora os métodos no estilo $L^\star$ sejam bem estabelecidos para autômatos Booleanos (determinísticos e não determinísticos), estendê-los para Autômatos Finitos Ponderados (WFAs) provou ser significativamente mais desafiador. Os WFAs generalizam os autômatos Booleanos ao atribuir pesos de um semianel às transições, permitindo a modelagem de propriedades quantitativas como custo, probabilidade e consumo de recursos.

As abordagens existentes para aprender WFAs baseiam-se em generalizações da matriz de Hankel ou da tabela de observação (por exemplo, $WL^\star$). Esses métodos exigem raciocínio sobre a estrutura algébrica do semianel subjacente. Consequentemente, provar a terminação e a minimalidade é sutil e frequentemente restrito a classes algébricas específicas (por exemplo, corpos, domínios ideais principais). Para muitos semianéis relevantes na prática, como o semianel Tropical ou o semianel de Gargalo, as garantias de terminação são desconhecidas ou não garantem autômatos mínimos. Além disso, os algoritmos existentes frequentemente produzem modelos não mínimos ou falham em escalar efetivamente sobre semianéis infinitos.

Metodologia

Os autores propõem um algoritmo de aprendizado ativo baseado em restrições que formula o problema de aprendizado diretamente como um problema de satisfatibilidade solúvel por solucionadores SMT (Satisfiability Modulo Theories).

Abordagem Central

Em vez de refinar uma tabela de observação, o algoritmo constrói incrementalmente um sistema de equações sobre o semianel dado $S$. As soluções desse sistema correspondem exatamente a WFAs não determinísticos que concordam com o "professor" (a linguagem alvo) em todas as consultas observadas.

O processo de aprendizado segue um loop padrão de aprendizado ativo (Algoritmo 1):

1. Geração de Hipótese: O algoritmo tenta encontrar um WFA com $n$ estados que seja consistente com o conjunto de observações atual $O$. Isso é delegado a uma sub-rotina getAutomaton.
2. Consulta de Equivalência: Se uma hipótese consistente $H$ for encontrada, o professor é consultado para verificar se $H$ reconhece a linguagem alvo $L$.
3. Tratamento de Contraexemplo: Se o professor fornecer um contraexemplo $w$ (onde $H(w) \neq L(w)$), $w$ é adicionado a $O$, e o loop se repete com as restrições reforçadas.

A Sub-rotina getAutomaton

O artigo apresenta duas implementações para getAutomaton:

1. Base Ingênua: Codifica diretamente a semântica do WFA. Trata pesos iniciais, matrizes de transição e pesos finais como variáveis desconhecidas e resolve a equação $out(w) = \text{semântica}(w)$ para todo $w \in O$.
2. Otimizada (SWAL): Utiliza uma perspectiva coalgébrica e o conceito de linguagens de estado. Em vez de resolver diretamente para a linguagem global, introduz variáveis intermediárias representando a linguagem aceita a partir de cada estado. Isso resulta em um sistema de equações onde:
   • Restrições de estabilização garantem que as linguagens de estado sejam consistentes com os pesos de transição.
   • Restrições de abrangência garantem que os pesos iniciais combinem corretamente as linguagens de estado para corresponder à saída alvo.
   • Insight Chave: Embora essa codificação introduza mais variáveis e equações, ela expõe subestruturas compartilhadas (sufixos) entre as observações. Isso permite que os solucionadores SMT reutilizem resultados intermediários, melhorando significativamente a escalabilidade em comparação com a abordagem ingênua.

Decidibilidade e Semianéis

O algoritmo é paramétrico no semianel. Os autores identificam que, para semianéis decidíveis (onde a satisfatibilidade de sistemas finitos de equações é decidível), a sub-rotina getAutomaton pode ser implementada de forma sólida e completa.

• Semianéis Finitos: Decidíveis trivialmente via força bruta ou SMT.
• Semianéis Infinitos: O artigo fornece codificações para o semianel Tropical ($\min, +$), Semianéis Tropicais Limitados e o semianel de Gargalo ($\max, \min$) em teorias decidíveis como Aritmética Linear Inteira Livre de Quantificadores (QF-LIA) e Vetores de Bits Livres de Quantificadores (QF-BV).

Contribuições Principais

1. Algoritmo Inovador: Um novo algoritmo de aprendizado ativo baseado em SMT para WFAs não determinísticos que é paramétrico no semianel.
2. Garantia de Minimalidade: Diferentemente dos métodos no estilo $L^\star$, que frequentemente carecem de garantias de minimalidade fora de estruturas algébricas específicas, este algoritmo é garantido para produzir WFAs mínimos ao terminar, independentemente do semianel.
3. Condições de Terminação: Os autores provam correção parcial e fornecem condições suficientes para terminação. Especificamente, provam que o algoritmo termina para todos os semianéis finitos. Para semianéis infinitos, embora a terminação não seja teoricamente garantida pelos mesmos argumentos de cardinalidade, a implementação demonstra sucesso prático.
4. Síntese Baseada em Restrições: O artigo introduz o primeiro algoritmo de geração baseado em restrições para WFAs, habilitando a síntese baseada em SMT. Identifica semianéis específicos onde os sistemas de restrições resultantes são decidíveis.
5. Avaliação Experimental: Uma avaliação abrangente comparando o método proposto (SWAL) com uma base ingênua e o algoritmo de última geração $WL^\star$.

Resultados Experimentais

Os autores implementaram o algoritmo (SWAL) em OCaml usando o solucionador Z3 e o avaliaram em mais de 5.000 benchmarks gerados aleatoriamente nos semianéis Booleano, Tropical, Tropical Limitado e de Gargalo.

• vs. Base Ingênua: O SWAL supera significativamente a codificação ingênua tanto em tempo de execução quanto em escalabilidade. Enquanto a abordagem ingênua luta para aprender autômatos com mais de 2–6 estados (dependendo do semianel), o SWAL aprende com sucesso autômatos mínimos com até 8 estados. A codificação otimizada (linguagens de estado) reduz o número de tempos esgotados/erros de falta de memória em ordens de magnitude.
• vs. $WL^\star$: Quando comparado ao $WL^\star$ (um algoritmo de última geração para domínios ideais principais):
  • Minimalidade: O SWAL produz consistentemente autômatos mínimos, enquanto o $WL^\star$ frequentemente produz autômatos até 10 vezes maiores.
  • Eficiência: O SWAL requer menos consultas de saída (interações com o professor) do que o $WL^\star$.
  • Tempo de Execução: O SWAL é competitivo em tempo de execução, frequentemente terminando mais rápido e com menos falhas de recursos (TE/FMO) do que o $WL^\star$.
• Incrementalidade: Habilitar a resolução incremental de SMT reduz drasticamente o tempo de aprendizado e o uso de recursos, confirmando a adequação da abordagem baseada em restrições para aprendizado incremental.

Significado e Alegações

O artigo posiciona o aprendizado baseado em restrições como uma alternativa prática e robusta aos métodos tradicionais estilo Hankel/$L^\star$ para autômatos ponderados, particularmente em configurações orientadas à verificação.

• Robustez: A abordagem lida com uma gama mais ampla de semianéis (incluindo infinitos como o Tropical) onde as provas de terminação algébrica para métodos no estilo $L^\star$ são difíceis ou inexistentes.
• Minimalidade: A garantia de minimalidade é uma vantagem crucial, pois modelos mínimos são essenciais para verificação e abstração eficientes.
• Escalabilidade: Os resultados experimentais demonstram que a síntese baseada em SMT pode escalar para aprender autômatos ponderados complexos e mínimos que estão atualmente fora do alcance dos algoritmos existentes.

Os autores concluem que, embora não forneçam uma prova de terminação geral para todos os semianéis infinitos (um problema aberto conhecido), seu método oferece uma solução prática que aprende com sucesso WFAs mínimos em cenários onde métodos anteriores falham ou produzem modelos subótimos. Trabalhos futuros incluem explorar atualizações de hipóteses mais incrementais e estender a abordagem para autômatos probabilísticos.