28 artigos
Este artigo estabelece uma conexão teórica fundamental entre complexidade computacional e arquiteturas de redes neurais, demonstrando que as RNNs lineares são altamente paralelizáveis por pertencerem à classe (semelhante aos Transformers), enquanto as RNNs não lineares enfrentam barreiras de paralelização ao resolverem problemas completos em ou .
Este artigo apresenta um algoritmo distribuído aleatório de uma rodada para 2-coloração de ciclos que reduz a fração esperada de arestas monocromáticas para abaixo de 0,24118 (com um limite inferior de 0,23879), superando os melhores resultados anteriores e tendo sua prova desenvolvida principalmente por modelos de linguagem grande e formalizada em Lean 4.
Este artigo investiga a complexidade do problema de alcançabilidade em VASS estendidos com contadores inteiros (VASS+Z), demonstrando que o problema é NP-completo para uma única variável não negativa, situando-se na classe para , e provando que a adição de contadores inteiros reduz significativamente a dimensão necessária para atingir complexidades PSPACE e TOWER em comparação com os VASS clássicos.
Este artigo caracteriza algebricamente a reversibilidade de autômatos celulares de primeiro grau sobre , estabelecendo três condições necessárias e suficientes que permitem verificar a reversibilidade global de qualquer regra desse tipo em tempo constante, independentemente do tamanho da rede.
Este artigo investiga a complexidade computacional do cálculo de alinhamentos em mineração de processos, demonstrando que o problema é PSPACE-completo para redes de Petri seguras, NP-completo para várias subclasses como árvores de processo e sistemas T, e solúvel em tempo polinomial apenas para sistemas S vivos e seguros.
Este artigo resolve uma questão aberta há mais de uma década ao apresentar um autômato de Büchi histórico-determinista com 65 estados que possui estritamente menos estados do que qualquer autômato de Büchi determinista equivalente, demonstrando assim a superioridade concisa dos primeiros.
Este artigo detalha a modelagem formal, verificação e teste do ambiente de execução de autômatos de contrato (CARE) utilizando a ferramenta Uppaal, demonstrando como essas técnicas melhoram a confiabilidade da aplicação distribuída de código aberto.
O artigo apresenta o SpotIt, um novo pipeline de avaliação para Text-to-SQL que utiliza verificação formal de equivalência para identificar diferenças entre consultas geradas e de referência que os métodos tradicionais baseados em testes poderiam ignorar.