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

Título: O MCC Aproxima-se da Média Geométrica de Precisão e Recall à Medida que os Verdadeiros Negativos Tendem ao Infinito

1. Problema e Motivação

A avaliação de classificadores binários é tradicionalmente realizada através de uma matriz de confusão, que contém quatro entradas: Verdadeiros Positivos (TP), Verdadeiros Negativos (TN), Falsos Positivos (FP) e Falsos Negativos (FN).

• Métricas Comuns: O F1-score e o índice Fowlkes-Mallows (FM) são métricas populares que resumem o desempenho, mas baseiam-se apenas em três das quatro entradas (ignoram os TN). Elas são definidas como a média harmônica e a média geométrica de Precisão (PPV) e Recall (TPR), respectivamente.
• O Coeficiente de Correlação de Matthews (MCC): Diferente do F1 e do FM, o MCC considera todas as quatro entradas da matriz de confusão, sendo frequentemente considerado uma métrica mais robusta e balanceada.
• O Desafio em "Open World": Em problemas como a detecção de objetos, o número de "verdadeiros negativos" (caixas de delimitação que não correspondem a nenhum objeto) é efetivamente ilimitado ou incontrolável. Calcular o TN exato é impraticável, o que torna o cálculo do MCC difícil ou impossível nesses cenários.
• Questão Central: Qual é o comportamento limite do MCC quando o número de Verdadeiros Negativos ($TN$) tende ao infinito? É possível relacionar o MCC a métricas que não dependem de TN (como o FM) neste limite?

2. Metodologia

O artigo emprega uma abordagem tripla para investigar e validar a relação matemática entre o MCC e o FM no limite de $TN \to \infty$:

1. Derivação Algébrica Analítica:

   • Os autores partem da definição formal do MCC e aplicam limites algébricos.
   • Multiplicam o numerador e o denominador por $1/TN$.
   • Demonstram que, à medida que $TN \to \infty$, os termos contendo $TN$ no denominador (como $FP/TN$e$FN/TN$) tendem a zero.
   • Simplificam a expressão resultante para mostrar que ela se torna idêntica à fórmula do índice Fowlkes-Mallows (FM).

2. Verificação Computacional (SymPy):

   • Utilizam a biblioteca simbólica Python SymPy para definir as expressões do MCC e do FM.
   • Calculam o limite simbólico do MCC quando $TN \to \infty$.
   • Verificam que a diferença entre o limite calculado e a fórmula do FM é zero, confirmando a igualdade numericamente/simbolicamente.

3. Formalização Matemática Rigorosa (Lean 4):

   • Para garantir a correção absoluta e evitar erros humanos ou de software, os autores formalizaram a prova no assistente de prova Lean 4.
   • A prova em Lean define as métricas (PPV, TPR, FM, MCC) e utiliza filtros de topologia (Filter.Tendsto) para expressar o conceito de limite.
   • O código Lean prova que, sob condições de não-negatividade e positividade das somas parciais ($TP+FP > 0$, $TP+FN > 0$), a função MCC converge para o FM quando $TN$ tende ao infinito.

3. Contribuições Principais

• Prova Formal do Limite: Estabelecimento rigoroso de que $\lim_{TN \to \infty} \text{MCC} = \text{FM}$. Isso significa que, em cenários onde os TN são massivos (como em detecção de objetos), o MCC se comporta exatamente como a média geométrica de Precisão e Recall.
• Contextualização em Visão Computacional: A aplicação deste resultado matemático ao problema prático da detecção de objetos, justificando teoricamente o uso de métricas que ignoram TN (como FM ou F1) em "mundos abertos", desde que se reconheça que o MCC converge para essas métricas.
• Formalização em Lean 4: Fornecimento de uma prova verificada por máquina, aumentando a confiança no resultado e servindo como exemplo de formalização matemática em ciência da computação.
• Conexão Interdisciplinar: Identificação de que este resultado já era conhecido na literatura de ecologia (sob os nomes de coeficiente phi e índice de Ochiai), mas não era amplamente reconhecido ou provado no contexto de classificadores binários de aprendizado de máquina.

4. Resultados

• Convergência Matemática: A prova demonstra que:
  $$\lim_{TN \to \infty} \frac{TP \cdot TN - FP \cdot FN}{\sqrt{(TP+FP)(TP+FN)(TN+FP)(TN+FN)}} = \sqrt{\frac{TP}{TP+FP} \cdot \frac{TP}{TP+FN}} = \text{FM}$$
• Validação: O código Lean compila com sucesso, fornecendo uma garantia de que cada passo algébrico e de limite é válido sob as premissas assumidas.
• Descoberta de Literatura: O uso de LLMs (Modelos de Linguagem) ajudou a localizar referências anteriores na ecologia que já haviam notado essa relação, mas não a haviam formalizado no contexto de ML.

5. Significado e Impacto

• Para a Avaliação de Modelos: Este trabalho oferece uma justificativa teórica sólida para o uso do índice Fowlkes-Mallows (ou F1, embora o FM seja o limite exato do MCC) em tarefas de detecção de objetos e outros problemas de "open world", onde contar TN é impossível. Ele conecta a métrica mais completa (MCC) às métricas práticas (FM/F1) através de um limite matemático.
• Papel da IA na Pesquisa: O artigo destaca o papel emergente dos Grandes Modelos de Linguagem (LLMs) na pesquisa científica, especificamente em:
  1. Assistência à Prova: Ajudando autores a formalizar provas complexas em sistemas como Lean 4.
  2. Busca de Literatura: Identificando conexões entre terminologias de campos distintos (Ecologia vs. Visão Computacional).
• Rigor Científico: Demonstra a importância de formalizar intuições matemáticas simples, mas não triviais, para garantir sua validade em aplicações críticas.

Em resumo, o artigo fecha uma lacuna teórica importante, provando que em cenários de dados desbalanceados com infinitos negativos, o MCC perde sua dependência dos TN e se torna equivalente à média geométrica de Precisão e Recall, validando o uso de métricas focadas apenas nos positivos em problemas de detecção de objetos.