64 artigos
Este artigo investiga como propriedades fundamentais de monads de medidas de probabilidade, como leis de Kleisli, monoidalidade laxa e afinidade, emergem de suas apresentações como monads de codensidade, estabelecendo conexões com a teoria de categorias de Markov e caracterizando o monad de Radon e o monad de Giry sob essas condições.
Este artigo introduz um operado de diagramas de fiação direcionados dependentes para compor máquinas de Mealy e diagramas de estoque e fluxo, permitindo a conexão instantânea entre entradas e saídas enquanto evita ciclos, e estabelece uma semântica formal para esses diagramas através de um morfismo de álgebras para máquinas de Mealy.
Este artigo apresenta o Preguss, um framework modular que combina análise estática e modelos de linguagem para automatizar a geração e refinamento de especificações formais, permitindo a verificação de programas de grande escala com mais de 1000 linhas de código e reduzindo o esforço humano em até 88,9%.
O artigo apresenta uma metodologia de verificação formal escalável para circuitos de Estimativa de Fase Quântica (QPE) que utiliza abstração simbólica baseada em lógica de vetores de bits para verificar corretamente circuitos com mais de mil qubits usando menos de 3,5 GB de memória.
Este artigo estabelece explicitamente que o tamanho ótimo de um circuito varia no máximo em sob perturbações na tabela verdade, estendendo esse limite para distâncias de Hamming gerais e confirmando sua otimalidade para através de uma verificação exaustiva baseada em SAT.
O artigo apresenta o RoadLogic, uma ferramenta de código aberto que utiliza Programação em Conjuntos de Respostas, planejamento de movimento e monitoramento baseado em especificações para transformar automaticamente definições declarativas de cenários (OpenSCENARIO) em simulações executáveis e verificadas para testes de veículos autônomos.
Este artigo apresenta um novo quadro geral que estende a compilação de conhecimento em d-DNNF para o nível de SMT, permitindo consultas polinomiais em qualquer teoria através da combinação de fórmulas SMT com lemas teóricos pré-computados antes da compilação proposicional.
O artigo apresenta o BemaGANv2, um vocoder baseado em GAN aprimorado para geração de áudio de longo prazo, que substitui blocos Res por módulos AMP com função de ativação Snake e integra o Discriminador Multi-Envelope (MED) ao Discriminador Multi-Resolução (MRD) para otimizar a coerência temporal e a estrutura harmônica através de uma avaliação sistemática de estratégias de combinação de discriminadores.
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 formaliza a correspondência de Galois entre espaços de recobrimento e subgrupos do grupo fundamental na Teoria dos Tipos Homotópicos, desenvolvendo uma generalização n-dimensional e aplicando-a à classificação de recobrimentos de espaços de lentes e à construção da esfera de homologia de Poincaré.
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 compara três semânticas de satisfatibilidade para lógica quântica em dimensões fixas, demonstrando que a semântica padrão é estritamente mais expressiva que as semânticas de projetores comutantes globais e booleanos parciais locais, ao apresentar uma fórmula explícita que é satisfatível apenas na primeira.
O artigo descreve o experimento "Agent Hunt", que utiliza um mercado simulado baseado em recompensas para coordenar múltiplos agentes de LLM em uma busca colaborativa e descentralizada por provas e definições formais de topologia algébrica dentro de um ambiente de Prova Teórica Interativa.
O artigo apresenta o Twitch, uma ferramenta que descobre automaticamente abstrações (padrões de termos recorrentes) a partir de provas parciais ou bem-sucedidas para auxiliar o provador de teoremas equacionais Twee, resultando na prova de problemas de dificuldade rating-1 e em acelerações significativas em outros.
O artigo apresenta o LLM2SMT, um estudo de caso em que um agente de codificação baseado em LLM construiu, sem nenhuma intervenção humana, um solver SMT completo e competitivo para a lógica QF_UF, implementando o algoritmo de fechamento de congruência de Nieuwenhuis-Oliveras e emitindo provas em Lean.
O artigo apresenta o Elenchus, um sistema de diálogo que utiliza a interação entre um especialista humano e um modelo de linguagem para construir bases de conhecimento baseadas em semântica inferencialista, mapeando os estados dialéticos para a lógica NMMS e demonstrando sua eficácia na eliciação e verificação formal das tensões de design da ontologia PROV-O.
O artigo investiga o uso de redes neurais gráficas para prever ordens de ramificação iniciais em solucionadores SAT baseados em CDCL, demonstrando acelerações significativas em instâncias aleatórias e pseudo-industriais, embora o desempenho seja limitado em problemas industriais complexos devido à rápida sobrescrita das heurísticas dinâmicas do solucionador.
Este artigo apresenta as bases de dados orientadas a esboços, um quadro categórico que codifica paradigmas de bases de dados como esboços de limites finitos e modelos de conjuntos, ilustrando como características comuns de grafos são capturadas uniformemente, propondo regras de inferência para caminhos e introduzindo "esboços de vacilação" para facilitar a composição modular e o crescimento escalável de modelos.
Este artigo apresenta um método para a geração automatizada de exercícios de prova matemática em linguagem de primeira ordem, com níveis de complexidade comparáveis, utilizando tabelas analíticas livres de símbolos lógicos para capturar formalmente o esforço necessário para a resolução.
Este documento apresenta os anais da Oitava Conferência Internacional de Teoria de Categorias Aplicada, realizada em junho de 2025 na Universidade da Flórida, que reuniu contribuições de diversas disciplinas, incluindo ciência da computação, probabilidade, química e computação quântica, por meio de palestras plenárias, apresentações de pesquisadores júnior e demonstrações de software.