Lax Lean Archive

Panoptic Quality as a function of its four counts

Lax303562.PanopticQuality · concepts/Lax303562/PanopticQuality.lean · lax-303562

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    The Panoptic Quality of an instance segmentation (Kirillov et al., 2019) scores a set of predicted instances against a set of annotated instances. Predictions and annotations are matched by intersection over union; a matched pair is a true positive, an unmatched prediction a false positive, an unmatched annotation a false negative. The metric is

    PQ=∑matched pairsIoU∣TP∣+12∣FP∣+12∣FN∣.\mathrm{PQ} = \frac{\sum_{\text{matched pairs}} \mathrm{IoU}}{|TP| + \tfrac12 |FP| + \tfrac12 |FN|}.

    Everything in this submission is a statement about this quotient as a function of four numbers: the sum ss of the matched IoUs, the number nn of matched pairs, and the counts fpfp and fnfn of false positives and false negatives. How the matching is produced is a separate question, treated in MatchingMatching.

    The denominator is defined on its own because every result below is an exact statement about how it moves when one count changes.

    Concept map
    1 concept; 5 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Data.Real.Basic
    2
    3/-!
    4---
    5title: Panoptic Quality as a function of its four counts
    6type: definition
    7---
    8The *Panoptic Quality* of an instance segmentation (Kirillov et al., 2019) scores
    9a set of predicted instances against a set of annotated instances. Predictions and
    10annotations are matched by intersection over union; a matched pair is a *true
    11positive*, an unmatched prediction a *false positive*, an unmatched annotation a
    12*false negative*. The metric is
    13
    14PQ=∑matched pairsIoU∣TP∣+12∣FP∣+12∣FN∣.\mathrm{PQ} = \frac{\sum_{\text{matched pairs}} \mathrm{IoU}}{|TP| + \tfrac12 |FP| + \tfrac12 |FN|}.
    15
    16Everything in this submission is a statement about this quotient as a function of
    17four numbers: the sum `s` of the matched IoUs, the number `n` of matched pairs,
    18and the counts `fp` and `fn` of false positives and false negatives. How the
    19matching is produced is a separate question, treated in `Matching`.
    20
    21The denominator is defined on its own because every result below is an exact
    22statement about how it moves when one count changes.
    23-/
    24
    25namespace Lax303562.PanopticQuality
    26
    27/-- The denominator of Panoptic Quality: matched pairs count `1`, unmatched
    28predictions and unmatched annotations count `½` each. -/
    29noncomputable def den (n fp fn : ℕ) : ℝ := (n : ℝ) + (fp + fn) / 2
    30
    31/-- Panoptic Quality: the sum `s` of the matched IoUs over the denominator. -/
    32noncomputable def pq (s : ℝ) (n fp fn : ℕ) : ℝ := s / den n fp fn
    33
    34end Lax303562.PanopticQuality
    35
    Builds on

    none

    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…