💻 computer science

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

Dit artikel bewijst dat de Matthews Correlation Coefficient (MCC) convergeert naar het geometrisch gemiddelde van precisie en recall (de Fowlkes-Mallows-score) naarmate het aantal ware negatieven oneindig groot wordt, en onderbouwt dit resultaat met een volledige wiskundige bewijsvoering en een Lean-formalisatie.

Oorspronkelijke auteurs: Jon Crall

Gepubliceerd 2026-03-19

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Jon Crall

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een detective bent die probeert te achterhalen of een verdachte schuldig is. Je hebt een lijst met verdachten en je moet ze in twee categorieën plaatsen: "Schuldig" (positief) of "Onschuldig" (negatief).

In de wereld van kunstmatige intelligentie (AI) doen computers precies hetzelfde. Ze proberen te voorspellen of iets een bepaald object is (bijvoorbeeld een hond) of niet. Om te zien hoe goed ze zijn, gebruiken wetenschappers een soort scorebord, een verwarringsmatrix.

Op dit scorebord staan vier soorten resultaten:

Ware Positieven (TP): De hond werd herkend als een hond. (Goed gedaan!)
Valse Positieven (FP): De hond werd herkend als een hond, maar het was eigenlijk een kat. (Foutje.)
Valse Negatieven (FN): De hond werd gemist en niet herkend. (Ook een foutje.)
Ware Negatieven (TN): De computer keek naar een steen, een boom of een wolk en zei: "Nee, dat is geen hond."

Het Probleem: De Oneindige Zee van "Niet-Honden"

In een simpele test met 10 foto's is het makkelijk om te tellen hoeveel "ware negatieven" er zijn. Maar in de echte wereld, zoals bij objectdetectie (bijvoorbeeld in een zelfrijdende auto), is het heel anders.

Stel je voor dat je een camera hebt die 1000 keer per seconde een foto maakt. Op elke foto zijn er miljoenen mogelijke plekken waar een hond zou kunnen zitten. De computer moet controleren of die plekken een hond zijn.

Als de computer zegt "geen hond" op een plek waar ook echt geen hond zit, is dat een Ware Negatief.
Het probleem? Er zijn oneindig veel plekken waar geen hond zit. De lucht, de weg, de bomen... het zijn allemaal "ware negatieven".

Het is onmogelijk om dit getal te tellen. Het is als proberen te tellen hoeveel zandkorrels er niet in een emmer zitten, terwijl de zee oneindig groot is.

De Twee Meetlatjes

Wetenschappers hebben twee manieren om de prestaties te meten:

De F1-score (De "Korte" Meetlat): Deze kijkt alleen naar de honden die wel of niet gevonden werden. Hij negeert de oneindige zee van "niet-honden". Hij is makkelijk te berekenen, maar voelt voor sommige wiskundigen niet helemaal eerlijk omdat hij een groot stuk van de realiteit negeert.
De MCC-score (De "Volledige" Meetlat): Deze kijkt naar alles: de gevonden honden, de gemiste honden, de verkeerde meldingen én de "niet-honden". Dit wordt gezien als de meest eerlijke score, maar hij heeft een groot nadeel: hij heeft het getal van de "ware negatieven" nodig. En dat getal is in de echte wereld vaak onmogelijk te bepalen.

De Grote Ontdekking: Wat gebeurt er als het getal oneindig wordt?

De auteur van dit artikel, Jon Crall, vroeg zich af: "Wat gebeurt er met die eerlijke MCC-score als we aannemen dat het aantal 'ware negatieven' (de niet-honden) oneindig groot wordt?"

Hij deed een wiskundig experiment. Hij liet het getal van de "niet-honden" steeds groter worden, tot het oneindig was. En wat bleek?

De MCC-score veranderde precies in de F1-score.

Een Simpele Analogie: De Naald in de Hooiberg

Stel je voor dat je een naald (de hond) zoekt in een hooiberg.

Als de hooiberg klein is (weinig "niet-honden"), maakt het uit of je kijkt naar de hele berg of alleen naar de plek waar de naald zou kunnen zitten. De MCC-score (die naar de hele berg kijkt) en de F1-score (die alleen naar de naald kijkt) zijn dan verschillend.
Maar als de hooiberg oneindig groot wordt (zoals in de echte wereld), wordt het aantal "niet-honden" zo gigantisch dat het de berekening domineert.
Op dat punt "verdwijnt" het effect van het tellen van de hooiberg. De wiskundige formule van de MCC-score "slikt" het oneindige getal op en reduceert zichzelf tot precies hetzelfde als de F1-score.

De conclusie is dus: In situaties waar het aantal "negatieve" voorbeelden (zoals niet-honden) zo groot is dat het oneindig lijkt, is het veilig om de MCC-score te gebruiken. Je kunt je zorgen maken over het tellen van de "niet-honden" niet meer, want wiskundig gezien levert dat precies hetzelfde resultaat op als de simpele F1-score.

Waarom is dit belangrijk?

Het lost een dilemma op: Het geeft wetenschappers en engineers geruststelling. Ze kunnen de "eerlijke" MCC-score gebruiken in complexe systemen (zoals zelfrijdende auto's) zonder zich zorgen te hoeven maken over het tellen van de oneindige "niet-honden". Ze weten nu dat het resultaat hetzelfde is als de bekende F1-score.
Het verbindt werelden: De auteur merkte op dat ecologen (die dieren tellen) dit al lang wisten, maar met andere namen. Ze zagen dat als je twee soorten dieren vergelijkt in een enorm gebied, de correlatie (MCC) overgaat in een andere maatstaf (FM-index). Dit artikel brengt die kennis terug naar de wereld van AI.
De rol van AI in het bewijzen: Interessant genoeg heeft de auteur zelf AI gebruikt om dit wiskundige bewijs te controleren. Hij gebruikte een speciaal computerprogramma (Lean) om te garanderen dat elke stap in de wiskunde 100% correct is, zonder menselijke fouten.

Kortom: Als je een AI bouwt die moet zoeken in een wereld vol met "niet-dingen", hoef je je geen zorgen te maken over het tellen van die "niet-dingen". De wiskunde zegt dat je resultaat op dat punt gewoon klopt, ongeacht hoe groot de wereld is.

Titel en Context

Het artikel onderzoekt de wiskundige relatie tussen de Matthews Correlation Coefficient (MCC) en de Fowlkes-Mallows (FM) score (het geometrisch gemiddelde van precisie en recall) in de context van binaire classificatie, met name wanneer het aantal ware negatieven (True Negatives, TN) naar oneindig gaat.

1. Het Probleem

De prestaties van een binaire classifier worden doorgaans samengevat door een confusiematrix met vier waarden: True Positives (TP), True Negatives (TN), False Positives (FP) en False Negatives (FN).

MCC: Deze metriek is uniek omdat hij alle vier de waarden van de confusiematrix gebruikt en wordt beschouwd als een robuuste maatstaf voor correlatie tussen voorspelling en werkelijkheid.
F1 en FM: Deze scores negeren het aantal ware negatieven (TN) en baseren zich alleen op TP, FP en FN.
Het Dilemma: In "open-world" scenario's, zoals objectdetectie, is het tellen van ware negatieven vaak onmogelijk of onpraktisch. Het aantal mogelijke negatieve kandidaat-boundingboxes is effectief onbegrensd (bijna elke pixelcombinatie die geen object bevat, is een potentiële TN).
De Vraag: Wat gebeurt er met de MCC-waarde als het aantal ware negatieven (TN) naar oneindig gaat? Is er een limiet die de MCC koppelt aan de bestaande, TN-vrije metrieken zoals FM?

2. Methodologie

De auteurs hanteren een drietalige aanpak om het probleem aan te pakken:

Analytische Afleiding: Een handmatige algebraïsche berekening van de limiet van de MCC-formule wanneer $TN \to \infty$ .
Symbolische Verificatie: Het gebruik van de Python-bibliotheek SymPy om de algebraïsche stappen en de limietberekening te verifiëren.
Formele Verificatie: Het opstellen van een formeel bewijs in Lean 4, een interactief bewijshulpmiddel met een klein, betrouwbaar kernel. Dit garandeert dat elke algebraïsche manipulatie en limietstap wiskundig correct is onder expliciete aannames.

Daarnaast wordt er gebruikgemaakt van LLMs (Large Language Models) om:

Het formele bewijs in Lean te genereren en te verfijnen (van 654 regels naar 66 regels).
Bestaande literatuur te doorzoeken om te bevestigen dat dit resultaat eerder was opgemerkt in de ecologie, maar onder andere namen.

3. Belangrijkste Bijdragen en Resultaten

De Wiskundige Limiet

De kern van het artikel is het bewijs dat:
$\lim_{TN \to \infty} \text{MCC} = \text{FM}$
Waarbij FM de Fowlkes-Mallows index is, gedefinieerd als het geometrisch gemiddelde van precisie (PPV) en recall (TPR):
$\text{FM} = \sqrt{\text{PPV} \cdot \text{TPR}} = \sqrt{\frac{TP}{TP+FP} \cdot \frac{TP}{TP+FN}}$

De afleiding (samengevat):
Door de teller en noemer van de MCC-formule te vermenigvuldigen met $1/TN$ en de limiet te nemen, verdwijnen de termen die $TN$ bevatten in de noemer (ze gaan naar 0). De teller vereenvoudigt tot $TP$. De uitdrukking reduceert tot:
$\frac{TP}{\sqrt{(TP+FP)(TP+FN)}}$
Dit is algebraïsch identiek aan de formule voor de FM-score.

Formele Verificatie in Lean 4

De auteurs hebben het bewijs volledig geformaliseerd in Lean 4.

Het bewijs definieert de variabelen en de voorwaarden (alle waarden niet-negatief, $TP+FP > 0$, $TP+FN > 0$).
Het bewijst dat de functie van de MCC convergeert naar de FM-waarde wanneer $TN$ naar oneindig gaat (gebruikmakend van filters en topologie in Lean).
Dit biedt een machine-verifieerbare garantie dat het resultaat foutloos is, wat een belangrijk onderscheid is ten opzichte van traditionele handmatige bewijzen.

Literatuur en Context

Het artikel identificeert dat dit resultaat eerder was opgemerkt in de ecologie (onderzoek naar associatie tussen soorten), waar de phi-coëfficiënt (identiek aan MCC) en de Ochiai-index (identiek aan FM) worden gebruikt. In de ecologie is het bekend dat de phi-coëfficiënt convergeert naar de Ochiai-index wanneer het aantal "double zeros" (TN) toeneemt. Dit artikel brengt deze kennis over naar het domein van machine learning en objectdetectie.

4. Betekenis en Impact

Theoretisch Inzicht: Het artikel lost een theoretische vraag op over het gedrag van de MCC in situaties waar TN niet meetbaar is. Het bevestigt dat in "open-world" problemen (zoals objectdetectie), het negeren van TN niet willekeurig is, maar wiskundig equivalent is aan het nemen van de limiet van de MCC.
Praktische Implicatie voor Objectdetectie: Voor objectdetectie-systemen, waar het tellen van ware negatieven ondoenlijk is, biedt dit resultaat een rechtvaardiging voor het gebruik van de FM-score (of het geometrisch gemiddelde van precisie en recall) als een proxy voor de MCC. Het laat zien dat FM de "natuurlijke" limiet is van de MCC in deze context.
Rol van AI in Wetenschap: Het artikel dient als een casestudy voor het gebruik van LLMs in de wetenschap. Ze hielpen niet alleen bij het vinden van gerelateerde, maar anders getermineerde literatuur (ecologie vs. ML), maar waren ook cruciaal bij het genereren en optimaliseren van het formele bewijs in Lean 4, een taal die voor de auteur nieuw was.

Conclusie

Het artikel bewijst wiskundig en formeel dat de Matthews Correlation Coefficient convergeert naar de Fowlkes-Mallows index (het geometrisch gemiddelde van precisie en recall) naarmate het aantal ware negatieven naar oneindig gaat. Dit biedt een wiskundige basis voor het gebruik van TN-vrije metrieken in open-world classificatieproblemen en demonstreert de groeiende synergie tussen menselijke onderzoekers en AI-tools voor zowel literatuuronderzoek als formeel wiskundig bewijs.