O artigo Stepwise, assinado por Baoding He e outros seis autores, apresenta uma estrutura de busca de provas neuro-simbólica voltada à verificação automatizada de sistemas. Submetido em 20 de março de 2026 e disponibilizado no repositório arXiv, o estudo descreve um método que combina modelos de linguagem de grande porte com ferramentas de prova interativa para reduzir o trabalho manual na construção de provas formais, com foco em projetos de verificação em nível de sistema. De acordo com informações do arXiv, a proposta foi avaliada no benchmark FVEL seL4 e em outros desenvolvimentos em Isabelle.
Segundo o resumo do artigo, a verificação formal por meio de prova interativa tem sido usada para assegurar a correção de sistemas críticos, mas a elaboração de scripts de prova de grande porte ainda depende fortemente de trabalho manual, o que limita a escalabilidade. Os autores argumentam que os avanços recentes dos modelos de linguagem, especialmente em raciocínio matemático, tornam mais promissora sua integração à verificação de software. No Brasil, esse tipo de tecnologia tem relevância para áreas que dependem de software confiável, como serviços financeiros, infraestrutura digital e sistemas públicos, onde falhas podem afetar operações em larga escala.
Como o método Stepwise funciona?
O framework descrito no trabalho realiza uma busca em árvore do tipo best-first — expressão em inglês usada para um método que prioriza primeiro os caminhos considerados mais promissores — sobre estados de prova. Nesse processo, um modelo de linguagem é consultado repetidamente para sugerir o próximo passo candidato da prova. No lado neural, os autores afirmam ter ajustado modelos de linguagem com conjuntos de dados formados por pares de estado de prova e etapa de prova.
No lado simbólico, o sistema incorpora diferentes ferramentas de prova interativa para reparar etapas rejeitadas, filtrar e ranquear estados de prova e descarregar automaticamente subobjetivos quando o progresso da busca fica estagnado. De acordo com o texto, essa combinação permite uma adaptação mais eficiente dos modelos e uma poda do espaço de busca orientada pela semântica.
- Busca em árvore do tipo best-first sobre estados de prova
- Consultas repetidas a modelo de linguagem para sugerir passos
- Ajuste fino com pares de estado e etapa de prova
- Uso de ferramentas de ITP para reparar, filtrar e ranquear
- Automação de subobjetivos quando a busca perde avanço
Quais ferramentas e bases de teste foram usadas?
Os autores informam ter implementado o framework em um novo REPL de Isabelle, descrito como capaz de expor estados de prova detalhados e ferramentas de automação. Isabelle é um assistente de provas usado em verificação formal, área que busca demonstrar matematicamente que um software ou sistema atende a determinadas propriedades. A avaliação foi feita no benchmark FVEL seL4 e em outros desenvolvimentos na mesma linguagem de prova.
No caso do seL4, o artigo afirma que o sistema conseguiu provar até 77,6% dos teoremas. O resumo também diz que esse resultado supera abordagens anteriores baseadas em modelos de linguagem e o uso isolado do Sledgehammer, além de resolver significativamente mais provas com múltiplas etapas.
O que os resultados indicam, segundo os autores?
De acordo com o resumo, os resultados obtidos em benchmarks adicionais apontam para forte capacidade de generalização. Com base nisso, os autores sustentam que a abordagem pode representar um caminho viável para ampliar a verificação automatizada de software em escala.
O texto disponibilizado pelo arXiv não detalha, além do resumo, métricas complementares, limitações experimentais ou comparações metodológicas mais extensas. Ainda assim, a descrição apresentada destaca uma linha de pesquisa que tenta combinar raciocínio estatístico de modelos de linguagem com restrições formais de ferramentas simbólicas para atacar um dos principais gargalos da verificação formal: a dificuldade de produzir provas longas e complexas com baixo grau de intervenção humana. Para o cenário brasileiro, o tema dialoga com o avanço do uso de inteligência artificial no desenvolvimento de software e com a demanda por maior segurança em sistemas críticos e aplicações corporativas.
Assinam o trabalho Baoding He, Zenan Li, Wei Sun, Yuan Yao, Taolue Chen, Xiaoxing Ma e Zhendong Su. O artigo está classificado na área de Inteligência Artificial do arXiv sob o identificador 2603.19715.
