O artigo introduz o Lean4Agent, uma estrutura que utiliza Lean4 para modelagem e verificação formal do comportamento de agentes, especialmente em fluxos de trabalho multi-etapas orientados por LLMs. Ele visa abordar a falta de métodos formais nos sistemas de agentes atuais, permitindo verificações de consistência semântica e a localização de falhas em tempo de execução.
Esta pesquisa introduz uma estrutura inovadora de aprendizado para refinar, visando superar o alto custo computacional de LLMs na prova formal de teoremas. Ao explorar como os compiladores compactam diversas tentativas de prova em modos de falha estruturados, o método permite uma exploração de provas eficiente e correção local de erros, amplificando significativamente as capacidades de raciocínio dos provadores base.
Este trabalho apresenta uma estrutura formalmente verificada para análise de patentes, utilizando um pipeline híbrido de IA e Lean 4. É a primeira aplicação conhecida da prova de teorema interativa para a análise de propriedade intelectual, superando as limitações dos métodos existentes.
Este é um esboço v0.0 do artigo 'Rei as a Formal-Verification Compilation Pass for AI-Generated Mathematics', que detalha a proposta de Rei como uma passagem de compilação para verificação formal de hipóteses geradas por IA. A validação atual está em fase de teste inicial, com uma demonstração completa ainda pendente para a promoção da versão 0.1.
Este artigo apresenta uma semântica algébrica para execução governada, baseada em árvores de interação e coindução parametrizada, com uma implementação mecanizada em Rocq. O framework introduz uma GovernanceAlgebra que gera uma categoria monoidal simétrica e um sistema de efeitos algébricos que garante handlers que preservam a governança.
Este artigo propõe BODHI, um método de prompt de conhecimento de domínio para inferência de especificação do kernel do sistema operacional, visando superar as limitações atuais dos LLMs. Ele aumenta o prompt few-shot com um guia de tradução C para Python, melhorando a automação e a precisão das especificações.
Esta pesquisa introduz os Transformers Verificáveis, uma estrutura para converter circuitos de Transformer localizados por tarefa em afirmações limitadas e verificáveis por solver. Permite a verificação de propriedades como equivalência funcional e robustez através de codificação SMT direta ou mediada por substituto.
NeuroNL2LTL é uma arquitetura neurosimbólica que une a tradução aprendida com a verificação formal para converter linguagem natural em Lógica Temporal Linear. Ele utiliza um treinamento com verificador no loop, onde os resultados da verificação servem como sinais de recompensa para o aprendizado por reforço, otimizando a correção formal.