ProofBench — Benchmark hybride IA : calcul symbolique + système de vérification de preuves sémantique

TL;DR

ProofBench est un benchmark hybride IA et système de vérification de preuves de nouvelle génération qui combine les mathématiques symboliques (SymPy/Pyodide) et l’analyse sémantique par IA (consensus multi-LLM).

Il évalue simultanément la structure logique des preuves et leur validité sémantique, afin de détecter les raisonnements « apparemment corrects » et de les quantifier avec le Logic Integrity Index (LII).

---

🎯 Pourquoi l’avoir créé

Les vérificateurs de preuves traditionnels

• sont soit basés sur la logique formelle et donc trop stricts et peu pratiques,
• soit s’arrêtent au niveau grammatical et ne détectent pas les erreurs sémantiques,
• soit ont un coût de calcul élevé, ce qui rend difficile un retour en temps réel.

ProofBench est un framework de benchmark hybride IA qui combine la rigueur de la vérification symbolique et la capacité de compréhension flexible de l’IA avec une approche hybride « 70 % symbolique + 30 % sémantique ».

---

📊 Voici les questions que ProofBench permet de vérifier

• « L’IA peut-elle comprendre la cohérence logique ? »
• « La visualisation de la structure des preuves sous forme de graphe permet-elle de faire apparaître des motifs d’erreur ? »
• « À quel point l’évaluation sémantique est-elle fiable ? »
• « Un benchmark combinant symbolique et sémantique est-il utile pour l’éducation, la recherche et l’évaluation de l’IA ? »

---

🧩 Indicateurs du benchmark hybride IA

• LII (Logic Integrity Index) : mesure centrale de l’intégrité logique
• Coherence Variance : niveau d’accord entre plusieurs modèles
• Symbolic Pass Rate : taux de cohérence mathématique
• Semantic Stability : taux de maintien de la cohérence contextuelle

Ces mesures pourront ensuite évoluer vers une référence commune pour évaluer chez les modèles d’IA leur “raisonnement logique, leur cohérence et leur capacité d’interprétation sémantique”.

---

🔍 Aperçu de l’architecture

• Symbolic Layer — exécute SymPy via Pyodide pour une vérification déterministe dans le navigateur
• Semantic Layer — évalue les réponses de plusieurs LLM sur la base d’un consensus
• Hybrid Orchestrator — pondération par défaut 70/30 (ajustable), calcul du score final
• LII Engine — calcul de l’indice d’intégrité logique + intervalle de confiance
• Justification Analyzer — graphe de dépendances + détection de cycles
• Feedback Generator — génération de rapports d’évaluation étape par étape en langage naturel

---

⚙️ Fonctionnalités clés (v3.7.2)

• Moteur de vérification hybride : exécution de SymPy avec Pyodide dans le navigateur + analyse sémantique fondée sur le consensus multi-LLM
• LII (Logic Integrity Index) : quantification de la cohérence logique avec un score de 0 à 100 et un intervalle de confiance à 95 %
• Justification Graph : visualisation des dépendances entre preuves et détection automatique des raisonnements circulaires
• Consensus Manager : calcule l’accord entre plusieurs modèles et produit un score moyen fondé sur la cohérence
• Natural Feedback Generator : retour en langage naturel sur les erreurs et leurs causes à chaque étape
• UI / Dashboard : visualisation des résultats par étape de preuve, vue graphe, rapports et score LII
• Exécution Docker en un clic : utilisable immédiatement avec une seule ligne docker run

docker run -p 3000:80 ghcr.io/flamehaven/proofbench:latest  
# → http://localhost:3000  
  

---

🧱 Limites

• La couche sémantique reste sensible aux pièges linguistiques complexes (la couche symbolique amortit cet effet)
• Le LII n’est pas un certificat de preuve formel, mais un indicateur de qualité
• Pyodide a un coût de démarrage initial sur les appareils peu puissants

---

⚡ Points sur lesquels j’aimerais avoir des retours

• La pondération par défaut 70/30 est-elle raisonnable ? (faut-il un poids adaptatif ?)
• LII + intervalle de confiance constituent-ils un benchmark pertinent pour l’éducation et la recherche ?
• La détection des raisonnements circulaires est-elle utile dans de vrais exercices de mathématiques/logique ?
• Des idées pour améliorer les goulots d’étranglement de performance dans le navigateur (Pyodide) ?
• Les exemples de preuves « qui ont l’air justes mais sont fausses » sont les bienvenus 🧩

---

🗺️ Feuille de route

• Pondération adaptative par section
• Prise en charge de divers formats de preuve (Lean, Coq, formules Markdown, etc.)
• Renforcement des modèles d’export de rapports fondés sur LII + graphe
• Mise en place d’un benchmark de red team (publication d’un ensemble de preuves « plausibles mais fausses »)

---

🔗 Liens

• GitHub: https://github.com/Flamehaven/proofbench
• Licence: MIT

---

✍️ Commentaire de développement

ProofBench est un outil conçu pour tester si l’IA peut comprendre non pas la « bonne réponse », mais la « justification », en unifiant dans un seul benchmark la structure logique, la cohérence sémantique et l’explicabilité.

Ce n’est pas un simple vérificateur — c’est appelé à devenir un nouveau banc d’essai pour mesurer la capacité de raisonnement de l’IA.