The MCC approaches the geometric mean of precision and recall as true negatives approach infinity

Cet article démontre et formalise que, dans les contextes où le nombre de vrais négatifs tend vers l'infini, le coefficient de corrélation de Matthews converge vers le score de Fowlkes-Mallows, soit la moyenne géométrique de la précision et du rappel.

L'essentiel

🎯 Le Problème : Comment juger un détective quand le monde est infini ?

Imaginez que vous évaluez un détective (un algorithme d'intelligence artificielle) qui cherche à repérer des chats dans des photos.
Pour savoir s'il est bon, on regarde quatre choses :

1. Vrais Positifs (TP) : Il a vu un chat, et c'était un chat. (Bravo !)
2. Faux Positifs (FP) : Il a cru voir un chat, mais c'était un chien. (Erreur !)
3. Faux Négatifs (FN) : Il y avait un chat, mais il ne l'a pas vu. (Oups !)
4. Vrais Négatifs (TN) : Il a regardé un coin de l'image, n'a rien vu, et c'était bien vide. (Correct !)

Dans un monde normal (comme une photo de chat), on peut compter tous ces éléments. Mais dans le monde de la détection d'objets (comme chercher des voitures sur une autoroute), le problème est différent.

L'analogie du "Mur Infini" :
Imaginez que votre détective regarde une route infinie.

• Il voit 10 voitures (TP).
• Il se trompe 2 fois (FP).
• Il en rate 1 (FN).
• Mais combien de fois a-t-il regardé un endroit vide et dit "rien ici" ? Des milliards ! Chaque mètre carré de bitume, chaque nuage, chaque arbre qui n'est pas une voiture est un "Vrai Négatif".

Le nombre de "Vrais Négatifs" est si gigantesque qu'il est pratiquement infini. C'est comme essayer de compter le sable sur toutes les plages du monde pour évaluer si un détective est bon. C'est impossible et cela fausse les calculs classiques.

📉 La Question : Que devient la note du détective ?

Les experts utilisent une note très stricte appelée MCC (Coefficient de Corrélation de Matthews) qui prend en compte les 4 éléments (y compris le sable infini). Mais comme on ne peut pas compter le sable, on utilise souvent une note plus simple (F1 ou FM) qui ignore le sable et ne regarde que les voitures (positifs) et les erreurs.

La question du papier est simple : Si le nombre de "sable" (Vrais Négatifs) devient infini, la note stricte (MCC) finit-elle par devenir identique à la note simple (FM) ?

💡 La Réponse : Oui, elles se ressemblent !

L'auteur, Jon Crall, a prouvé mathématiquement que oui.
Quand le nombre de "choses qui ne sont pas l'objet" devient infini, la note complexe (MCC) se simplifie et tombe exactement sur la note simple (FM).

L'analogie du "Bruit de fond" :
Imaginez que vous écoutez une conversation dans une pièce.

• Si la pièce est petite, le bruit de fond (les Vrais Négatifs) compte beaucoup dans votre jugement de la conversation.
• Mais si la pièce devient l'océan entier, le bruit de fond est si énorme qu'il devient le "fond" de tout. Dans ce cas, pour juger la conversation, vous n'avez plus besoin de compter chaque vague. Vous vous concentrez uniquement sur ce qui est dit (les Positifs) et ce qui est mal compris (les Erreurs).
• Le calcul complexe s'effondre pour devenir le calcul simple.

🛠️ Comment l'a-t-il prouvé ? (Le côté "Magie des Machines")

Ce n'est pas juste une intuition. L'auteur a fait deux choses :

1. Mathématiques classiques : Il a fait des calculs algébriques (comme simplifier une fraction) pour montrer que lorsque le nombre de négatifs tend vers l'infini, les termes compliqués disparaissent et il ne reste que la formule simple.
2. Preuve par Ordinateur (Lean) : Pour être absolument sûr qu'il n'y a pas d'erreur humaine, il a demandé à un assistant mathématique (un logiciel appelé Lean) de vérifier chaque étape de son raisonnement. C'est comme demander à un robot de vérifier votre devoir de maths ligne par ligne pour garantir qu'il n'y a aucune faille logique.

🤖 Le rôle de l'Intelligence Artificielle (LLM)

Ce papier est aussi intéressant car il parle de l'aide qu'il a reçue d'autres intelligences artificielles (les LLMs comme GPT) pour écrire ce papier :

• Pour les maths : L'auteur ne connaissait pas bien le langage "Lean". Il a utilisé une IA pour l'aider à traduire son raisonnement humain en langage informatique rigoureux.
• Pour la recherche : Il a utilisé une IA pour fouiller dans des articles scientifiques vieux de plusieurs décennies, écrits par des écologistes (qui étudient les espèces animales). Il a découvert que ce résultat était déjà connu dans le monde de l'écologie, mais sous un autre nom ! L'IA a fait le pont entre deux mondes qui ne se parlaient pas.

🏁 En résumé

Ce papier dit :

"Quand on essaie d'évaluer une IA dans un monde où les 'faux négatifs' sont infinis (comme chercher des objets dans un océan de pixels), on peut arrêter d'utiliser la formule compliquée. Elle devient naturellement égale à la formule simple que tout le monde utilise déjà. C'est une bonne nouvelle : cela valide l'utilisation des méthodes simples dans des cas complexes."

C'est une preuve mathématique rassurante qui dit : "Ne vous inquiétez pas de compter l'infini, concentrez-vous sur ce qui compte vraiment."

Résumé technique

1. Problématique

L'évaluation des classificateurs binaires repose souvent sur une matrice de confusion contenant quatre entrées : les vrais positifs (TP), les vrais négatifs (TN), les faux positifs (FP) et les faux négatifs (FN).

• Le défi : Dans certains contextes, notamment la détection d'objets (open-world settings), le nombre de vrais négatifs est difficilement mesurable, voire infini. En effet, l'espace des candidats (boîtes englobantes potentielles) est si vaste que la majorité des prédictions correctes sont des "vrais négatifs" implicites.
• La limitation des métriques actuelles :
  • Le Score F1 et l'indice Fowlkes-Mallows (FM) ne prennent en compte que TP, FP et FN (ils ignorent TN).
  • Le Coefficient de Corrélation de Matthews (MCC) est souvent considéré comme une métrique plus robuste car il intègre les quatre termes de la matrice de confusion. Cependant, son calcul devient problématique ou inapplicable lorsque TN est inconnu ou tend vers l'infini.
• Question centrale : Quelle est la limite du MCC lorsque le nombre de vrais négatifs ($TN$) tend vers l'infini ?

2. Méthodologie

Les auteurs adoptent une approche combinant analyse mathématique classique, vérification symbolique et preuve formelle assistée par ordinateur :

1. Analyse Mathématique : Ils étudient le comportement asymptotique de la formule du MCC lorsque $TN \to \infty$. En manipulant algébriquement l'expression du MCC (en divisant numérateur et dénominateur par $TN$), ils montrent que les termes contenant $TN$ s'annulent à la limite.
2. Vérification Symbolique (SymPy) : Ils utilisent la bibliothèque Python SymPy pour calculer symboliquement la limite et vérifier que l'expression résultante est identique à celle de l'indice FM.
3. Preuve Formelle (Lean 4) : Pour garantir une rigueur absolue et éviter les erreurs humaines ou les bugs logiciels potentiels des outils symboliques, les auteurs formalisent la preuve dans Lean 4, un assistant de preuve interactif avec un noyau vérifiable. Cette preuve machine vérifie chaque étape algébrique et les règles de limites sous des hypothèses explicites (non-négativité des termes, dénominateurs non nuls).
4. Recherche de littérature assistée par LLM : Les auteurs utilisent des modèles de langage (LLM) pour identifier des travaux antérieurs dans d'autres domaines (écologie) qui avaient déjà noté ce lien, mais sous des noms différents (coefficient phi et indice d'Ochiai).

3. Contributions Clés

• Preuve du résultat asymptotique : Démonstration formelle que lorsque $TN \to \infty$, le MCC converge exactement vers l'indice Fowlkes-Mallows (FM).
  $$\lim_{TN \to \infty} \text{MCC} = \text{FM} = \sqrt{\text{Précision} \times \text{Rappel}}$$
• Formalisation en Lean 4 : Fourniture d'une preuve complète et vérifiable par machine (code de 66 lignes après optimisation), rendant le résultat incontestable d'un point de vue logique.
• Contextualisation interdisciplinaire : Mise en lumière du fait que ce résultat était déjà connu en écologie (sous le nom de convergence du coefficient $\phi$ vers l'indice d'Ochiai) mais restait obscur pour la communauté du Machine Learning, en particulier pour la détection d'objets.
• Étude de cas sur l'usage des LLMs : Documentation de l'utilisation des LLMs non seulement pour la recherche bibliographique (combler le fossé terminologique entre écologie et ML), mais aussi pour l'assistance à la formalisation de preuves mathématiques complexes.

4. Résultats

• Convergence : Le MCC, qui dépend de tous les termes de la matrice, se simplifie mathématiquement pour devenir le FM (moyenne géométrique de la précision et du rappel) lorsque le nombre de vrais négatifs devient négligeable par rapport à la taille de l'espace de recherche (tend vers l'infini).
• Validation : La preuve Lean 4 compile avec succès, confirmant que la déduction algébrique est correcte sous les hypothèses standards (TP+FP > 0, TP+FN > 0).
• Implication pour la détection d'objets : Dans les problèmes de détection d'objets où le comptage des TN est intractable, l'utilisation du FM est justifiée théoriquement comme étant la limite naturelle du MCC. Cela valide l'usage de métriques ignorant les TN dans ces contextes spécifiques.

5. Signification et Impact

• Justification théorique : Ce travail fournit une fondation mathématique solide pour l'utilisation de métriques comme le FM ou le F1 dans les scénarios "open-world" où les vrais négatifs sont illimités. Il répond à la critique selon laquelle ignorer les TN est "insatisfaisant" en montrant que le MCC lui-même converge vers ces métriques dans la limite.
• Rigueur scientifique : L'intégration d'une preuve formelle (Lean) dans un article de recherche appliquée marque une avancée vers une plus grande fiabilité des résultats théoriques en intelligence artificielle.
• Rôle des LLMs : L'article sert d'étude de cas sur l'évolution du rôle des LLMs dans la recherche scientifique : ils ne se contentent pas de générer du texte, mais agissent comme des ponts entre des domaines spécialisés (écologie vs vision par ordinateur) et comme des assistants de preuve formelle, bien que l'intervention humaine reste cruciale pour la validation et la structuration.

En résumé, ce papier établit un lien mathématique rigoureux entre une métrique "complète" (MCC) et une métrique "partielle" (FM) dans des conditions limites spécifiques, validé par des outils de preuve formelle et contextualisé par l'histoire des sciences.