28 artigos
O artigo apresenta o FATE, uma nova série de benchmarks em álgebra formal com níveis de dificuldade que vão de exercícios universitários a problemas além de exames de doutorado, revelando que os modelos de linguagem atuais têm desempenho significativamente inferior nessa tarefa de raciocínio matemático avançado em comparação com competições tradicionais.
Este artigo constrói autômatos para reconhecer relações em sequências -automáticas, estabelece uma relação entre a complexidade de subpalavras e a complexidade de estados de subsequências lineares, resolve uma questão recente sobre o formato de entrada mais significativo primeiro e analisa a complexidade computacional de tais construções usando aritmética de Büchi.
Este artigo apresenta uma abordagem que estende a mineração de especificações a tipos de dados mais ricos, unificando a síntese de transformações de dados e especificações temporais via TSL para gerar programas reativos com maior eficiência de amostragem e robustez em comparação a métodos tradicionais baseados em abstração booleana.
Este artigo investiga jogos em grafos concorrentes com n jogadores cooperativos que utilizam randomização distribuída (sem fonte de aleatoriedade compartilhada), demonstrando que estratégias sem memória são suficientes para o problema de limiar (NP-difícil e em ) e que o problema de quase-certeza é NP-completo, além de propor a lógica IRATL e um solver prático para essas questões.
Este artigo resolve a incompatibilidade entre a estrutura combinatória e o comportamento observável dos Autômatos de Dimensões Superiores (HDAs) ao desenvolver uma semântica independente da ordem dos eventos baseada em ipomsets de intervalo, estabelecendo isomorfismos categóricos e unificando noções de bisimulação para fornecer uma fundação coerente que elimina artefatos representacionais e conecta HDAs a outros modelos de concorrência.
Este artigo demonstra que a decidibilidade da limitação do número de viradas em autômatos de pilha e de um contador é indecidível, estabelece uma troca não recursiva entre diferentes classes de autômatos com restrições de viradas e prova a existência de uma hierarquia infinita de complexidade baseada em funções sublineares do número de viradas.
Este artigo investiga as árvores verdadeiramente livres de contexto, demonstrando que elas admitem uma descrição por autômatos não determinísticos de arestas múltiplas e que o problema de isomorfismo para árvores determinísticas é completo para a classe NL, tanto na versão enraizada quanto na não enraizada.
Este artigo demonstra novas propriedades da representação de inteiros, incluindo a prova de uma conjectura de Kimberling de 2012, com auxílio das ferramentas de prova automática Walnut e ChatGPT 5.
Este artigo propõe uma análise unificada da assimetria fundamental entre geração e reconhecimento em teoria das linguagens formais, identificando seis dimensões distintas (complexidade computacional, ambiguidade, direcionalidade, disponibilidade de informação, inferência de gramática e temporalidade) para demonstrar que a distinção clássica de "geração fácil, análise difícil" é enganosa e que a verdadeira assimetria reside no fato de que a análise é sempre restrita por uma entrada dada, enquanto a geração não necessariamente o é.
Este artigo demonstra que os fatores de palavras suaves são f-suaves e avança na conjectura de Sing sobre a complexidade das palavras f-suaves binárias, provando a fórmula assintótica para alfabetos pares, estabelecendo o limite inferior para qualquer alfabeto binário e melhorando o limite superior conhecido para alfabetos ímpares.
Este artigo apresenta o ZipLex, um framework verificado para análise léxica invertível e de tempo linear que garante que a lexagem e a impressão sejam inversas mútuas, superando as limitações de desempenho e de verificação de soluções anteriores como o Verbatim++ e o Coqlex.
Este artigo desenvolve uma abordagem baseada em dados para o controle supervisionário não bloqueante de sistemas a eventos discretos de modelo desconhecido, introduzindo e formalizando o conceito de "informatividade de dados de marcação" para verificar a viabilidade de projetar supervisores válidos e propondo algoritmos para lidar com casos de dados insuficientes através de restrições e informatização.
Este artigo estabelece fundamentos teóricos para a decodificação restrita a gramáticas, demonstrando que gramáticas linguisticamente equivalentes podem gerar custos de processamento drasticamente diferentes e propondo métricas de ambiguidade estrutural e limites inferiores para otimizar a eficiência em modelos de linguagem.
Este artigo demonstra que máquinas de Moore podem ser realizadas como modelos de espaço de estado (SSMs), propondo uma abordagem híbrida que utiliza o aprendizado de autômatos simbólicos para inicializar SSMs, resultando em uma convergência 2 a 5 vezes mais rápida e maior precisão em comparação com inicializações aleatórias.
Este artigo apresenta um framework de monitoramento online escalável e eficiente para Lógica Temporal Métrica (MTL), baseado na construção unificada de redes sequenciais que utilizam a técnica de marcação temporal futura para processar comportamentos em tempo discreto e denso.
Este artigo estabelece que a verificação de módulos em sistemas multiagentes de pilha (PMS) é completa para 2EXPTIME sob especificações ATL, mas atinge uma complexidade incomum de 4EXPTIME sob especificações ATL*, tornando-se exponencialmente mais difícil do que os problemas de verificação de modelos correspondentes.
Este artigo investiga teoremas do tipo Ramsey para árvores infinitas e ferramentas combinatórias relacionadas, aplicando-os ao problema de expansão de álgebras de árvores.
Este artigo apresenta uma abordagem para a condução autônoma que equilibra diversos riscos, como colisões e violações de regras, ao estender métricas de risco para cenários complexos definidos por Lógica Temporal Linear e reformular o problema de síntese de controle como um problema de alcançabilidade resolvido via programação linear.
Este artigo prova as conjecturas de Clark Kimberling sobre a sequência binária que ele definiu, estabelecendo sua relação com a palavra de Tribonacci e determinando sua complexidade de subpalavras e expoente crítico, utilizando o provador de teoremas Walnut.
Este artigo apresenta uma classificação completa da complexidade computacional distribuída de problemas de otimização local em ciclos direcionados, demonstrando que, para qualquer problema e razão de aproximação, a complexidade pertence a uma de quatro classes específicas e pode ser determinada automaticamente por um meta-algoritmo eficiente que também sintetiza algoritmos distribuídos assintoticamente ótimos.