64 artigos
Este artigo apresenta o novo solver upCoP, que combina estratégias de saturação e redução de objetivos em cálculos de conexão de lógica de primeira ordem através de codificações SAT com quebra de simetria para avançar a automação de provas.
Este artigo introduz as "grupos de comutação" e as "palavras contextuais" como estruturas algébricas para analisar e caracterizar a contextualidade independente de estado, fornecendo representações unitárias e construções explícitas de atribuições de valores não-contextuais.
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 estabelece, através de verificação formal em Lean 4 e validação externa com TTT2, uma barreira de impossibilidade para medidas composicionais diretas na orientação de recursores duplicadores de passos em sistemas de reescrita, demonstrando como métodos baseados em projeção superam essa limitação e fornecendo uma cadeia completa de certificação para um cálculo mínimo de teste.
Este artigo apresenta o MPBMC, uma abordagem híbrida que utiliza embeddings de redes neurais gráficas e estatísticas de tempo de execução para agrupar funcionalmente propriedades de hardware, acelerando significativamente a verificação formal por meio de Model Checking Limitado (BMC) em benchmarks do HWMCC.
Este artigo investiga a preservação de propriedades como completude de Kripke e decidibilidade nas fusões independentes de lógicas modais de primeira ordem de uma variável, demonstrando que tais propriedades são mantidas sem igualdade, mas falham na presença de igualdade e constantes não rígidas devido a uma codificação de equações diofantinas, enquanto a propriedade do modelo finito é preservada apenas no caso local.
Este trabalho apresenta axiomatizações completas da divergência de Kullback-Leibler e das divergências de Rényi de ordem arbitrária, utilizando uma linguagem gráfica de diagramas de corda enriquecida com equações quantitativas para estudar a entropia relativa como um enriquecimento quantitativo de categorias de matrizes estocásticas sob estruturas monoidais de produto de Kronecker e soma direta.
Este artigo apresenta uma revisão sistemática de fragmentos restritos de lógicas proposicionais e modais, analisando como sua expressividade e complexidade computacional dependem dos operadores permitidos, integrando abordagens baseadas em reticulados de Post e frameworks de conectivos modais, além de discutir resultados sobre aprendibilidade e identificar problemas em aberto.
Este artigo introduz as lógicas modais construtivas e , demonstrando que ambas são completas em EXPTIME e possuem a propriedade de modelo finito exponencial, o que resolve a conjectura de Afshari et al. para seu fragmento sem diamante e permite a incorporação das lógicas e com complexidade de validade em EXPTIME.
Este artigo apresenta uma abordagem de aprendizado de restrições para reduzir o excesso de retrocesso na busca de provas no cálculo de conexão de primeira ordem, mantendo a completude em calculistas de tabela não confluentes.
Este artigo apresenta uma nova abordagem para resolver equações de string, estendendo as transformações de Nielsen através da combinação de um operador de potência, generalizações das imagens de Parikh e decomposição de igualdade.
O artigo apresenta o NL2GDS, um framework inovador que utiliza modelos de linguagem grandes para traduzir descrições de hardware em linguagem natural em layouts GDSII completos via fluxo OpenLane, demonstrando reduções significativas em área, atraso e consumo de energia em benchmarks padrão.
Este trabalho apresenta a linguagem SCORE e demonstra, com auxílio de um assistente de prova, como interpretar suas operações de pilha como bijeções totais, permitindo que todos os termos do modelo computacional sejam vistos como bijeções totais em vez de parciais.
Este artigo introduz uma nova teoria equacional para o cálculo I baseada em "árvores Ohana", que preservam variáveis livres ocultas ou infinitas, e demonstra a compatibilidade dessa igualdade através de aproximações de programas, expansões de Taylor e um modelo denotacional não idempotente generalizado.
Este artigo apresenta o LeanTutor, um tutor de provas matemáticas baseado em IA que combina as capacidades de comunicação natural de modelos de linguagem com a correção verificável de provadores de teoremas, e introduz o PeanoBench como um novo conjunto de dados para avaliação.
Este trabalho propõe um novo quadro geométrico que modela o raciocínio de grandes modelos de linguagem como fluxos suaves no espaço de representações, demonstrando que o treinamento por previsão de próximo token permite a internalização de invariantes lógicos como geometria de ordem superior e desafia a visão de que esses modelos são meros "papagaios estocásticos".
O artigo apresenta o Strat2Rocq, uma abordagem que extrai estratégias de prova de modelos de linguagem para formalizá-las como lemas no Rocq, aumentando assim a taxa de sucesso dos provadores simbólicos e dos agentes de prova baseados em LLM.
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.
Este artigo apresenta uma metodologia escalável para verificação formal de aritmética de ponto flutuante em nível RTL, que utiliza uma estratégia de dividir e conquistar com refinamento guiado por contraexemplos e geração automatizada de propriedades por IA para superar as limitações dos modelos de alto nível e alcançar maior eficiência de cobertura.