Pith. sign in

REVIEW 4 major objections 5 minor 72 references

Monitoring of Static Fairness

T0 review · 4 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Runtime monitors can audit fairness of unknown Markovian decision systems from a single observed trace, with finite-sample confidence intervals that shrink over time.

desk verdict New uniform-soundness results with complete proofs, but the POMC monitor's assumptions make its guarantees nearly vacuous in the paper's own example. read the letter →

arxiv 2507.03048 v1 pith:YIRXZPQ7 submitted 2025-07-03 cs.LG cs.AI

Thomas A. Henzinger , Mahyar Karimi , Konstantin Kueffner , Kaushik Mallik This is my paper
classification cs.LGcs.AI
keywords runtimeverificationalgorithmicfairnesspartiallyobservedMarkovchainsboundedspecificationexpressionsprobabilisticconfidencesequencesdemographicparityPACguarantees
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper establishes that one long observation stream from an unknown decision-making system can serve as a quantitative fairness audit, provided the system's hidden or visible state evolves as a Markov chain. The authors design monitors that, after every observation, output a confidence interval for a specified fairness metric such as demographic parity, equal opportunity, or social burden, and they prove that the interval contains the true fairness value with a user-chosen confidence. The interval tightens as the trace grows, and the guarantee comes in two strengths: pointwise soundness at each time step, and uniform soundness over the entire verdict stream. If the central claim is correct, deployed black-box systems can be continuously audited for group fairness without ever learning their transition probabilities.

What carries the argument

The load-bearing object is the bounded specification expression (BSE): an arithmetic formula built from bounded atomic functions over sliding windows of observations, whose fair value is the limit of empirical averages along a run. Monitoring rests on three mechanisms. Stationary start makes the sliding-window average an unbiased estimator of the BSE's expectation. A Markov-chain concentration inequality with bounded differences, together with a known mixing-time bound, turns that estimator into a confidence interval; a time-uniform union bound (or, in the fully observed case, a martingale-based confidence sequence) upgrades it from pointwise to uniform soundness. For fully observed chains, PSE atoms $ρ(j|i)$ are estimated by counting edge visits, and dependent multiplications are handled by a temporal shift that makes the relevant Bernoulli trials independent, producing a single i.i.d. sequence whose mean is the PSE value.

What would settle it

Run the pointwise POMC monitor on a known ergodic Markov chain whose initial distribution is deliberately far from stationarity, while supplying a valid mixing-time bound; if a statistically significant fraction of output intervals fail to contain the true BSE value beyond the allowed $δ$, the unbiasedness assumption is falsified in practice. On stationary-start chains, a coverage experiment at many time points should track $1-δ$.

Watch

Extended reading notes

Core claim

The central claim is Theorem 5: given any bounded specification expression $φ$ (a BSE) and confidence $δ$, Algorithms 1 and 2 construct a monitor that, over the class of aperiodic, stationary-starting partially observed Markov chains with a known mixing-time bound, is $δ$-pointwise-sound with error $ε^p_{POMC}$ and $δ$-uniformly-sound with error $ε^u_{POMC}$. The monitor uses $O(k+n)$ memory and $O(k·n)$ time per observed symbol, where $k$ counts the atoms in the expression. The same framework specializes to fully observed Markov chains and the PSE fragment, where the monitor needs no mixing-time bound and attains much tighter intervals by aggregating per-state Bernoulli observations into an i.i.d. sequence. The paper also proves that the path-based (empirical-average) semantics of BSEs equals the earlier model-based semantics on irreducible positive-recurrent chains, and that the resulting estimator is unbiased exactly when the chain starts in stationarity.

Load-bearing premise

The load-bearing premise is that the unknown system has already been running long enough that its state distribution is the long-run equilibrium, and that a finite upper bound on how quickly it reaches that equilibrium is known in advance; without stationarity the point estimate is biased and the confidence interval is not guaranteed to contain the true fairness value.

Editorial extensions

If this is right

  • A single observed trace suffices for a finite-sample, PAC-style guarantee on the value of a fairness metric, so no transition model or simulator is needed.
  • Longer traces automatically shrink the reported interval, so the same monitor can be used for quick screening and later for tighter certification.
  • Uniformly sound monitors give a guarantee that holds over the entire infinite verdict stream, making them suitable for continuous compliance monitoring.
  • The full-observability PSE monitor drops the mixing-time requirement and yields tightly controlled intervals, at the price of a richer observation model.
  • Expressions with conditional probabilities, such as demographic parity, inherit division-induced interval arithmetic, which can dramatically slow convergence in practice.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The paper leaves implicit that the formal guarantee's practical value hinges on the quality of the user-supplied mixing-time bound: with a conservative bound, the lending example needs around $10^{12}$ observations to shrink the error to $0.1$, so the guarantee can be nearly vacuous even when the local estimates look reasonable.
  • Because stationarity is what makes the point estimator unbiased, a natural extension is a monitor that first tests for approximate stationarity in the observed prefix and withholds or widens its verdicts until that condition is plausible.
  • A direct empirical extension is a coverage experiment on synthetic Markov chains with known ground truth: run the monitor many times, record the fraction of intervals containing the true BSE value, and compare that fraction with $1-δ$ to validate both the pointwise and uniform bounds.
  • For dependent multiplications, the temporal-shift trick converts dependence into independence at the cost of reducing the effective sample size; comparing monitors for product-free and product-heavy specifications would quantify that price in concrete settings.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper develops runtime monitors for algorithmic fairness properties over Markov chains with unknown transition probabilities. For the partially observed case, it defines a path-based semantics for a bounded specification expression (BSE) language, introduces pointwise and uniform soundness for monitors, and proves that Algorithms 1–2 provide finite-sample PAC guarantees for aperiodic, stationary-start POMCs with a known mixing-time upper bound (Theorem 5). For the fully observed case, it restricts attention to probabilistic specification expressions (PSE) and presents Algorithm 3, which constructs an i.i.d. auxiliary sequence so that Hoeffding-type and martingale-based bounds can be applied (Theorem 12). The paper includes proofs of the main correctness claims, a comparison with prior work, and experiments on lending, college-admission, and hypercube examples.

Significance. If the technical gaps identified below are repaired, this is a valuable contribution to runtime verification and algorithmic fairness: it gives the first finite-sample, time-uniform monitoring guarantees for group-fairness metrics over partially observed Markov chains, it makes the distinction between pointwise and uniform soundness precise, and it consolidates the authors' earlier pointwise-sound results with a martingale-based uniform extension. The paper is also transparent about its own limitations, including the conservative mixing-time bound in Section 7.1 and the projection of the lending intervals. The formal framework, the use of Paulin's concentration inequality, and the stitching argument from Howard et al. are appropriate and mostly well executed. However, several load-bearing formal issues—especially the undefined monitor output for short prefixes, the randomized nature of Algorithm 3 relative to the deterministic monitor model, and the incorrect treatment of the random sample size in Lemma 15—currently prevent the stated theorems from being accepted at face value.

major comments (4)
  1. [§4, Definitions 2–3; §5.1, Algorithm 1] Definitions 2 and 3 quantify over all t ∈ N, but Algorithm 1 returns ⊥ for t < n (lines 3–5), and ⊥ is not in the output alphabet of intervals {[l,u] | l,u∈R, l<u}. As stated, Theorems 4 and 5 are therefore false for the first n−1 observation steps. Please restrict the definitions to t ≥ n or assign a formal semantics to ⊥ as a non-verdict, and adjust the statements of Theorems 4 and 5 accordingly.
  2. [§2.3, Definition 1; §6.2, Algorithm 3 (ExtractOutcome)] The paper's monitor model is deterministic: Definition 1 gives a transition function T : Σ × Φ(R) → Γ(R), and JAK is a function from finite words to outputs. Algorithm 3, however, uses random reshuffling in ExtractOutcome, so its state update is randomized and JAK is no longer a function. The probabilities in Definitions 2–3 quantify only over the POMC path, not over the monitor's internal randomness. Please extend the definitions to randomized monitors, state explicitly that soundness is over both the POMC path and the monitor's internal coins, and re-establish Theorem 12 under that semantics.
  3. [§6.3, Lemma 15 and Algorithm 3 (UpdateEst)] Lemma 15 conflates the random number n of constructed i.i.d. observations with the MC time index t. The statement uses JidK(Y_t) and εp_MC(t, δ, ...), while Algorithm 3 increments n and calls UpdateEst(w, n), and the proof says 'let n := |Y|' and then forms '1/t Σ_{i=1}^n Y_i'. Hoeffding's inequality does not directly apply when the sample size is a stopping time that may depend on the sampled values. Please state the concentration bound in terms of the deterministic length of the auxiliary sequence, or use a valid time-uniform and data-dependent bound, and make Algorithm 3's error call consistent with the theorem.
  4. [§5, Assumption 3; §7.1, lending example] Assumption 3 requires that the unknown POMC starts in its stationary distribution and that the user knows a finite upper bound on τmix, but the paper's stated goal is monitoring systems whose models are unknown. No procedure is given to obtain or validate a τmix bound from the observation stream alone, and Section 7.1 shows the practical consequences: with the cited conservative bound τmix = 170589.78, the φDP monitor needs roughly 10^12 observations to reduce ε to 0.1, and after 7×10^8 steps the measured interval is the trivial [−1,1], with the plotted tightening being a projection. The core guarantee is therefore formally correct only under assumptions that are not verifiable from the trace and can be practically vacuous; please either provide a data-driven method for τmix or substantially qualify the practical claims about monitoring unknown systems.
minor comments (5)
  1. [§3.4, Theorem 3] Theorem 3 states that the limit exists 'for every realization' of W, but the proof only establishes almost-sure convergence after entering a recurrent component; exceptional null paths in the support can fail. Please change the quantification to 'almost surely' or add a separate argument covering all paths.
  2. [§6.3, Lemma 17] Lemma 17 states that the polynomial form of φ_m has size 2^{2m+1} − 1, but its own proof concludes 2^{m+1}m − 1. These are very different quantities; please correct the statement and check that the complexity bounds in Theorem 12 and Lemma 18 use the correct value.
  3. [§5.1.2, Algorithm 2] For BSEs involving division, Algorithm 2 uses interval arithmetic on the output of a submonitor, but it does not specify what to do when the denominator interval contains 0; the expression 1/[l,u] is undefined in that case. Please state a convention, for example returning a trivial interval or treating the verdict as inconclusive.
  4. [§6.2, Algorithm 3 comment] The comment in UpdateEst contains an unresolved placeholder 'See ??'; please replace it with the appropriate equation or lemma reference.
  5. [§3, first paragraph] There is a typo in 'we pove that our new path-based semantics generalises'; it should read 'prove'.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the PAC guarantees are derived from external concentration inequalities and the ergodic theorem; self-citations are definitional continuity only.

full rationale

The central soundness results (Theorems 4, 5, and 12) are derived from three ingredients: (i) the unbiasedness of the finitary-semantics point estimator under stationarity (Lemma 7), (ii) the bounded-difference property (Lemma 8), and (iii) external concentration inequalities—Paulin's McDiarmid-style bound for Markov chains [61], Hoeffding's inequality, and Howard et al.'s time-uniform martingale bounds [39]. None of these inputs is fitted to the data that the monitors subsequently 'predict'; the only monitor inputs are the observed trace and the user-supplied confidence δ and mixing-time bound. The equivalence between path-based and model-based semantics (Theorem 2 and Lemma 1) is proved from the ergodic theorem rather than assumed. BSE and PSE definitions are reused from the authors' prior work [35, 36], but those citations supply syntax and previous semantics, not the new guarantees, and the paper includes the previously omitted proofs. The practical limitations are real but non-circular: Assumption 3 (stationary start, known τ_mix) is load-bearing, Lemma 7 fails without stationarity, and Section 7.1 admits that with the conservative τmix = 170589.78 the lending monitor's interval was trivial (the whole interval [−1, 1]) after about 7×10^8 steps, with the plotted tightening being a projection rather than measured output; this affects usefulness, not derivation. A formal gap also exists because Definitions 2 and 3 quantify over all t ∈ N while Algorithm 1 returns ⊥ for t < n, but this is a correctness bug, not a circular reduction.

Assumptions & free parameters 2 free parameters · 5 assumptions · 0 invented entities

The soundness theorems do not fit any parameter to data; they take δ, τmix, and expression bounds as inputs. The main assumptions are stationarity of the observed process, a known mixing time bound, and external concentration inequalities from the literature.

free parameters (2)
  • δ (confidence level) = 0.05 in experiments
    User-specified failure probability; appears in all soundness guarantees as the allowed error probability.
  • τmix (mixing time upper bound) = 170589.78 (lending), 204.94 (hypercube conservative), 7.45 (hypercube true)
    Assumed known input required by Theorem 6 and the εp/εu_POMC bounds; experimental interval quality depends heavily on this value.
assumptions (5)
  • domain assumption Assumption 3: POMC is irreducible, aperiodic, starts in its stationary distribution, and a finite upper bound on mixing time is known.
    Required for unbiasedness of the estimator (Lemma 7) and for the concentration inequality (Theorem 6).
  • domain assumption Assumption 4: the fully observed MC is irreducible and positively recurrent.
    Guarantees every state is visited infinitely often, needed for the Bernoulli aggregation in Section 6.
  • standard math Paulin's McDiarmid-style concentration inequality for Markov chains (Theorem 6, from [61]).
    Provides the pointwise concentration used to build εp_POMC and εu_POMC.
  • standard math Ergodic theorem (Theorem 1.10.2 of Norris [58]).
    Used in Lemma 1 to equate the path-based and model-based semantics for irreducible positively recurrent POMCs.
  • standard math Howard et al. time-uniform martingale bound (Theorem 14, from [39]).
    Used for the uniformly sound monitors over fully observed MCs (εu_MC).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Monitoring of Static Fairness." pith.science (2026). https://pith.science/paper/YIRXZPQ7

@misc{pith2026250703048,
  author       = {Pith},
  title        = {Pith review of: Monitoring of Static Fairness},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YIRXZPQ7}},
  note         = {Machine review of arXiv:2507.03048}
}
read the original abstract

Machine-learned systems are in widespread use for making decisions about humans, and it is important that they are fair, i.e., not biased against individuals based on sensitive attributes. We present a general framework of runtime verification of algorithmic fairness for systems whose models are unknown, but are assumed to have a Markov chain structure, with or without full observation of the state space. We introduce a specification language that can model many common algorithmic fairness properties, such as demographic parity, equal opportunity, and social burden. We build monitors that observe a long sequence of events as generated by a given system, and output, after each observation, a quantitative estimate of how fair or biased the system was on that run until that point in time. The estimate is proven to be correct modulo a variable error bound and a given confidence level, where the error bound gets tighter as the observed sequence gets longer. We present two categories of monitoring algorithms, namely ones with a uniform error bound across all time points, and ones with weaker non-uniform, pointwise error bounds at different time points. Our monitoring algorithms use statistical tools that are adapted to suit the dynamic requirements of monitoring and the special needs of the fairness specifications. Using a prototype implementation, we show how we can monitor if a bank is fair in giving loans to applicants from different social backgrounds, and if a college is fair in admitting students while maintaining a reasonable financial burden on the society. In these experiments, our monitors took less than a millisecond to update their verdicts after each observation.

Figures

Figures reproduced from arXiv: 2507.03048 by the authors.

Figure 1
Figure 1. The POMCs modeling the sequential interaction between the bank [PITH_FULL_IMAGE:figures/full_fig_p008_1.png] view at source ↗
Figure 2
Figure 2. Variation of ratio of the est. error using the existing approach [3] to [PITH_FULL_IMAGE:figures/full_fig_p038_2.png] view at source ↗
Figure 3
Figure 3. Confidence interval comparison for uniformly sound monitors using [PITH_FULL_IMAGE:figures/full_fig_p039_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Monitoring φDP (first, third) and φTDP (second, fourth) on the lending (first, second) and the hypercube (third, fourth) examples. The first and second plots show the computed 95%-confidence interval (solid) and the true value of the property (dashed) for the lending P…
Figure 5
Figure 5. Figure 5: Markov chains for the lending and the college-admission examples. [PITH_FULL_IMAGE:figures/full_fig_p042_5.png]
Figure 6
Figure 6. Figure 6: The plots show the 95% confidence intervals estimated by the mon [PITH_FULL_IMAGE:figures/full_fig_p043_6.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

72 extracted references · 67 canonical work pages

  1. [1]

    A survey of statistical model checking

    Gul Agha and Karl Palmskog. A survey of statistical model checking. ACM Transactions on Modeling and Computer Simulation (TOMACS) , 28(1):1– 39, 2018

    work page 2018

  2. [2]

    Fairsquare: probabilistic verification of program fairness

    Aws Albarghouthi, Loris D’Antoni, Samuel Drews, and Aditya V Nori. Fairsquare: probabilistic verification of program fairness. Proceedings of the ACM on Programming Languages , 1(OOPSLA):1–30, 2017

    work page 2017

  3. [3]

    Fairness-aware programming

    Aws Albarghouthi and Samuel Vinitsky. Fairness-aware programming. In Proceedings of the Conference on Fairness, Accountability, and Trans- parency, pages 211–219, 2019

    work page 2019

  4. [4]

    Pac statistical model checking for markov decision processes and stochastic games

    Pranav Ashok, Jan Kˇ ret ´ ınsk` y, and Maximilian Weininger. Pac statistical model checking for markov decision processes and stochastic games. In International Conference on Computer Aided Verification , pages 497–519. Springer, 2019

    work page 2019

  5. [5]

    Baier, B

    C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model-checking algorithms for continuous-time markov chains. IEEE Transactions on Soft- ware Engineering, 29(6):524–541, 2003

    work page 2003

  6. [6]

    Fair normalizing flows

    Mislav Balunovic, Anian Ruoss, and Martin Vechev. Fair normalizing flows. In International Conference on Learning Representations , 2021

    work page 2021

  7. [7]

    Specification- based monitoring of cyber-physical systems: a survey on theory, tools and applications

    Ezio Bartocci, Jyotirmoy Deshmukh, Alexandre Donz´ e, Georgios Fainekos, Oded Maler, Dejan Niˇ ckovi´ c, and Sriram Sankaranarayanan. Specification- based monitoring of cyber-physical systems: a survey on theory, tools and applications. In Lectures on Runtime Verification, pages 135–175. Springer, 2018. 44

    work page 2018

  8. [8]

    Springer, 2018

    Ezio Bartocci and Yli` es Falcone, editors.Lectures on Runtime Verification - Introductory and Advanced Topics , volume 10457 of Lecture Notes in Computer Science. Springer, 2018

    work page 2018

Show all 72 references
  1. [9]

    Probabilistic verification of fairness properties via concentration.Proceedings of the ACM on Programming Languages, 3(OOPSLA):1–27, 2019

    Osbert Bastani, Xin Zhang, and Armando Solar-Lezama. Probabilistic verification of fairness properties via concentration.Proceedings of the ACM on Programming Languages, 3(OOPSLA):1–27, 2019

    2019

  2. [10]

    Ai fairness 360: An extensi- ble toolkit for detecting and mitigating algorithmic bias

    Rachel KE Bellamy, Kuntal Dey, Michael Hind, Samuel C Hoffman, Stephanie Houde, Kalapriya Kannan, Pranay Lohia, Jacquelyn Martino, Sameep Mehta, Aleksandra Mojsilovi´ c, et al. Ai fairness 360: An extensi- ble toolkit for detecting and mitigating algorithmic bias. IBM Journal ...

    2019

  3. [11]

    A convex frame- work for fair regression

    Richard Berk, Hoda Heidari, Shahin Jabbari, Matthew Joseph, Michael Kearns, Jamie Morgenstern, Seth Neel, and Aaron Roth. A convex frame- work for fair regression. arXiv preprint arXiv:1706.02409 , 2017

    2017 arXiv

  4. [12]

    Fairlearn: A toolkit for assessing and improving fairness in ai

    Sarah Bird, Miro Dudik, Richard Edgar, Brandon Horn, Roman Lutz, Vanessa Milan, Mehrnoosh Sameki, Hanna Wallach, and Kathleen Walker. Fairlearn: A toolkit for assessing and improving fairness in ai. Microsoft, Tech. Rep. MSR-TR-2020-32, 2020

    2020

  5. [13]

    Fairness shields: Safeguarding against biased decision makers

    Filip Cano, Thomas A Henzinger, Bettina K¨ onighofer, Konstantin Ku- effner, and Kaushik Mallik. Fairness shields: Safeguarding against biased decision makers. In Proceedings of the AAAI Conference on Artificial In- telligence, volume 39, pages 15659–15668, 2025

    2025

  6. [14]

    Fair prediction with disparate impact: A study of bias in recidivism prediction instruments

    Alexandra Chouldechova. Fair prediction with disparate impact: A study of bias in recidivism prediction instruments. Big data , 5(2):153–163, 2017

    2017

  7. [15]

    Statistical model checking for cyber- physical systems

    Edmund M Clarke and Paolo Zuliani. Statistical model checking for cyber- physical systems. In International symposium on automated technology for verification and analysis , pages 1–12. Springer, 2011

    2011

  8. [16]

    Algorithmic decision making and the cost of fairness

    Sam Corbett-Davies, Emma Pierson, Avi Feller, Sharad Goel, and Aziz Huq. Algorithmic decision making and the cost of fairness. In Proceedings of the 23rd acm sigkdd international conference on knowledge discovery and data mining , pages 797–806, 2017

    2017

  9. [17]

    Sculley, and Yoni Halpern

    Alexander D’Amour, Hansa Srinivasan, James Atwood, Pallavi Baljekar, D. Sculley, and Yoni Halpern. Fairness is not static: Deeper understanding of long term fairness via simulation studies. In Proceedings of the 2020 Conference on Fairness, Accountability, and Transparency, F ...

    2020

  10. [18]

    Optimizing control strategy using statistical model checking

    Alexandre David, Dehui Du, Kim Guldstrand Larsen, Axel Legay, and Marius Mikuˇ cionis. Optimizing control strategy using statistical model checking. In NASA Formal Methods Symposium , pages 352–367. Springer, 2013. 45

    2013

  11. [19]

    Robust satisfaction of temporal logic over real-valued signals

    Alexandre Donz´ e and Oded Maler. Robust satisfaction of temporal logic over real-valued signals. In International Conference on Formal Modeling and Analysis of Timed Systems , pages 92–106. Springer, 2010

    2010

  12. [20]

    The accuracy, fairness, and limits of predict- ing recidivism

    Julia Dressel and Hany Farid. The accuracy, fairness, and limits of predict- ing recidivism. Science advances, 4(1):eaao5580, 2018

    2018

  13. [21]

    Fairness through awareness

    Cynthia Dwork, Moritz Hardt, Toniann Pitassi, Omer Reingold, and Richard Zemel. Fairness through awareness. In Proceedings of the 3rd in- novations in theoretical computer science conference, pages 214–226, 2012

    2012

  14. [22]

    Individual fairness under compo- sition

    Cynthia Dwork and Christina Ilvento. Individual fairness under compo- sition. Proceedings of Fairness, Accountability, Transparency in Machine Learning, 2018

    2018

  15. [23]

    Runaway feedback loops in predictive polic- ing

    Danielle Ensign, Sorelle A Friedler, Scott Neville, Carlos Scheidegger, and Suresh Venkatasubramanian. Runaway feedback loops in predictive polic- ing. In Conference on Fairness, Accountability and Transparency , pages 160–171. PMLR, 2018

    2018

  16. [24]

    Concentration without independence via information measures

    Amedeo Roberto Esposito and Marco Mondelli. Concentration without independence via information measures. arXiv preprint arXiv:2303.07245 , 2023

    2023 arXiv

  17. [25]

    Real-time stream-based monitoring

    Peter Faymonville, Bernd Finkbeiner, Maximilian Schwenger, and Hazem Torfah. Real-time stream-based monitoring. arXiv preprint arXiv:1711.03829, 2017

    2017 arXiv

  18. [26]

    Certifying and removing disparate im- pact

    Michael Feldman, Sorelle A Friedler, John Moeller, Carlos Scheidegger, and Suresh Venkatasubramanian. Certifying and removing disparate im- pact. In proceedings of the 21th ACM SIGKDD international conference on knowledge discovery and data mining , pages 259–268, 2015

    2015

  19. [27]

    Monitoring event frequencies

    Thomas Ferrere, Thomas A Henzinger, and Bernhard Kragl. Monitoring event frequencies. In 28th EACSL Annual Conference on Computer Science Logic, volume 152, 2020

    2020

  20. [28]

    A theory of reg- ister monitors

    Thomas Ferr` ere, Thomas A Henzinger, and N Ege Sara¸ c. A theory of reg- ister monitors. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science , pages 394–403, 2018

    2018

  21. [29]

    Collecting statistics over runtime executions

    Bernd Finkbeiner, Sriram Sankaranarayanan, and Henny Sipma. Collecting statistics over runtime executions. Electronic Notes in Theoretical Com- puter Science, 70(4):36–54, 2002

    2002

  22. [30]

    Al- gorithmic fairness verification with graphical models

    Bishwamittra Ghosh, Debabrota Basu, and Kuldeep S Meel. Al- gorithmic fairness verification with graphical models. arXiv preprint arXiv:2109.09447, 2021. 46

    2021 arXiv

  23. [31]

    Justicia: A stochastic sat approach to formally verify fairness

    Bishwamittra Ghosh, Debabrota Basu, and Kuldeep S Meel. Justicia: A stochastic sat approach to formally verify fairness. In Proceedings of the AAAI Conference on Artificial Intelligence , volume 35, pages 7554–7563, 2021

    2021

  24. [32]

    Monitoring robustness and individual fairness

    Ashutosh Gupta, Thomas A Henzinger, Konstantin Kueffner, Kaushik Mallik, and David Pape. Monitoring robustness and individual fairness. arXiv preprint arXiv:2506.00496 , 2025

    2025 arXiv

  25. [33]

    Equality of opportunity in supervised learning

    Moritz Hardt, Eric Price, and Nati Srebro. Equality of opportunity in supervised learning. Advances in neural information processing systems , 29, 2016

    2016

  26. [34]

    Runtime monitoring of dynamic fairness properties

    Thomas Henzinger, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik. Runtime monitoring of dynamic fairness properties. In Proceed- ings of the 2023 ACM Conference on Fairness, Accountability, and Trans- parency, pages 604–614, 2023

    2023

  27. [35]

    Monitoring algorithmic fairness

    Thomas A Henzinger, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik. Monitoring algorithmic fairness. In International Conference on Computer Aided Verification, pages 358–382. Springer, 2023

    2023

  28. [36]

    Mon- itoring algorithmic fairness under partial observations

    Thomas A Henzinger, Konstantin Kueffner, and Kaushik Mallik. Mon- itoring algorithmic fairness under partial observations. In International Conference on Runtime Verification, pages 291–311. Springer, 2023

    2023

  29. [37]

    Monitorability under assumptions

    Thomas A Henzinger and N Ege Sara¸ c. Monitorability under assumptions. In International Conference on Runtime Verification, pages 3–18. Springer, 2020

    2020

  30. [38]

    Quantitative and approximate mon- itoring

    Thomas A Henzinger and N Ege Sara¸ c. Quantitative and approximate mon- itoring. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–14. IEEE, 2021

    2021

  31. [39]

    Time-uniform, nonparametric, nonasymptotic confidence sequences

    Steven R Howard, Aaditya Ramdas, Jon McAuliffe, and Jasjeet Sekhon. Time-uniform, nonparametric, nonasymptotic confidence sequences. The Annals of Statistics , 49(2):1055–1080, 2021

    2021

  32. [40]

    Differentially pri- vate fair learning

    Matthew Jagielski, Michael Kearns, Jieming Mao, Alina Oprea, Aaron Roth, Saeed Sharifi-Malvajerdi, and Jonathan Ullman. Differentially pri- vate fair learning. In International Conference on Machine Learning, pages 3000–3008. PMLR, 2019

    2019

  33. [41]

    General mixing time bounds for finite markov chains via the absolute spectral gap

    Daniel Jerison. General mixing time bounds for finite markov chains via the absolute spectral gap. arXiv preprint arXiv:1310.8021 , 2013

    2013 arXiv

  34. [42]

    Ver- ifying individual fairness in machine learning models

    Philips George John, Deepak Vijaykeerthy, and Diptikalyan Saha. Ver- ifying individual fairness in machine learning models. In Conference on Uncertainty in Artificial Intelligence , pages 749–758. PMLR, 2020. 47

    2020

  35. [43]

    Runtime monitors for markov decision processes

    Sebastian Junges, Hazem Torfah, and Sanjit A Seshia. Runtime monitors for markov decision processes. In International Conference on Computer Aided Verification, pages 553–576. Springer, 2021

    2021

  36. [44]

    Data preprocessing techniques for clas- sification without discrimination

    Faisal Kamiran and Toon Calders. Data preprocessing techniques for clas- sification without discrimination. Knowledge and information systems , 33(1):1–33, 2012

    2012

  37. [45]

    Preventing fairness gerrymandering: Auditing and learning for subgroup fairness

    Michael Kearns, Seth Neel, Aaron Roth, and Zhiwei Steven Wu. Preventing fairness gerrymandering: Auditing and learning for subgroup fairness. In International Conference on Machine Learning , pages 2564–2572. PMLR, 2018

    2018

  38. [46]

    Inherent Trade-Offs in the Fair Determination of Risk Scores

    Jon Kleinberg, Sendhil Mullainathan, and Manish Raghavan. Inherent Trade-Offs in the Fair Determination of Risk Scores. In Christos H. Pa- padimitriou, editor, 8th Innovations in Theoretical Computer Science Con- ference (ITCS 2017) , volume 67 of Leibniz International Proceed...

    2017

  39. [47]

    Fairness-aware pac learn- ing from corrupted data

    Nikola H Konstantinov and Christoph Lampert. Fairness-aware pac learn- ing from corrupted data. Journal of Machine Learning Research, 23, 2022

    2022

  40. [48]

    Concentration of measure with- out independence: a unified approach via the martingale method

    Aryeh Kontorovich and Maxim Raginsky. Concentration of measure with- out independence: a unified approach via the martingale method. In Con- vexity and Concentration , pages 183–210. Springer, 2017

    2017

  41. [49]

    Coun- terfactual fairness

    Matt J Kusner, Joshua Loftus, Chris Russell, and Ricardo Silva. Coun- terfactual fairness. Advances in neural information processing systems , 30, 2017

    2017

  42. [50]

    ifair: Learning individually fair data representations for algorithmic decision making

    Preethi Lahoti, Krishna P Gummadi, and Gerhard Weikum. ifair: Learning individually fair data representations for algorithmic decision making. In 2019 ieee 35th international conference on data engineering (icde) , pages 1334–1345. IEEE, 2019

    2019

  43. [51]

    Markov chains and mixing times , volume

    David A Levin and Yuval Peres. Markov chains and mixing times , volume

  44. [52]

    Delayed impact of fair machine learning

    Lydia T Liu, Sarah Dean, Esther Rolf, Max Simchowitz, and Moritz Hardt. Delayed impact of fair machine learning. In International Conference on Machine Learning, pages 3150–3158. PMLR, 2018

    2018

  45. [53]

    To predict and serve? Significance, 13(5):14–19, 2016

    Kristian Lum and William Isaac. To predict and serve? Significance, 13(5):14–19, 2016

    2016

  46. [54]

    Monitoring temporal properties of contin- uous signals

    Oded Maler and Dejan Nickovic. Monitoring temporal properties of contin- uous signals. In International Symposium on Formal Techniques in Real- Time and Fault-Tolerant Systems , pages 152–166. Springer, 2004. 48

    2004

  47. [55]

    A survey on bias and fairness in machine learning

    Ninareh Mehrabi, Fred Morstatter, Nripsuta Saxena, Kristina Lerman, and Aram Galstyan. A survey on bias and fairness in machine learning. ACM Computing Surveys (CSUR) , 54(6):1–35, 2021

    2021

  48. [56]

    Certifying robustness to programmable data bias in decision trees

    Anna Meyer, Aws Albarghouthi, and Loris D’Antoni. Certifying robustness to programmable data bias in decision trees. Advances in Neural Informa- tion Processing Systems, 34:26276–26288, 2021

    2021

  49. [57]

    The social cost of strategic classification

    Smitha Milli, John Miller, Anca D Dragan, and Moritz Hardt. The social cost of strategic classification. In Proceedings of the Conference on Fairness, Accountability, and Transparency, pages 230–239, 2019

    2019

  50. [58]

    J. R. Norris. Markov Chains . Cambridge Series in Statistical and Proba- bilistic Mathematics. Cambridge University Press, 1997

    1997

  51. [59]

    Dissecting racial bias in an algorithm used to manage the health of populations

    Ziad Obermeyer, Brian Powers, Christine Vogeli, and Sendhil Mul- lainathan. Dissecting racial bias in an algorithm used to manage the health of populations. Science, 366(6464):447–453, 2019

    2019

  52. [60]

    Quantita- tive automata under probabilistic semantics

    Jan Otop, Thomas A Henzinger, and Krishnendu Chatterjee. Quantita- tive automata under probabilistic semantics. Logical Methods in Computer Science, 15, 2019

    2019

  53. [61]

    Concentration inequalities for markov chains by marton couplings and spectral methods

    Daniel Paulin. Concentration inequalities for markov chains by marton couplings and spectral methods. 2015

    2015

  54. [62]

    How computers see gender: An evaluation of gender classification in commer- cial facial analysis services

    Morgan Klaus Scheuerman, Jacob M Paul, and Jed R Brubaker. How computers see gender: An evaluation of gender classification in commer- cial facial analysis services. Proceedings of the ACM on Human-Computer Interaction, 3(CSCW):1–33, 2019

    2019

  55. [63]

    Chexclusion: Fairness gaps in deep chest x-ray classifiers

    Laleh Seyyed-Kalantari, Guanxiong Liu, Matthew McDermott, Irene Y Chen, and Marzyeh Ghassemi. Chexclusion: Fairness gaps in deep chest x-ray classifiers. In BIOCOMPUTING 2021: proceedings of the Pacific symposium, pages 232–243. World Scientific, 2020

    2021

  56. [64]

    Average indi- vidual fairness: Algorithms, generalization and experiments

    Saeed Sharifi-Malvajerdi, Michael Kearns, and Aaron Roth. Average indi- vidual fairness: Algorithms, generalization and experiments. Advances in Neural Information Processing Systems , 32, 2019

    2019

  57. [65]

    Runtime verification with state estimation

    Scott D Stoller, Ezio Bartocci, Justin Seyster, Radu Grosu, Klaus Havelund, Scott A Smolka, and Erez Zadok. Runtime verification with state estimation. In International conference on runtime verification, pages 193–207. Springer, 2011

    2011

  58. [66]

    Probabilistic verification of neural networks against group fairness

    Bing Sun, Jun Sun, Ting Dai, and Lijun Zhang. Probabilistic verification of neural networks against group fairness. In International Symposium on Formal Methods, pages 83–102. Springer, 2021. 49

    2021

  59. [67]

    Bias preserva- tion in machine learning: the legality of fairness metrics under eu non- discrimination law

    Sandra Wachter, Brent Mittelstadt, and Chris Russell. Bias preserva- tion in machine learning: the legality of fairness metrics under eu non- discrimination law. W. Va. L. Rev. , 123:735, 2020

    2020

  60. [68]

    The what-if tool: Interactive prob- ing of machine learning models

    James Wexler, Mahima Pushkarna, Tolga Bolukbasi, Martin Wattenberg, Fernanda Vi´ egas, and Jimbo Wilson. The what-if tool: Interactive prob- ing of machine learning models. IEEE transactions on visualization and computer graphics, 26(1):56–65, 2019

    2019

  61. [69]

    Probabilistic verification of dis- crete event systems using acceptance sampling

    H ˚ akan LS Younes and Reid G Simmons. Probabilistic verification of dis- crete event systems using acceptance sampling. InInternational Conference on Computer Aided Verification , pages 223–235. Springer, 2002

    2002

  62. [70]

    Fairness constraints: A flexible approach for fair clas- sification

    Muhammad Bilal Zafar, Isabel Valera, Manuel Gomez-Rodriguez, and Kr- ishna P Gummadi. Fairness constraints: A flexible approach for fair clas- sification. The Journal of Machine Learning Research , 20(1):2737–2778, 2019

    2019

  63. [71]

    Learning fair representations

    Rich Zemel, Yu Wu, Kevin Swersky, Toni Pitassi, and Cynthia Dwork. Learning fair representations. In International conference on machine learning, pages 325–333. PMLR, 2013. 50

    2013

  64. [107]

    American Mathematical Soc., 2017

    2017

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.