Probabilistic verification of fairness properties via concentration
Open accessAbstract
As machine learning systems are increasingly used to make real world legal and financial decisions, it is of paramount importance that we develop algorithms to verify that these systems do not discriminate against minorities. We design a scalable algorithm for verifying fairness specifications. Our algorithm obtains strong correctness guarantees based on adaptive concentration inequalities; such inequalities enable our algorithm to adaptively take samples until it has enough data to make a decision. We implement our algorithm in a tool called VeriFair, and show that it scales to large machine learning models, including a deep recurrent neural network that is more than five orders of magnitude larger than the largest previously-verified neural network. While our technique only gives probabilistic guarantees due to the use of random samples, we show that we can choose the probability of error to be extremely small.
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Integrity signals
Registry
Cites
Statistics
Claims the paper makes
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
Probabilistic verification of fairness measures via the sampling of sensitive variables has been proposed to evaluate a trained model within some (small) confidence bound.
“Probabilistic veriication (e.g.[18]) of fairness measures via the sampling of sensitive variables has also been proposed to evaluate a trained model within some (small) conidence bound.”
From Fairness in machine learning: A survey (2024) · cites this paper as [18]
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
The self-check needs the paper’s full text.
Cites
Probability Inequalities for sums of Bounded Random Variables
Hoeffding, W. (1994) · Springer series in statistics · doi:10.1007/978-1-4612-0865-5_26 · Cited by 6,683 · see citing works
Probability Inequalities for Sums of Bounded Random Variables
Hoeffding, W. (1963) · Journal of the American Statistical Association · doi:10.1080/01621459.1963.10500830 · Cited by 4,869 · see citing works
Dwork, C., Hardt, M., Pitassi, T., Reingold, O., & Zemel, R. (2012) · Proceedings of the 3rd Innovations in Theoretical Computer Science Conference · doi:10.1145/2090236.2090255 · Cited by 3,501 · see citing works
Barocas, S., & Selbst, A. D. (2014) · doi:10.2139/ssrn.2477899 · Cited by 3,048 · see citing works
The complexity of computing the permanent
Valiant, L. G. (1979) · Theoretical Computer Science · doi:10.1016/0304-3975(79)90044-6 · Cited by 2,705 · see citing works
Equality of Opportunity in Supervised Learning
Hardt, M., Price, E., & Srebro, N. (2016) · arXiv · doi:10.48550/arxiv.1610.02413 · Cited by 2,536 · see citing works
Certifying and Removing Disparate Impact
Feldman, M., Friedler, S. A., Moeller, J., Scheidegger, C., & Venkatasubramanian, S. (2015) · Proceedings of the 21th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining · doi:10.1145/2783258.2783311 · Cited by 1,827 · see citing works
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
Katz, G., Barrett, C., Dill, D. L., Julian, K., & Kochenderfer, M. J. (2017) · Lecture Notes in Computer Science · doi:10.1007/978-3-319-63387-9_5 · Cited by 1,706 · see citing works
Sequential Tests of Statistical Hypotheses
Wald, A. (1992) · Springer series in statistics · doi:10.1007/978-1-4612-0919-5_18 · Cited by 1,365 · see citing works
Algorithmic Decision Making and the Cost of Fairness
Corbett-Davies, S., Pierson, E., Feller, A., Goel, S., & Huq, A. (2017) · Proceedings of the 23rd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining · doi:10.1145/3097983.3098095 · Cited by 1,149 · see citing works
(2013) · Cited by 1,126 · see citing works
AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation
Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., & Vechev, M. T. (2018) · IEEE Symposium on Security and Privacy · doi:10.1109/sp.2018.00058 · Cited by 1,038 · see citing works
Kusner, M. J., Loftus, J. R., Russell, C., & Silva, R. (2017) · arXiv · doi:10.48550/arxiv.1703.06856 · Cited by 995 · see citing works
Inherent trade-offs in the fair determination of risk scores
Kleinberg, J., Mullainathan, S., & Raghavan, M. (2017) · Schloss Dagstuhl – Leibniz-Zentrum für Informatik · doi:10.4230/lipics.itcs.2017.43 · Cited by 943 · cited 1× · see citing works
“For example, we can straightforwardly support other kinds of fairness for supervised learning [Galhotra et al. 2017; Kleinberg et al. 2017; Zafar et al. 2017].”
MethodSafety Verification of Deep Neural Networks
Huang, X., Kwiatkowska, M., Wang, S., & Wu, M. (2017) · Lecture notes in computer science · doi:10.1007/978-3-319-63387-9_1 · Cited by 854 · see citing works
PRISM: Probabilistic Symbolic Model Checker
Kwiatkowska, M., Norman, G., & Parker, D. (2002) · Computer Performance Evaluation / TOOLS · doi:10.1007/3-540-46029-2_13 · Cited by 834 · see citing works
Three naive Bayes approaches for discrimination-free classification.
Calders, T., & Verwer, S. (2010) · Data Mining and Knowledge Discovery · doi:10.1007/s10618-010-0190-x · Cited by 764 · see citing works
Discrimination-aware data mining
Pedreshi, D., Ruggieri, S., & Turini, F. (2008) · Proceedings of the 14th ACM SIGKDD international conference on Knowledge discovery and data mining · doi:10.1145/1401890.1401959 · Cited by 676 · see citing works
Zafar, M. B., Valera, I., Gomez Rodriguez, M., & Gummadi, K. P. (2017) · Proceedings of the 26th International Conference on World Wide Web · doi:10.1145/3038912.3052660 · Cited by 632 · see citing works
Certified Defenses against Adversarial ExamplesPreprint
Raghunathan, A., Steinhardt, J., & Liang, P. (2018) · arXiv (Cornell University) · doi:10.48550/arxiv.1801.09344 · Cited by 572 · see citing works
A Neural Representation of Sketch DrawingsPreprint
Ha, D., & Eck, D. (2017) · arXiv (Cornell University) · doi:10.48550/arxiv.1704.03477 · Cited by 538 · see citing works
Building Classifiers with Independency Constraints
Calders, T., Kamiran, F., & Pechenizkiy, M. (2009) · 2009 IEEE International Conference on Data Mining Workshops · doi:10.1109/icdmw.2009.83 · Cited by 468 · see citing works
Optimized Pre-Processing for Discrimination Prevention
Calmon, F. P., Wei, D., Vinzamuri, B., Ramamurthy, K. N., & Varshney, K. R. (2017) · neural information processing systems · Cited by 459 · see citing works
Statistical Model Checking: An Overview
Legay, A., Delahaye, B., & Bensalem, S. (2010) · Lecture notes in computer science · doi:10.1007/978-3-642-16612-9_11 · Cited by 426 · see citing works
Fairness testing: testing software for discrimination
Galhotra, S., Brun, Y., & Meliou, A. (2017) · Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering · doi:10.1145/3106237.3106277 · Cited by 405 · see citing works
Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling
Younes, H. L. S., & Simmons, R. G. (2002) · Lecture notes in computer science · doi:10.1007/3-540-45657-0_17 · Cited by 373 · see citing works
Gordon, A. D., Henzinger, T. A., Nori, A. V., & Rajamani, S. K. (2014) · Future of Software Engineering (FOSE) · doi:10.1145/2593882.2593900 · Cited by 372 · see citing works
Avoiding Discrimination through Causal Reasoning
Kilbertus, N., Rojas-Carulla, M., Parascandolo, G., Hardt, M., Janzing, D., & Schölkopf, B. (2017) · arXiv · doi:10.48550/arxiv.1706.02744 · Cited by 358 · see citing works
A Methodology for Direct and Indirect Discrimination Prevention in Data Mining
Hajian, S., & Domingo-Ferrer, J. (2013) · IEEE Transactions on Knowledge and Data Engineering · doi:10.1109/tkde.2012.72 · Cited by 312 · see citing works
Approximate Probabilistic Model Checking
Thomas Herault, A., Lassaigne, R., Magniette, F., & Sylvain Peyronnet, D. (2004) · Lecture notes in computer science · doi:10.1007/978-3-540-24622-0_8 · Cited by 300 · see citing works
Statistical Model Checking of Black-Box Probabilistic Systems
Sen, K., Viswanathan, M., & Agha, G. (2004) · Lecture notes in computer science · doi:10.1007/978-3-540-27813-9_16 · Cited by 285 · see citing works
Measuring Neural Net Robustness with ConstraintsPreprint
Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A., & Criminisi, A. (2016) · arXiv (Cornell University) · doi:10.17863/cam.26484 · Cited by 257 · see citing works
Self-citationOn Statistical Model Checking of Stochastic Systems
Sen, K., Viswanathan, M., & Agha, G. (2005) · Lecture notes in computer science · doi:10.1007/11513988_26 · Cited by 241 · see citing works
Lawrence, J. (1991) · Mathematics of Computation · doi:10.1090/s0025-5718-1991-1079024-2 · Cited by 202 · see citing works
Statistical probabilistic model checking with a focus on time-bounded properties
Younes, H. L. S., & Simmons, R. G. (2006) · Information and Computation · doi:10.1016/j.ic.2006.05.002 · Cited by 194 · see citing works
Statistical Model Checking for Cyber-Physical Systems
Clarke, E. M., & Zuliani, P. (2011) · Lecture notes in computer science · doi:10.1007/978-3-642-24372-1_1 · Cited by 176 · see citing works
A Confidence-Based Approach for Balancing Fairness and Accuracy
Fish, B., Kun, J., & Lelkes, Á. D. (2016) · SIAM International Conference on Data Mining · doi:10.1137/1.9781611974348.17 · Cited by 163 · see citing works
PSI: Exact Symbolic Inference for Probabilistic Programs
Gehr, T., Misailovíc, S., & Vechev, M. (2016) · Lecture notes in computer science · doi:10.1007/978-3-319-41528-4_4 · Cited by 161 · see citing works
Grosu, R., & Smolka, S. A. (2005) · Lecture notes in computer science · doi:10.1007/978-3-540-31980-1_18 · Cited by 148 · see citing works
Probabilistic symbolic execution
Geldenhuys, J., Dwyer, M. B., & Visser, W. (2012) · International Symposium on Software Testing and Analysis · doi:10.1145/2338965.2336773 · Cited by 146 · see citing works
Inherent Trade-Offs in Algorithmic Fairness
Kleinberg, J. (2018) · Abstracts of the 2018 ACM International Conference on Measurement and Modeling of Computer Systems · doi:10.1145/3219617.3219634 · Cited by 125 · see citing works
Ramesh Johari, B., Koomen, P., Pekelis, L., & Walsh, D. (2017) · ACM SIGKDD Conference on Knowledge Discovery and Data Mining (KDD) · doi:10.1145/3097983.3097992 · Cited by 124 · see citing works
Static analysis for probabilistic programs
Sankaranarayanan, S., Chakarov, A., & Gulwani, S. (2013) · Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation · doi:10.1145/2491956.2462179 · Cited by 123 · see citing works
Lakkaraju, H., Kleinberg, J., Leskovec, J., Ludwig, J., & Mullainathan, S. (2017) · Proceedings of the 23rd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining · doi:10.1145/3097983.3098066 · Cited by 110 · see citing works
Abstract Interpretation of Probabilistic Semantics
Monniaux, D. P. (2000) · Lecture notes in computer science · doi:10.1007/978-3-540-45099-3_17 · Cited by 108 · see citing works
Biddle, D. (2005) · Cited by 101 · see citing works
FairSquare: probabilistic verification of program fairness
Albarghouthi, A., D'Antoni, L., Drews, S., & Nori, A. V. (2017) · Proceedings of the ACM on Programming Languages · doi:10.1145/3133904 · Cited by 94 · see citing works
Expressing and verifying probabilistic assertions
Sampson, A., Panchekha, P., Mytkowicz, T., McKinley, K. S., Grossman, D., & Ceze, L. (2014) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/2594291.2594294 · Cited by 89 · see citing works
Understanding Discrimination in the Scored SocietyPreprint
Zarsky, T. (2014) · SSRN Electronic Journal · Cited by 81 · see citing works
Bayesian inference using data flow analysis
Claret, G., Rajamani, S. K., Nori, A. V., Gordon, A. D., & Borgström, J. (2013) · ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) · doi:10.1145/2491411.2491423 · Cited by 65 · see citing works
Transparent Data Mining for Big and Small Data
Cerquitelli, T., Cerquitelli, T., Quercia, D., & Pasquale, F. (2017) · Studies in big data · doi:10.1007/978-3-319-54024-5 · Cited by 61 · see citing works
An Abstract Monte-Carlo Method for the Analysis of Probabilistic Programs
Monniaux, D. P. (2001) · Cited by 44 · see citing works
Static analysis for probabilistic programs
Sankaranarayanan, S., Chakarov, A., & Gulwani, S. (2013) · ACM SIGPLAN Notices · doi:10.1145/2499370.2462179 · Cited by 31 · see citing works
An abstract Monte-Carlo method for the analysis of probabilistic programs
Monniaux, D. (2001) · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) · doi:10.1145/360204.360211 · Cited by 28 · see citing works
Backwards Abstract Interpretation of Probabilistic Programs
Monniaux, D. P. (2001) · Lecture notes in computer science · doi:10.1007/3-540-45309-1_24 · Cited by 27 · see citing works
Adaptive Concentration Inequalities for Sequential Decision Problems
Zhao, S., Zhou, E., Sabharwal, A., et al. (2016) · neural information processing systems · Cited by 26 · see citing works
Nabi, R., & Shpitser, I. (2018) · Proceedings of the AAAI Conference on Artificial Intelligence · doi:10.1609/aaai.v32i1.11553 · Cited by 20 · see citing works
Flagged first, then by citations
Research works printed but not linked: 10
- Yuansi Chen, Raaz Dwivedi, Martin J Wainwright, and Bin Yu. 2018. Fast MCMC sampling algorithms on polytopes. The Journal of Machine Learning Research 19, 1 (2018), 2146ś2231.
- Cynthia Dwork, Nicole Immorlica, Adam Tauman Kalai, and Mark DM Leiserson. 2018. Decoupled Classifiers for Group-Fair and Efficient Machine Learning. In Conference on Fairness, Accountability and Transparency. 119ś133.
- Andre Esteva, Brett Kuprel, Roberto A Novoa, Justin Ko, Susan M Swetter, Helen M Blau, and Sebastian Thrun. 2017. Dermatologist-level classification of skin cancer with deep neural networks. Nature 542, 7639 (2017), 115.
- Antonio Filieri, Corina S Păsăreanu, and Willem Visser. 2013. Reliability analysis in symbolic pathfinder. In Proceedings of the 2013 International Conference on Software Engineering. IEEE Press, 622ś631.
- Ian J Goodfellow, Jonathon Shlens, and Christian Szegedy. 2014. Explaining and harnessing adversarial examples. In ICLR.
- Thomas Herault, Richard Lassaigne, and Sylvain Peyronnet. 2006. APMC 3.0: Approximate verification of discrete and continuous time Markov chains. In Quantitative Evaluation of Systems, 2006. QEST 2006. Third International Conference on. IEEE, 129ś130.
- Vincent Tjeng and Russ Tedrake. 2017. Verifying Neural Networks with Mixed Integer Programming. arXiv preprint arXiv:1711.07356 (2017). · arXiv
- Min Wen, Osbert Bastani, and Ufuk Topcu. 2019. Fairness with Dynamics. arXiv preprint arXiv:1901.08568 (2019). · arXiv
- Håkan LS Younes, David J Musliner, et al. 2002. Probabilistic plan verification through acceptance sampling. In Proceedings of the AIPS-02 Workshop on Planning via Model Checking. Citeseer, 81ś88.
- Hakan Lorens Samir Younes. 2004. Verification and Planning for Stochastic Processes with Asynchronous Events. Ph.D. Dissertation. Pittsburgh, PA, USA.
Cited by
Sorted by citations
Fairness in machine learning: A survey
Caton, S., & Haas, C. (2024) · ACM Computing Surveys · doi:10.1145/3616865 · Cited by 646 · see citing works
Fairness in Machine Learning: A Survey
Caton, S., & Haas, C. (2020) · arXiv · doi:10.48550/arxiv.2010.04053 · Cited by 646 · see citing works
A Review on Human–Machine Trust Evaluation: Human-Centric and Machine-Centric Perspectives
Gebru, B., Zeleke, L., Blankson, D., Nabil, M., Nateghi, S., Homaifar, A., & Tunstel, E. (2022) · IEEE Transactions on Human-Machine Systems · doi:10.1109/thms.2022.3144956 · Cited by 101 · see citing works
- Authors
- Bastani, O., Zhang, X., & Solar-Lezama, A.
- Affiliations
- University of Pennsylvania (US)
- Massachusetts Institute of Technology (US)
- Venue
- Proceedings of the ACM on Programming Languages
- Published
- 2019-10-10
- Volume
- 3
- Issue
- OOPSLA
- Pages
- 1-27
- ISSN
- 2475-1421 (ISSN-L)
- OpenAlex
- W2980222512
- Cited by
- 57
- References
- 57
- Citations by year
- 2026: 3 · 2025: 6 · 2024: 4 · 2023: 17 · 2022: 11 · 2021: 9 · 2020: 7
- FWCI
- 4.59
- Type
- journal article
- Language
- en
- Open access
- diamond
- doi.org
- Licence
- Locations
- Proceedings of the ACM on Programming Languages (publishedVersion, cc-by)
- Funders
- Office of Naval Research (N00014-17-1-2699)
- Topics
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
- Social Sciences › Safety Research › Ethics and Social Impacts of AI
- Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
- Keywords
- algorithmic fairness, probabilistic verification, concentration inequalities, adaptive sampling, deep recurrent neural networks, discrimination against minorities, probabilistic guarantees
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
