ProofOfThought: raciocínio baseado em LLM com provas de teoremas do Z3

• ProofOfThought combina modelos de linguagem de grande porte (LLMs) com o provador de teoremas Z3 para oferecer um raciocínio poderoso e interpretável
• Este projeto fornece resultados de raciocínio precisos e confiáveis para consultas em linguagem natural
• Por meio de uma API Python de alto nível, desenvolvedores podem implementar e testar com facilidade tarefas complexas de raciocínio
• Com o Z3DSL, também oferece acesso a uma DSL de baixo nível baseada em JSON, permitindo customização flexível
• Sua publicação no Sys2Reasoning Workshop NeurIPS 2024 demonstra as vantagens práticas da aplicação de pesquisas recentes

---

Introdução ao projeto open source ProofOfThought

ProofOfThought é uma biblioteca open source de raciocínio que adota uma abordagem de síntese de programas neuro-simbólica ao combinar modelos de linguagem de grande porte (LLMs) com o provador de teoremas Z3. Seu valor é importante tanto para uso prático quanto para pesquisa por fornecer resultados de raciocínio robustos e interpretáveis para problemas complexos do mundo real.

Por ser open source, qualquer pessoa pode utilizá-lo livremente em pesquisa, serviços e desenvolvimento, e ele tem a vantagem de tornar mais fácil validar o processo de raciocínio e interpretar erros em comparação com sistemas de raciocínio baseados apenas em LLM. Em relação a outros sistemas, sua grande característica é a transparência estrutural de linguagem natural de entrada → conversão automática para programa lógico → raciocínio baseado em Z3.

Arquitetura do sistema e principais componentes

• API de alto nível (z3dsl.reasoning) :

  • Execução de consultas de raciocínio baseadas em linguagem natural
  • Fornece uma interface Python fácil de aplicar até para iniciantes

• DSL de baixo nível (z3dsl) :

  • Permite acesso ao provador de teoremas Z3 com base em JSON
  • Vantajosa para customizações complexas e construção de pipelines automatizados

Exemplos de principais funcionalidades

• O LLM converte a consulta recebida em uma fórmula lógica (programa simbólico)

• Por meio do provador Z3, gera resultados verdadeiro/falso (yes/no) ou interpretações baseadas em condições

• Exemplo:

  • Consulta: "Nancy Pelosi condenaria publicamente o aborto?"
  • Resultado: False (não)

• Fornece um pipeline de avaliação (EvaluationPipeline):

  • Permite avaliação em lote sobre grandes conjuntos de dados
  • Geração automática de relatórios, incluindo acurácia

Aplicações e casos de uso

• Automação de benchmarks de raciocínio para fins de pesquisa
• Serviços de prova automática para grafos de conhecimento baseados em LLM ou problemas de lógica de ordem superior
• Potencial para aplicação em diversos serviços de IA, como consultas complexas de políticas públicas e classificação automática de debates em linguagem natural

Significado acadêmico e características

• Apresentado no workshop Sys2Reasoning da NeurIPS 2024
• Confiabilidade baseada em interpretação simbólica para complementar as limitações existentes dos LLMs (incerteza no raciocínio)
• A transparência dos resultados e dos fundamentos do raciocínio é um grande diferencial para o desenvolvimento de serviços reais

Conclusão

ProofOfThought combina os pontos fortes dos LLMs e do provador de teoremas Z3 para oferecer valor prático a desenvolvedores e pesquisadores que desejam construir uma infraestrutura de raciocínio em IA robusta e interpretável. A licença e a estrutura do projeto foram desenhadas para se adequar ao ecossistema open source, tornando-o atraente tanto para pesquisa acadêmica quanto para uso industrial.

[GN⁺]

Opiniões no Hacker News

• Compartilha uma experiência interessante com o Gemini 2.5 Pro. Ao tentar resolver um sistema de equações em um CAS online, o CAS não funcionou como esperado, então pediu ajuda ao Gemini, que apresentou diretamente a solução. Explicou que usou o pacote sympy do Python. Compartilha a impressão de que a combinação entre um LLM ambíguo e ferramentas rígidas pode gerar um efeito poderoso
  • Parece algo parecido com os humanos. Somos ruins em cálculos complexos, mas criamos computadores incríveis para fazê-los bem. E, depois de um enorme esforço, também criamos programas que, com base em cálculo numérico, fazem previsão de texto de forma razoável, mas continuam ruins em cálculos difíceis. No fim, esse programa passa a conseguir prever como criar e usar programas que são bons em cálculo numérico
  • Gosta muito da combinação de LLM com sympy para matemática. Se o LLM escrever o código em sympy, dá para confiar que a manipulação simbólica foi feita corretamente. O próprio código permanece como artefato, podendo ser corrigido e melhorado de forma incremental por humanos ou por LLMs, além de poder ser gerenciado com histórico do git etc. A confiança na exatidão matemática é mantida por meio de testes e validações. Também usa funções auxiliares para converter facilmente de código sympy para LaTeX. Trabalhos matemáticos recentes relacionados ao experimento de quantum eraser também foram feitos dessa forma. link do github
  • Entende que acompanhar com o LLM o processo de resolução de problemas com ferramentas é um bom método. Na prática, funcionou melhor do que esperava. Mas, em vez de induzir o LLM a fazer matemática, deixar de usar um CAS seria como fazer uma mudança de apartamento indo e voltando várias vezes de ônibus em vez de usar um caminhão de carga. Isso mesmo já tendo passe de ônibus
• Enfatiza que LLMs são, no fim das contas, modelos estatísticos de linguagem. Pela experiência, gerar programas lógicos, especialmente código-fonte em Prolog, funciona melhor do que o esperado. Talvez porque o Prolog tenha sido aplicado ao processamento simbólico de linguagem natural e também haja muitas amostras correspondentes no dataset de treinamento. Vale considerar usar a sintaxe Datalog do Z3 em vez da sintaxe SMTLib. Recomenda ver a demo relacionada e a sintaxe Datalog do Z3
  • A sintaxe Datalog no Z3 é muito boa. Usamos SMT no artigo sobre grammars porque era a opção com maior compatibilidade com vários solvers. Mas testamos durante a revisão da NeurIPS que essa abordagem também funciona bem com PROLOG. Espera-se que também funcione com Datalog. link do artigo, exemplo de datalog
• Acha que é uma abordagem interessante. A equipe deles também criou um protótipo parecido para codificar políticas operacionais de negócios em LEAN. O LLM primeiro converte a base de conhecimento de uma wiki interna ou do Google Docs em código LEAN. Depois executa um solver para verificar consistência. Quando a wiki é modificada, todo o processo roda novamente, funcionando como uma espécie de linter de processo. No entanto, como a própria conversão para LEAN exigia revisão de engenheiros, o projeto ficou na fase de protótipo. Mesmo assim, parece promissor para domínios que exigem compliance jurídico e financeiro
  • Menciona que a barreira da formalização automática é realmente alta. Compartilha a experiência de ter quantificado e analisado, no artigo deles da NeurIPS 2025, a incerteza da formalização automática sobre uma gramática bem definida. link do artigo Se quiser discutir em mais detalhes, pode entrar em contato a qualquer momento
  • Para quem estiver se perguntando o que é LEAN: é o Lean Theorem Prover, criado pela Microsoft. link do projeto
  • Fica curioso por exemplos reais. Gostaria de ouvir que tipo de política, no mundo real, é descrita com precisão suficiente para ser definida em LEAN
  • Parece muito útil o fato de essa abordagem permitir identificar de forma sistemática diretrizes contraditórias
• É uma área de pesquisa muito interessante. Alguns anos atrás, usou motores de raciocínio baseados em lógica e probabilidade para verificar se as premissas realmente levavam às conclusões. Também usou agents para sintetizar, formalizar e criticar conhecimento de domínio. Não é bala de prata, mas foi possível garantir certo nível de precisão. Acredita que algum grau de simbolismo e o conceito de agent-as-a-judge são promissores para o futuro. artigo de referência
  • Leu esse trabalho. Muito legal. Também teve recentemente a experiência de criar um agente de autoformalization no AWS ARChecks. Ainda não é público, mas já existem produtos disponíveis para uso geral que podem servir de referência blog da AWS
  • Considera que usar Agent/LLM como juiz traz viés e serve apenas para bootstrapping. Quando o desempenho sobe o suficiente, o juiz LLM acaba virando um limitador artificial, então no fim é preciso migrar para juízes humanos especialistas ou oráculos determinísticos
• Menciona que o knife-edge rolling kernel do RHEL foi usado no proof of concept
• Sentiu falta de explicações mais detalhadas no repositório, embora isso possa ser porque ele serve como artefato complementar do artigo. Essencialmente, parece ser uma API que tenta fazer o LLM gerar programas em Z3. A ideia é induzi-lo a expressar consultas do mundo real de forma lógica, capturando fatos, regras de inferência e objetivos. A função de supervisão seria permitir ler diretamente a especificação lógica e executar o solver para verificar se algo é verdadeiro ou falso. Os pontos que geram dúvida são: quem vai ler manualmente as regras SMT e compará-las com a perspectiva do mundo real, quem valida os valores constantes e como evitar que o LLM adicione, por engano ou para atingir o objetivo, regras desalinhadas com a lógica ou com a realidade. O artigo registrou 51% de false positive em benchmarks lógicos, o que parece surpreendentemente alto e sugere que o LLM é fraco em modelagem lógica ou gera regras incompletas. A avaliação é fraca e não explica claramente por que isso acontece
  • Afirma que este artigo foi escrito no ano passado com GPT-4o, e que a situação melhorou bastante com modelos mais recentes. Por exemplo, na pesquisa recente, na Tab 1, compara-se o desempenho baseado em texto com o baseado em SMT. O o3-mini alinha bem os resultados de text reasoning e SMT. No produto comercial AWS Automated Reasoning Checks, cria-se o modelo do domínio, valida-se esse modelo e, na etapa de geração de respostas, pares de perguntas e respostas do LLM passam por verificação rígida por solver para confirmar se seguem a política. Com isso, enfatiza-se que é possível garantir mais de 99% de validade relacionada à política nos pares de Q/A blog da AWS
• Pergunta se a interpretação dele está correta. Se a estrutura é que a saída probabilística produzida pelo LLM vai para um modelo lógico, expressa a suspeita de que isso não seria apenas “entra lixo, sai lixo” no fim das contas
  • A lógica formal faz o papel de filtro. Ou seja: “entra lixo, sai lixo filtrado”. Usa a analogia de que a evolução também envolve mutações aleatórias “ruins” sendo filtradas pelo ambiente natural
  • Afirma que nem sempre sai “lixo”. Com bastante frequência saem resultados úteis, e isso já faz valer a pena
  • Diz que isso é uma avaliação subjetiva. Afinal, tudo que a humanidade produziu ao longo de milhares de anos também poderia ser considerado lixo. Se for por esse lado, talvez viver em cavernas fosse mais simples
• Acha muito interessante o fato de a IA não apenas “pensar”, mas deixar um diário verificável. É como um filósofo vivendo com um tabelião criptográfico ao lado. Trabalho realmente impressionante
• A ideia central é que o LLM esboça o processo de raciocínio de forma estruturada, em um DSL JSON, e isso é então convertido de maneira determinística para lógica de primeira ordem, tentando obter uma prova no Z3. Assim, a saída final é uma conclusão demonstrável (ou um contraexemplo), o que a diferencia de uma simples cadeia de texto apenas convincente
• Pesquisa interessante. Foi ao repositório por curiosidade para ver exemplos de DSL, mas teve dificuldade de encontrar exemplos claros. Seria bom haver um snippet de código de exemplo no README
  • Agradece o interesse e diz que vai adicionar isso em breve. Enquanto isso, o artigo traz várias explicações de cenários a partir da página 11 PDF do artigo