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

この論文は、真陰性数が無限大に近づくにつれて、4 つの分類結果すべてに依存するマシューズ相関係数（MCC）が、真陰性を無視した精度と再現率の幾何平均であるフォークス・マローウスコアに収束することを証明し、その証明を Lean 形式化で示したものである。

要約

この論文は、機械学習（AI）が「正解」を見つけたかどうかを評価する際の数式について、少し不思議で面白い「極限」の話をしています。

専門用語を避け、**「AI のテスト」と「宇宙の広さ」**というイメージを使って、わかりやすく解説しますね。

1. 背景：AI のテストと「正解」の難しさ

まず、AI が画像から「猫」を見つけるテストをすると想像してください。
AI は画像の中に「猫がいる（正解）」か「猫はいない（不正解）」かを答えます。

評価には通常、4 つの数字を使います。

1. 正解（TP）: 猫だと予測して、本当に猫だった。
2. 誤検知（FP）: 猫じゃないのに「猫だ！」と騒いできた。
3. 見逃し（FN）: 猫がいるのに「猫じゃない」と見落とした。
4. 正解の否定（TN）: 「猫じゃない」と予測して、本当に猫じゃなかった。

ここで問題なのが**「4. 正解の否定（TN）」です。
「猫じゃない」ものは、空、木、車、石、そして画像の隅々まで……無限に近いほどたくさんあります。
「猫じゃない」と正しく判断した回数を数えようとしても、それは「宇宙の砂粒の数」を数えるようなもので、実質的に無限大**になってしまいます。

2. 2 つの評価基準の対決

AI の性能を測るには、いくつかの「スコア」があります。

• F1 スコア（F1 Score）：
  「正解（TP）」と「誤検知（FP）」と「見逃し（FN）」の 3 つだけを見て評価します。「猫じゃない（TN）」の数は無視します。

  • イメージ: 「猫を見つけること」に特化した評価。

• MCC（マシューズ相関係数）：
  上記の 3 つに加え、「猫じゃない（TN）」の数もすべて含めて評価します。

  • イメージ: 「猫を見つけること」と「猫じゃないと見分けること」の両方を完璧に測る、非常に厳格な評価。

通常、MCC の方が「より正確で完璧な指標」と言われています。しかし、「猫じゃない（TN）」の数が無限大になってしまう場合（例えば、画像の背景全体を評価する場合）、MCC を計算するのは不可能になります。

3. この論文の発見：「無限」の魔法

著者たちは、ある不思議な問いを立てました。
「もし『猫じゃない（TN）』の数が、限りなく無限大に近づいたら、MCC というスコアはどうなる？」

答えはシンプルで、かつ驚くべきものです。

MCC は、無限大になると、F1 スコア（の兄弟分）に「変身」します。

具体的には、MCC は**「Fowlkes-Mallows 指数（FM スコア）」**という値に収束します。
FM スコアは、F1 スコアと似ていますが、少し計算方法が違います（幾何平均を使います）。

【わかりやすい比喩】
MCC という「巨大な船」が、海（TN の数）が広がりすぎて無限の海に漕ぎ出したと想像してください。
最初は船の重さ（TN の数）が重要でしたが、海が広がりすぎると、船の重さの影響は相対的にゼロになります。
すると、船の動きは、「帆（正解 TP）」と「舵（誤検知 FP・見逃し FN）」だけで決まる、よりシンプルな船（FM スコア）と同じ動きをするようになります。

つまり、**「無限に広い世界では、MCC という複雑な指標は、F1 や FM というシンプルな指標と全く同じ結果を出す」**ということです。

4. なぜこれが重要なのか？

• 現実的な意味:
  物体検出（画像から物体を見つける AI）のような分野では、「猫じゃない」領域は無限大です。これまでは「TN がわからないから MCC は使えない」と言われていましたが、この論文は**「無限大なら、MCC は FM スコアとみなしていいよ」**と証明しました。これで、複雑な計算をしなくても、信頼できる評価が可能になります。

• 数学的な証明:
  著者たちは、このことが「生態学（動物の生息地調査など）」の分野では昔から知られていたことに気づきました。しかし、機械学習の分野では知られていませんでした。
  さらに、著者たちはこの証明を**「Lean（リーン）」という、コンピュータがチェックできる厳密なプログラミング言語で書き直し、「数学的に間違いないこと」**を機械に保証させました。

5. AI（LLM）の役割

面白いことに、この論文を書く際、著者自身は「Lean」という言語に詳しくありませんでした。そこで、**AI（大規模言語モデル）**に頼りました。

• 証明の作成: AI が Lean のコードを書き、著者がそれを修正して完成させました。
• 文献の発見: AI に「この現象は他の分野で知られていないか？」と聞くと、生態学の古い論文を瞬時に見つけてくれました。

まとめ

この論文は、**「無限大という極端な状況では、複雑な評価基準（MCC）は、シンプルで実用的な基準（FM スコア）と全く同じ振る舞いをする」**という数学的な事実を、AI の力も借りて証明したものです。

「広すぎる海では、どんなに大きな船も、帆と舵だけで進む小さなボートと同じ速さになる」
そんなイメージを持っていただければ、この論文の核心はつかめたはずです。

技術概要

論文「THE MCC APPROACHES THE GEOMETRIC MEAN OF PRECISION AND RECALL AS TRUE NEGATIVES APPROACH INFINITY」の技術的サマリー

この論文は、二値分類器の評価指標である**マシューズ相関係数（MCC）とフォークス・マロウズ指数（FM）**の数学的関係性、特に「真の負例（True Negatives: TN）の数が無限大に近づく極限における MCC の挙動」について論じたものです。オブジェクト検出のような「オープンワールド」問題における評価指標の限界を数学的に解明し、その証明を Lean 4 による形式検証で裏付けています。

以下に、問題定義、手法、主要な貢献、結果、および意義を詳述します。

1. 問題定義 (Problem)

機械学習モデル、特にオブジェクト検出のようなオープンワールド問題における分類性能の評価には、以下の課題が存在します。

• 混同行列の不完全性: 分類性能は通常、真陽性（TP）、真陰性（TN）、偽陽性（FP）、偽陰性（FN）の 4 つの値で構成される混同行列で記述されます。
• MCC の限界: MCC は TP, TN, FP, FN の 4 つすべての値に依存する包括的な指標ですが、オブジェクト検出では「検出されなかった背景領域（真の負例）」の数が事実上無限大（または膨大）であり、TN を正確に数えることが不可能です。
• 既存指標の欠点: F1 スコアや FM 指数は TN を無視して TP, FP, FN のみで計算されます。これらは実用的ですが、TN を完全に無視することは概念的に不満が残ります。
• 核心的な問い: 「TN の数が無限大に近づくとき、MCC はどのように振る舞うのか？」という数学的な極限問題が提起されました。

2. 手法とアプローチ (Methodology)

著者は以下の 3 つのアプローチでこの問題を解決しました。

1. 数学的極限の導出:
   • MCC の定義式（式 6）において、TN を変数とし、$TN \to \infty$ の極限を代数操作によって計算しました。
   • 分子と分母を $1/TN$ で割ることで、TN に依存する項を消去し、式を簡略化しました。
2. 数値計算による検証 (SymPy):
   • Python の記号計算ライブラリ SymPy を使用し、MCC の極限値が FM 指数と一致することを数式的に確認しました。
3. 形式検証 (Lean 4):
   • 数学的な証明の厳密性を保証するため、証明支援系 Lean 4 を用いて完全な形式化を行いました。
   • 代数操作や極限の性質（フィルタ理論に基づく Tendsto など）を厳密に定義し、機械が検証可能な形で証明を構築しました。

3. 主要な貢献 (Key Contributions)

• MCC と FM の極限関係の証明:
  TN が無限大に発散する極限において、MCC がフォークス・マロウズ指数（FM）に収束することを厳密に証明しました。
  $$\lim_{TN \to \infty} \text{MCC} = \text{FM} = \sqrt{\text{Precision} \times \text{Recall}}$$
• 分野横断的な知見の統合:
  この結果は以前、生態学分野において「$\phi$係数（MCC と同一）の極限がオキアイ指数（FM と同一）に収束する」として指摘されていましたが（文献 [8] など）、その証明が省略されていました。本論文は、機械学習（二値分類）の文脈でこれを再発見し、完全な証明を提供しました。
• Lean 4 による形式化:
  数学的証明を Lean 4 で形式化し、コードとして公開しました。これにより、証明の各ステップが機械的に検証可能となり、論理的な誤りの可能性を排除しています。
• LLM の活用事例:
  証明の形式化と関連文献の探索において、大規模言語モデル（LLM）がどのように活用されたか（特に用語の壁を越えた文献発見と、複雑な証明の形式化支援）について言及し、LLM の科学的研究における役割を示しました。

4. 結果 (Results)

• 数学的結論:
  真の負例（TN）の数が非常に大きい（無限大に近づく）状況下では、MCC は TN に依存しなくなり、結果として「適合率（Precision）」と「再現率（Recall）」の幾何平均である FM 指数と等価になります。
  • 導出プロセスでは、分母の $\sqrt{(TN+FP)(TN+FN)}$ 項が $TN$ で支配され、分子の $TP \cdot TN$ 項も $TN$ で支配されるため、$TN$ が消去され、残る項が FM の定義式と一致することが示されました。
• 形式検証の成功:
  Lean 4 による証明コードはコンパイルを通過し、定理 tendsto_MCC_atTop_eq_FM が成功裏に証明されました。これにより、直感的な代数操作が数学的に正当であることが保証されました。

5. 意義と影響 (Significance)

• オブジェクト検出評価への示唆:
  オブジェクト検出のような「TN を数えられない」タスクにおいて、MCC を計算しようとする試みが本質的に FM 指数（または F1 スコアの幾何平均版）に収束することを示しました。これは、これらの指標が「オープンワールド」設定において事実上同等の情報を提供することを意味し、評価指標の選択に関する理論的根拠を提供します。
• 指標の解釈の深化:
  MCC が「TN を含むことでより包括的である」という一般的な認識に対し、TN が膨大になる極限ではその優位性が失われる（FM と等しくなる）ことを示しました。
• 形式数学と AI の融合:
  数学的な証明を Lean 4 で形式化するプロセスにおいて、LLM が「証明の骨格作成」や「既存文献の発見」に不可欠な役割を果たしたことを実証しました。これは、数学的研究と AI ツールの協働の新たなモデルを示唆しています。
• 学際的なつながり:
  生態学と機械学習という異なる分野で用いられている指標（$\phi$係数/オキアイ指数 と MCC/FM）が、数学的に同一の極限挙動を持つことを明らかにし、分野横断的な知見の共有を促進しました。

結論

本論文は、二値分類の評価指標である MCC が、真の負例が無限大になる極限条件下で FM 指数に収束することを数学的に証明し、その証明を Lean 4 で形式化しました。これは、オブジェクト検出などのオープンワールド問題における評価指標の理論的基礎を補強するとともに、LLM を活用した数学的証明と文献調査の新しい可能性を示す重要な成果です。