27 artigos
Este artigo estabelece uma equivalência entre right actegories com objetos hom e right-enriched categories com copowers em bases monoidais não fechadas e não simétricas, generalizando resultados existentes para fornecer a base semântica necessária ao suporte de processos de ordem superior na linguagem concorrente CaMPL.
Este artigo apresenta o primeiro estudo em grande escala sobre o uso de aritmética de ponto flutuante em repositórios públicos do GitHub para linguagens estaticamente tipadas, analisando milhões de funções para validar benchmarks existentes e fornecer um novo conjunto de dados de 10 milhões de funções para orientar o desenvolvimento e a avaliação de futuras técnicas de raciocínio automatizado.
O artigo apresenta o Turn, uma linguagem de programação compilada e baseada em atores projetada para software autônomo, que introduz garantias de nível de linguagem para segurança de tipos em inferência de LLMs, controle de fluxo baseado em confiança, isolamento de contexto, gestão segura de credenciais e absorção de esquemas em tempo de compilação, superando as limitações das abordagens atuais que tratam esses invariáveis apenas como convenções de aplicação.
O artigo apresenta o Arbiter, um framework que combina regras de avaliação formal e varredura com múltiplos modelos de linguagem para detectar padrões de interferência em prompts de sistema de agentes de codificação, revelando vulnerabilidades críticas em ferramentas de grandes empresas e demonstrando que a arquitetura do prompt influencia o tipo de falha, mas não sua gravidade.
Este artigo formaliza o conceito de fatias idempotentes e apresenta um algoritmo eficiente em GSA para extraí-las, permitindo uma otimização de redução de tamanho de código que funde instruções não contíguas, alcançando reduções de até 7,24% em benchmarks específicos do LLVM.
O artigo apresenta o vLLM Hook, um plug-in de código aberto que permite o acesso e a modificação programática dos estados internos de modelos LLM no vLLM, habilitando funcionalidades como detecção de prompts maliciosos, aprimoramento de RAG e direcionamento de ativações.
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.
O artigo apresenta o PolyBlocks, uma infraestrutura de compilador modular baseada em MLIR para frameworks e chips de IA, que utiliza pipelines de passagens e modelos de custo analíticos para gerar automaticamente código de alto desempenho, demonstrando resultados competitivos com soluções como Torch Inductor e XLA em GPUs NVIDIA.
Este artigo propõe três abordagens complementares para superar as limitações das ferramentas atuais na documentação de atividades criativas, que frequentemente perdem a estrutura de exploração não linear, a intenção representacional e os limites de interação, ao apresentar interfaces baseadas em nós para gestão de artefatos de IA generativa, um vocabulário de sinais visuais para autoria de visualizações e um modelo de programação que incorpora histórias semânticas diretamente no estado de interação.
O artigo apresenta o EAGLE-Pangu, um sistema reprodutível que implementa decodificação especulativa em árvore segura para aceleradores em NPUs Ascend com backend Pangu, alcançando um aumento médio de 1,27x no throughput de decodificação em comparação com a decodificação greed-only do modelo professor.
Este artigo desenvolve uma teoria de especificações GSOS abstratas para linguagens de ordem superior, transferindo os princípios do framework de Turi e Plotkin para esse contexto e estabelecendo um resultado geral de composicionalidade que se aplica a sistemas como o cálculo SKI e o cálculo lambda.
O artigo apresenta a VyZX, uma biblioteca verificada que permite o raciocínio formal sobre linguagens gráficas indutivas, como o cálculo ZX para computação quântica, superando as limitações das ferramentas de prova tradicionais ao preservar a natureza diagramática e suas teorias equacionais, além de oferecer um visualizador integrado para facilitar a manipulação direta de diagramas.
O artigo apresenta o RightTyper, uma nova abordagem híbrida para inferência automática de tipos em Python que combina observações de execução real com análise estática e amostragem adaptativa para gerar anotações precisas e de alta qualidade com apenas 27% de sobrecarga de tempo de execução, superando significativamente os métodos puramente estáticos, dinâmicos ou baseados em IA.
Este artigo apresenta uma nova teoria de localidade totalmente simbólica que deriva polinômios de desempenho de cache para laços afins, permitindo previsões de movimentos de dados com 99,6% de precisão em menos de um milissegundo após uma análise inicial.
Este artigo apresenta uma introdução à teoria das categorias focada em aplicações à programação funcional, abordando álgebras iniciais para caracterizar tipos de dados e funções recursivas, bem como monads para modelar efeitos, e inclui diversos exercícios com soluções.
Este artigo apresenta os "Linear Layouts", uma abordagem inovadora que modela layouts de tensores usando álgebra linear sobre para permitir definições genéricas e conversões eficientes, otimizando a geração de código no Triton e reduzindo a complexidade do backend do compilador.
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 propõe a "edição estruturada híbrida", uma abordagem que permite aos criadores de ferramentas definir garantias estruturais sobre o código para facilitar a integração de ferramentas de programação, enquanto mantém aos usuários uma interface de edição de texto familiar e consistente.
Este artigo analisa os desafios e armadilhas específicas na implementação de máquinas virtuais no hardware CHERI, utilizando o caso de estudo da portabilidade do CRuby para identificar como suposições sobre comportamentos indefinidos do C em arquiteturas tradicionais causam falhas e para propor soluções validadas.
Este estudo avalia a eficácia de nove modelos de linguagem de última geração em um curso de programação funcional utilizando OCaml, apresentando três novos benchmarks (CodeGen, Repair e Explain) que revelam que, embora os modelos se destaquem na correção de erros e na explicação de conceitos, sua capacidade de resolver problemas de programação é significativamente menor nesse ambiente de baixa recursos em comparação com linguagens de alto recurso como Python e Java.