ProofOfThought : raisonnement basé sur les LLM avec démonstration de théorèmes Z3

• ProofOfThought combine les grands modèles de langage (LLM) avec le démonstrateur de théorèmes Z3 pour offrir un raisonnement puissant et interprétable
• Ce projet fournit des résultats de raisonnement précis et fiables pour des requêtes en langage naturel
• Grâce à une API Python de haut niveau, les développeurs peuvent implémenter et expérimenter facilement des tâches de raisonnement complexes
• Avec Z3DSL, il propose aussi un accès à un DSL de bas niveau basé sur JSON, permettant une personnalisation flexible
• Sa publication au Sys2Reasoning Workshop NeurIPS 2024 illustre les bénéfices d’une mise en pratique de résultats de recherche récents

---

Présentation du projet open source ProofOfThought

ProofOfThought est une bibliothèque open source de raisonnement qui adopte une approche de synthèse de programmes neuro-symbolique combinant les grands modèles de langage (LLM) et le démonstrateur de théorèmes Z3. Sa capacité à fournir des résultats de raisonnement robustes et interprétables sur des problèmes complexes du monde réel lui confère une importance notable, tant en recherche que dans les usages concrets.

En tant que projet open source, il peut être librement utilisé par tous pour la recherche, les services ou le développement, et présente l’avantage de rendre la vérification du processus de raisonnement et l’interprétation des erreurs plus faciles que dans les systèmes de raisonnement basés uniquement sur les LLM. Par rapport à d’autres systèmes, sa grande particularité est sa transparence structurelle : entrée en langage naturel → conversion automatique en programme logique → raisonnement basé sur Z3.

Architecture du système et composants principaux

• API de haut niveau (z3dsl.reasoning) :

  • exécution de requêtes de raisonnement en langage naturel
  • interface Python facile à utiliser, y compris pour les débutants

• DSL de bas niveau (z3dsl) :

  • accès au démonstrateur de théorèmes Z3 via JSON
  • bien adapté à la personnalisation avancée et à la construction de pipelines d’automatisation

Exemples de fonctions principales

• Le LLM convertit la requête d’entrée en formule logique (programme symbolique)

• Le démonstrateur Z3 produit un résultat vrai/faux (yes/no) ou une interprétation conditionnelle

• Exemple :

  • requête : "Nancy Pelosi condamnerait-elle publiquement l’avortement ?"
  • résultat : False (non)

• Fournit un pipeline d’évaluation (EvaluationPipeline) :

  • évaluation par lots possible sur de grands jeux de données
  • génération automatique de rapports, notamment sur la précision

Cas d’application et usages

• Automatisation de benchmarks de raisonnement à des fins de recherche
• Services de preuve automatique pour des graphes de connaissances basés sur les LLM ou des problèmes de logique d’ordre supérieur
• Potentiel d’application dans divers services d’IA, comme les requêtes politiques complexes ou la classification automatique de débats en langage naturel

Apport scientifique et caractéristiques

• Présenté au workshop Sys2Reasoning de NeurIPS 2024
• Une fiabilité fondée sur l’interprétation symbolique qui compense les limites actuelles des LLM en matière d’incertitude du raisonnement
• La transparence des résultats et de leurs justifications, ainsi que leur interprétabilité, constituent un atout majeur pour le développement de services réels

Conclusion

ProofOfThought combine les atouts des LLM et du démonstrateur de théorèmes Z3 pour offrir une valeur concrète aux développeurs et chercheurs qui veulent construire une infrastructure de raisonnement IA robuste et interprétable. La licence et l’architecture du projet ont été conçues pour s’intégrer à l’écosystème open source, ce qui le rend attractif à la fois pour la recherche académique et les usages industriels.

[GN⁺]

Avis Hacker News

• Il raconte une expérience intéressante avec Gemini 2.5 Pro. En essayant de résoudre un système d’équations sur un service de CAS en ligne, le CAS ne s’est pas comporté comme prévu, alors il a demandé de l’aide à Gemini, qui a directement fourni la solution. Gemini a expliqué avoir utilisé le package sympy de Python. Il partage l’impression que la combinaison d’un LLM flou et d’un outil rigoureux peut produire un effet très puissant
  • Cela donne une impression proche de l’humain. Nous sommes faibles pour les calculs complexes, mais nous avons créé de formidables ordinateurs pour les effectuer. Puis, au prix d’un effort immense, nous avons aussi créé des programmes qui prédisent plus ou moins du texte à partir de calculs numériques, tout en restant maladroits pour les calculs difficiles. Au final, ce programme devient capable de prédire comment créer et utiliser un autre programme fort en calcul numérique
  • J’aime vraiment la combinaison LLM + sympy pour les mathématiques. Si on demande au LLM d’écrire du code sympy, on peut avoir confiance dans le fait que les manipulations symboliques sont correctes. Le code lui-même reste comme artefact, et peut être corrigé et amélioré progressivement par un humain ou par un LLM, tout en étant gérable via l’historique git, etc. La confiance dans l’exactitude mathématique est maintenue grâce aux tests et aux validations. J’utilise aussi des fonctions utilitaires pour convertir facilement le code sympy en LaTeX. J’ai récemment travaillé de cette manière sur les mathématiques liées à l’expérience du quantum eraser. lien GitHub
  • Il comprend que suivre avec un LLM, à l’aide d’outils, le processus de résolution d’un problème est une méthode acceptable. En pratique, cela a même mieux marché que prévu. Mais éviter d’utiliser un CAS et pousser à la place un LLM à faire des maths, c’est comme faire un déménagement d’appartement en multipliant les allers-retours en bus au lieu d’utiliser un camion. C’est son point de vue, même si l’on a déjà un abonnement de bus
• Il souligne qu’un LLM reste au fond un modèle statistique du langage. D’après son expérience, la génération de programmes logiques, en particulier de code source Prolog, fonctionne mieux que prévu. C’est sans doute parce que Prolog a été introduit dans le traitement symbolique du langage naturel, et qu’il existe aussi de nombreux exemples de traduction dans les jeux de données d’entraînement. Il recommande aussi d’envisager l’usage de la syntaxe Datalog de Z3 plutôt que la syntaxe SMTLib. Voir la démo associée et la syntaxe Datalog de Z3
  • Dans Z3, la syntaxe Datalog est plutôt excellente. Nous avons utilisé SMT dans l’article sur les grammars, car c’était ce qui offrait la meilleure compatibilité avec plusieurs solveurs. Mais pendant le processus de review NeurIPS, nous avons testé et confirmé que cette approche fonctionne aussi très bien avec PROLOG. Nous nous attendons à ce qu’elle fonctionne aussi avec Datalog. lien vers l’article, exemple Datalog
• Cela semble être une approche intéressante. Notre équipe a également construit un prototype similaire pour encoder des politiques de fonctionnement métier en LEAN. Le LLM convertit d’abord la base de connaissances d’un wiki interne ou de Google Docs en code LEAN. Ensuite, un solveur est exécuté pour vérifier la cohérence. Quand le wiki est modifié, tout le processus est relancé, jouant une sorte de rôle de linter de processus. Cela dit, la conversion en LEAN elle-même nécessitait encore une revue par des ingénieurs, donc cela en est resté au stade du prototype. Mais cela semble prometteur pour les domaines soumis à des exigences de conformité juridique ou financière
  • Il mentionne que la barrière de l’autoformalisation est vraiment très élevée. Il partage l’expérience de leur article NeurIPS 2025, où ils ont quantifié et analysé l’incertitude de l’autoformalisation sur des grammaires bien définies. lien vers l’article N’hésitez pas à les contacter si vous voulez en discuter plus en détail
  • Pour ceux qui se demandent ce qu’est LEAN, il s’agit de Lean Theorem Prover, créé par Microsoft. lien du projet
  • Je serais curieux de voir un exemple concret. Quel type de politique, dans le monde réel, est décrit avec une précision suffisante pour être défini en LEAN ?
  • Le fait que cette méthode permette d’identifier systématiquement des directives contradictoires semble très utile
• C’est un domaine de recherche très intéressant. Il y a quelques années, j’ai utilisé un moteur de raisonnement logique et probabiliste pour vérifier si des prémisses menaient correctement à une conclusion. J’ai aussi utilisé des agents pour synthétiser, formaliser et critiquer des connaissances de domaine. Ce n’est pas une solution miracle, mais cela permettait de garantir un certain niveau de précision. Je pense qu’un certain degré de symbolique, ainsi que le concept d’agent-as-a-judge, sont prometteurs pour l’avenir. article de référence
  • J’ai lu cette recherche. C’est plutôt impressionnant. J’ai moi-même récemment travaillé sur un agent d’autoformalisation chez AWS ARChecks. Ce n’est pas encore public, mais il existe déjà un produit utilisable de manière générale qui peut servir de référence blog AWS
  • Utiliser un agent/un LLM comme juge introduit un biais, et à mon avis ce n’est adapté qu’au bootstrap. Une fois que les performances montent suffisamment, le juge LLM devient lui-même une limite artificielle ; il faut alors passer à des juges humains experts ou à un oracle déterministe
• Il est mentionné que le kernel rolling knife-edge de RHEL est utilisé pour le proof of concept
• Il a trouvé que le dépôt manquait d’explications détaillées, ce qui peut s’expliquer par son rôle d’artefact annexe à l’article. En substance, cela ressemble à une API qui pousse un LLM à générer des programmes Z3. On l’incite à exprimer logiquement des requêtes du monde réel, en capturant faits, règles d’inférence et objectifs. La fonction de supervision consiste à pouvoir lire directement la description logique et exécuter le solveur pour vérifier si c’est vrai ou faux. Ses doutes sont les suivants : qui va lire une à une les règles SMT pour les comparer à la réalité, qui validera les constantes, et comment s’assurer que le LLM n’ajoute pas par erreur, ou pour atteindre son but, des règles incohérentes sur le plan logique ou réel ? L’article rapporte 51% de faux positifs sur des benchmarks logiques, ce qui lui semble étonnamment élevé et suggère que les LLM restent faibles en modélisation logique ou génèrent des règles incomplètes. L’évaluation est trop maigre pour expliquer clairement pourquoi cela se produit
  • Il affirme que cet article a été rédigé l’an dernier avec GPT-4o, et que les choses se sont nettement améliorées avec les modèles récents. Par exemple, dans le récent article, tableau 1, ils comparent les performances textuelles et SMT. o3-mini fait bien correspondre le raisonnement textuel et les résultats sur SMT. Dans le produit commercial AWS Automated Reasoning Checks, on construit un modèle de domaine, on le vérifie, puis, à l’étape de génération de réponses, les paires Q/R produites par le LLM passent par une validation stricte au solveur pour s’assurer qu’elles respectent la politique. Ils soulignent qu’il est ainsi possible de garantir à plus de 99% la validité, du point de vue des politiques, des paires Q/R blog AWS
• Il demande si son interprétation est correcte. Si la sortie probabiliste produite par le LLM est transmise à un modèle logique, cela ne revient-il pas à dire « garbage in, garbage out » ?
  • La logique formelle sert de filtre. Donc ce n’est pas « garbage in, garbage out », mais plutôt « garbage in, garbage filtré en sortie ». Il compare cela à l’évolution, où des mutations aléatoires « inutiles » sont filtrées par l’environnement naturel
  • Il soutient qu’on n’obtient pas toujours des « déchets ». Assez souvent, la sortie est utile, et c’est ce qui lui donne de la valeur
  • C’est une appréciation subjective. Après tout, on pourrait aussi considérer comme des déchets tout ce que l’humanité a produit depuis des millénaires. À la rigueur, la vie dans une grotte était peut-être plus simple
• Le fait que l’IA ne se contente pas de penser, mais laisse aussi un journal vérifiable, est extrêmement intéressant. C’est comme voir un philosophe vivre avec un notaire cryptographique. Travail vraiment remarquable
• L’idée centrale est que le LLM esquisse d’abord le processus de raisonnement sous forme structurée, dans un JSON DSL, puis que cela est converti de manière déterministe en logique du premier ordre afin de tenter une preuve avec Z3. Le résultat final est donc une conclusion prouvable, ou un contre-exemple, ce qui le distingue d’une simple chaîne de texte persuasive
• Recherche intéressante. J’ai consulté le dépôt par curiosité à propos des exemples de DSL, mais il était difficile d’y trouver un exemple clair. Un extrait de code dans le README serait utile
  • Merci pour l’intérêt, nous allons en ajouter bientôt. En attendant, le PDF de l’article décrit plusieurs scénarios à partir de la page 11 PDF de l’article