research-article

Open access

FairSquare: probabilistic verification of program fairness

Authors:

Aws Albarghouthi,

Loris D'Antoni,

Aditya V. NoriAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 1, Issue OOPSLA

Article No.: 80, Pages 1 - 30

https://doi.org/10.1145/3133904

Published: 12 October 2017 Publication History

Abstract

With the range and sensitivity of algorithmic decisions expanding at a break-neck speed, it is imperative that we aggressively investigate fairness and bias in decision-making programs. First, we show that a number of recently proposed formal definitions of fairness can be encoded as probabilistic program properties. Second, with the goal of enabling rigorous reasoning about fairness, we design a novel technique for verifying probabilistic properties that admits a wide class of decision-making programs. Third, we present FairSquare, the first verification tool for automatically certifying that a program meets a given fairness property. We evaluate FairSquare on a range of decision-making programs. Our evaluation demonstrates FairSquare’s ability to verify fairness for a range of different programs, which we show are out-of-reach for state-of-the-art program analysis techniques.

References

[1]

Ifeoma Ajunwa, Sorelle Friedler, Carlos E Scheidegger, and Suresh Venkatasubramanian. 2016. Hiring by algorithm: predicting and preventing disparate impact. Available at SSRN 2746078 (2016).

[2]

Aws Albarghouthi, Loris D’Antoni, and Samuel Drews. 2017. Repairing Decision-Making Programs Under Uncertainty. Springer, Cham, 181–200.

[3]

Julia Angwin, Jeff Larson, Surya Mattu, and Lauren Kirchner. 2016. Machine Bias: There’s Software Used Across the Country to Predict Future Criminals. And it’s Biased Against Blacks. https://www.propublica.org/article/ machine- bias- risk- assessments- in- criminal- sentencing . (May 2016). (Accessed on 06/18/2016).

[4]

Eugene Asarin, Olivier Bournez, Thao Dang, and Oded Maler. 2000. Approximate reachability analysis of piecewise-linear dynamical systems. In International Workshop on Hybrid Systems: Computation and Control. Springer, 20–31.

[5]

Mike Barnett and K Rustan M Leino. 2005. Weakest-precondition of unstructured programs. In ACM SIGSOFT Software Engineering Notes, Vol. 31. ACM, 82–87.

Digital Library

[6]

Solon Barocas and Andrew D Selbst. 2014. Big data’s disparate impact. Available at SSRN 2477899 (2014).

[7]

Gilles Barthe, Pedro R. D’Argenio, and Tamara Rezk. 2004. Secure Information Flow by Self-Composition. In CSFW.

[8]

Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, and Pierre-Yves Strub. 2014. Proving Differential Privacy in Hoare Logic. In IEEE 27th Computer Security Foundations Symposium, CSF 2014, Vienna, Austria, 19-22 July, 2014. 411–424.

Digital Library

[9]

Osbert Bastani, Yani Ioannou, Leonidas Lampropoulos, Dimitrios Vytiniotis, Aditya Nori, and Antonio Criminisi. 2016. Measuring Neural Net Robustness with Constraints. CoRR abs/1605.07262 (2016). http://arxiv.org/abs/1605.07262

[10]

Saugata Basu, Richard Pollack, and Marie-Françoise Roy. 2006. Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics). Springer-Verlag New York, Inc., Secaucus, NJ, USA.

Digital Library

[11]

Vaishak Belle, Guy Van den Broeck, and Andrea Passerini. 2016. Component Caching in Hybrid Domains with Piecewise Polynomial Densities. In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, February 12-17, 2016, Phoenix, Arizona, USA. 3369–3375. http://www.aaai.org/ocs/index.php/AAAI/AAAI16/paper/view/12542

Digital Library

[12]

Vaishak Belle, Andrea Passerini, and Guy Van den Broeck. 2015a. Probabilistic Inference in Hybrid Domains by Weighted Model Integration. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015. 2770–2776. http://ijcai.org/Abstract/15/392

[13]

Vaishak Belle, Guy Van den Broeck, and Andrea Passerini. 2015b. Hashing-based approximate probabilistic inference in hybrid domains. In Proceedings of the 31st Conference on Uncertainty in Artificial Intelligence (UAI).

[14]

Nate Berg. 2014. Predicting crime, LAPD-style. https://www.theguardian.com/cities/2014/jun/25/ predicting- crime- lapd- los- angeles- police- data- analysis- algorithm- minority- report . (June 2014). (Accessed on 06/18/2016).

[15]

Christopher M Bishop. 2006. Pattern recognition. Machine Learning 128 (2006).

[16]

Olivier Bournez, Oded Maler, and Amir Pnueli. 1999. Orthogonal Polyhedra: Representation and Computation. Springer Berlin Heidelberg, Berlin, Heidelberg, 46–60.

[17]

Christopher W. Brown. 2003. QEPCAD B: A Program for Computing with Semi-algebraic Sets Using CADs. SIGSAM Bull. 37, 4 (Dec. 2003), 97–108.

Digital Library

[18]

Toon Calders and Sicco Verwer. 2010. Three naive Bayes approaches for discrimination-free classification. Data Mining and Knowledge Discovery 21, 2 (2010), 277–292.

Digital Library

[19]

Michael Carbin, Sasa Misailovic, and Martin C. Rinard. 2013. Verifying quantitative reliability for programs that execute on unreliable hardware. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013, Indianapolis, IN, USA, October 26-31, 2013. 33–52.

Digital Library

[20]

Swarat Chaudhuri, Martin Clochard, and Armando Solar-Lezama. 2014. Bridging boolean and quantitative synthesis using smoothed proof search. In POPL, Vol. 49. ACM, 207–220.

Digital Library

[21]

Swarat Chaudhuri, Sumit Gulwani, Roberto Lublinerman, and Sara Navidpour. 2011. Proving Programs Robust. In Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering (ESEC/FSE ’11). ACM, New York, NY, USA, 102–112.

Digital Library

[22]

Siddhartha Chib and Edward Greenberg. 1995. Understanding the metropolis-hastings algorithm. The american statistician 49, 4 (1995), 327–335.

[23]

Dmitry Chistikov, Rayna Dimitrova, and Rupak Majumdar. 2015. Approximate Counting in SMT and Value Estimation for Probabilistic Programs. In Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 320–334.

Digital Library

[24]

Guillaume Claret, Sriram K Rajamani, Aditya V Nori, Andrew D Gordon, and Johannes Borgström. 2013. Bayesian inference using data flow analysis. In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering. ACM, 92–102.

Digital Library

[25]

Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004. A tool for checking ANSI-C programs. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 168–176.

[26]

Ron Cytron, Jeanne Ferrante, Barry K Rosen, Mark N Wegman, and F Kenneth Zadeck. 1991. Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems (TOPLAS) 13, 4 (1991), 451–490.

Digital Library

[27]

Anupam Datta, Shayak Sen, and Yair Zick. 2016. Algorithmic Transparency via Quantitative Input Influence. In Proceedings of 37th IEEE Symposium on Security and Privacy.

[28]

Amit Datta, Michael Carl Tschantz, and Anupam Datta. 2015. Automated experiments on Ad privacy settings. Proceedings on Privacy Enhancing Technologies 2015, 1 (2015), 92–112.

[29]

JA De Loera, Brandon Dutra, Matthias Koeppe, Stanislav Moreinis, Gregory Pinto, and Jianqiu Wu. 2012. Software for exact integration of polynomials over polyhedra. ACM Communications in Computer Algebra 45, 3/4 (2012), 169–172.

Digital Library

[30]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337–340.

[31]

Cynthia Dwork. 2006. Differential privacy. In Automata, languages and programming. Springer, 1–12.

Digital Library

[32]

Cynthia Dwork, Moritz Hardt, Toniann Pitassi, Omer Reingold, and Richard S. Zemel. 2012. Fairness through awareness. In Innovations in Theoretical Computer Science 2012, Cambridge, MA, USA, January 8-10, 2012. 214–226.

Digital Library

[33]

Martin Dyer, Alan Frieze, and Ravi Kannan. 1991. A random polynomial-time algorithm for approximating the volume of convex bodies. Journal of the ACM ( JACM) 38, 1 (1991), 1–17.

Digital Library

[34]

Martin E. Dyer and Alan M. Frieze. 1988. On the complexity of computing the volume of a polyhedron. SIAM J. Comput. 17, 5 (1988), 967–974.

Digital Library

[35]

EEOC. 2014. Code of Federal Regulations. https://www.gpo.gov/fdsys/pkg/CFR- 2014- title29- vol4/xml/ CFR- 2014- title29- vol4- part1607.xml . (July 2014). (Accessed on 06/18/2016).

[36]

Virginia Eubanks. 2015. The dangers of letting algorithms enforce policy. http://www.slate.com/articles/technology/ future_tense/2015/04/the_dangers_of _letting_algorithms_enforce_policy.html . (April 2015). (Accessed on 06/18/2016).

[37]

Michael Feldman, Sorelle A. Friedler, John Moeller, Carlos Scheidegger, and Suresh Venkatasubramanian. 2015. Certifying and Removing Disparate Impact. In Proceedings of the 21th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, Sydney, NSW, Australia, August 10-13, 2015. 259–268.

Digital Library

[38]

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.

Digital Library

[39]

Sorelle A. Friedler, Carlos Scheidegger, and Suresh Venkatasubramanian. 2016. On the (im)possibility of fairness. CoRR abs/1609.07236 (2016). http://arxiv.org/abs/1609.07236

[40]

Timon Gehr, Sasa Misailovic, and Martin Vechev. 2016. PSI: Exact Symbolic Inference for Probabilistic Programs. In Computer aided verification. Springer.

[41]

Jaco Geldenhuys, Matthew B Dwyer, and Willem Visser. 2012. Probabilistic symbolic execution. In Proceedings of the 2012 International Symposium on Software Testing and Analysis. ACM, 166–176.

Digital Library

[42]

Noah D. Goodman, Vikash K. Mansinghka, Daniel M. Roy, Keith Bonawitz, and Joshua B. Tenenbaum. 2008. Church: a language for generative models. In UAI 2008, Proceedings of the 24th Conference in Uncertainty in Artificial Intelligence, Helsinki, Finland, July 9-12, 2008. 220–229.

Digital Library

[43]

Andrew D Gordon, Thomas A Henzinger, Aditya V Nori, and Sriram K Rajamani. 2014. Probabilistic programming. In Proceedings of the on Future of Software Engineering. ACM, 167–181.

Digital Library

[44]

Mark Hall, Eibe Frank, Geoffrey Holmes, Bernhard Pfahringer, Peter Reutemann, and Ian H Witten. 2009. The WEKA data mining software: an update. ACM SIGKDD explorations newsletter 11, 1 (2009), 10–18.

Digital Library

[45]

Moritz Hardt, Eric Price, and Nathan Srebro. 2016. Equality of Opportunity in Supervised Learning. CoRR abs/1610.02413 (2016). http://arxiv.org/abs/1610.02413

[46]

Dejan Jovanović and Leonardo de Moura. 2013. Solving Non-linear Arithmetic. ACM Commun. Comput. Algebra 46, 3/4 (Jan. 2013), 104–105.

Digital Library

[47]

Leonid Khachiyan. 1993. Complexity of polytope volume computation. Springer.

[48]

Jon Kleinberg, Sendhil Mullainathan, and Manish Raghavan. 2017. Inherent Trade-Offs in the Fair Determination of Risk Scores. In ITCS.

[49]

Nicole Kobie. 2016. Who do you blame when an algorithm gets you fired? http://www.wired.co.uk/article/ make- algorithms- accountable . ( January 2016). (Accessed on 06/18/2016).

[50]

Daphne Koller and Nir Friedman. 2009. Probabilistic graphical models: principles and techniques. MIT press.

Digital Library

[51]

Dexter Kozen. 1981. Semantics of probabilistic programs. J. Comput. System Sci. 22, 3 (1981), 328–350.

[52]

Yi Li, Tian Huat Tan, and Marsha Chechik. 2014. Management of time requirements in component-based systems. In FM 2014: Formal Methods. Springer, 399–415.

Digital Library

[53]

Piotr Mardziel, Stephen Magill, Michael Hicks, and Mudhakar Srivatsa. 2011. Dynamic enforcement of knowledge-based security policies. In Computer Security Foundations Symposium (CSF), 2011 IEEE 24th. IEEE, 114–128.

Digital Library

[54]

Claire Cain Miller. 2015. Can an Algorithm Hire Better Than a Human? http://www.nytimes.com/2015/06/26/upshot/ can- an- algorithm- hire- better- than- a- human.html . (June 2015). (Accessed on 06/18/2016).

[55]

David Monniaux. 2000. Abstract interpretation of probabilistic semantics. In Static Analysis. Springer, 322–339.

[56]

David Monniaux. 2001a. An abstract Monte-Carlo method for the analysis of probabilistic programs. In ACM SIGPLAN Notices, Vol. 36. ACM, 93–101.

Digital Library

[57]

David Monniaux. 2001b. Backwards abstract interpretation of probabilistic programs. In Programming Languages and Systems. Springer, 367–382.

[58]

Vinod Nair and Geoffrey E Hinton. 2010. Rectified linear units improve restricted boltzmann machines. In Proceedings of the 27th International Conference on Machine Learning (ICML-10). 807–814.

Digital Library

[59]

Dino Pedreshi, Salvatore Ruggieri, and Franco Turini. 2008. Discrimination-aware data mining. In Proceedings of the 14th ACM SIGKDD international conference on Knowledge discovery and data mining. ACM, 560–568.

Digital Library

[60]

Walt L Perry. 2013. Predictive policing: The role of crime forecasting in law enforcement operations. Rand Corporation.

[61]

John Rawls. 2009. A theory of justice. Harvard university press.

[62]

Salvatore Ruggieri. 2014. Using t-closeness anonymity to control for non-discrimination. Transactions on Data Privacy 7, 2 (2014), 99–129.

[63]

Adrian Sampson, Pavel Panchekha, Todd Mytkowicz, Kathryn S McKinley, Dan Grossman, and Luis Ceze. 2014. Expressing and verifying probabilistic assertions. In ACM SIGPLAN Notices, Vol. 49. ACM, 112–122.

Digital Library

[64]

Sriram Sankaranarayanan, Aleksandar Chakarov, and Sumit Gulwani. 2013. Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013. 447–458.

Digital Library

[65]

Latanya Sweeney. 2013. Discrimination in online ad delivery. Queue 11, 3 (2013), 10.

Digital Library

[66]

Andrew Tutt. 2016. An FDA for Algorithms. Available at SSRN 2747994 (2016).

[67]

Jennifer Valentino-Devries, Jeremy Singer-Vine, and Ashkan Soltani. 2012. Websites Vary Prices, Deals Based on Users’ Information. http://www.wsj.com/articles/SB10001424127887323777204578189391813881534 . (December 2012). (Accessed on 06/18/2016).

[68]

Santosh Vempala. 2005. Geometric random walks: a survey. Combinatorial and computational geometry 52, 573-612 (2005), 2.

[69]

WH. 2014. Big Data: Seizing Opportunities, Preserving Values. https://www.whitehouse.gov/sites/default/files/docs/ big_data_privacy_report_may_1_2014.pdf . (May 2014). (Accessed on 06/18/2016).

[70]

WH. 2016. Preparing for the Future of Artificial Intelligence. https://www.whitehouse.gov/sites/default/files/whitehouse_ files/microsites/ostp/NSTC/preparing_for_the_future_of _ai.pdf . (Octorber 2016). (Accessed on 10/15/2016).

[71]

Tal Zarsky. 2014. Understanding discrimination in the scored society. Washington Law Review 89, 4 (2014).

[72]

Richard S. Zemel, Yu Wu, Kevin Swersky, Toniann Pitassi, and Cynthia Dwork. 2013. Learning Fair Representations. In Proceedings of the 30th International Conference on Machine Learning, ICML 2013, Atlanta, GA, USA, 16-21 June 2013. 325–333. http://jmlr.org/proceedings/papers/v28/zemel13.html

Digital Library

Cited By

D’Asaro FGenco FPrimiero G(2025)Checking trustworthiness of probabilistic computations in a typed natural deduction systemJournal of Logic and Computation10.1093/logcom/exaf003Online publication date: 23-Jan-2025
https://doi.org/10.1093/logcom/exaf003
Yadav CChowdhury ABoneh DChaudhuri KSalakhutdinov RKolter ZHeller KWeller AOliver NScarlett JBerkenkamp F(2024)FairProofProceedings of the 41st International Conference on Machine Learning10.5555/3692070.3694365(55682-55705)Online publication date: 21-Jul-2024
https://dl.acm.org/doi/10.5555/3692070.3694365
Skalka CNear J(2024)Language-Based Security for Low-Level MPCProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678246(1-14)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678246
Show More Cited By

Index Terms

FairSquare: probabilistic verification of program fairness
1. Mathematics of computing
  1. Probability and statistics
    1. Probabilistic inference problems
2. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Automated static analysis

Recommendations

PMAF: an algebraic framework for static analysis of probabilistic programs
PLDI '18

Automatically establishing that a probabilistic program satisfies some property ϕ is a challenging problem. While a sampling-based approach—which involves running the program repeatedly—can suggest that ϕ holds, to establish that the program satisfies ϕ,...
PMAF: an algebraic framework for static analysis of probabilistic programs
PLDI 2018: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation

Automatically establishing that a probabilistic program satisfies some property ϕ is a challenging problem. While a sampling-based approach—which involves running the program repeatedly—can suggest that ϕ holds, to establish that the program satisfies ϕ,...
Expressing and verifying probabilistic assertions
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation

Traditional assertions express correctness properties that must hold on every program execution. However, many applications have probabilistic outcomes and consequently their correctness properties are also probabilistic (e.g., they identify faces in ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 1, Issue OOPSLA

October 2017

1786 pages

EISSN:2475-1421

DOI:10.1145/3152284

Issue’s Table of Contents

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 October 2017

Published in PACMPL Volume 1, Issue OOPSLA

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

NSF

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

60
Total Citations
View Citations
1,887
Total Downloads

Downloads (Last 12 months)405
Downloads (Last 6 weeks)39

Reflects downloads up to 02 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

D’Asaro FGenco FPrimiero G(2025)Checking trustworthiness of probabilistic computations in a typed natural deduction systemJournal of Logic and Computation10.1093/logcom/exaf003Online publication date: 23-Jan-2025
https://doi.org/10.1093/logcom/exaf003
Yadav CChowdhury ABoneh DChaudhuri KSalakhutdinov RKolter ZHeller KWeller AOliver NScarlett JBerkenkamp F(2024)FairProofProceedings of the 41st International Conference on Machine Learning10.5555/3692070.3694365(55682-55705)Online publication date: 21-Jul-2024
https://dl.acm.org/doi/10.5555/3692070.3694365
Skalka CNear J(2024)Language-Based Security for Low-Level MPCProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678246(1-14)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678246
Tumlin AManzanas Lopez DRobinette PZhao YDerr TJohnson T(2024)FairNNV: The Neural Network Verification Tool For Certifying FairnessProceedings of the 5th ACM International Conference on AI in Finance10.1145/3677052.3698677(36-44)Online publication date: 14-Nov-2024
https://dl.acm.org/doi/10.1145/3677052.3698677
Liu JQu WGaboardi MGarg DUllman J(2024)Program Analysis for Adaptive Data AnalysisProceedings of the ACM on Programming Languages10.1145/36564148:PLDI(914-938)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656414
Garg PHoltzen SVan den Broeck GMillstein T(2024)Bit Blasting Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36564128:PLDI(865-888)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656412
Huot MGhavami MLew ASchaechtle UFreer CShelby ZRinard MSaad FMansinghka V(2024)GenSQL: A Probabilistic Programming System for Querying Generative Models of Database TablesProceedings of the ACM on Programming Languages10.1145/36564098:PLDI(790-815)Online publication date: 20-Jun-2024
https://doi.org/10.1145/3656409
Chen ZZhang JHort MHarman MSarro F(2024)Fairness Testing: A Comprehensive Survey and Analysis of TrendsACM Transactions on Software Engineering and Methodology10.1145/365215533:5(1-59)Online publication date: 11-Mar-2024
https://dl.acm.org/doi/10.1145/3652155
Randone FBortolussi LIncerto ETribastone M(2024)Inference of Probabilistic Programs with Moment-Matching Gaussian MixturesProceedings of the ACM on Programming Languages10.1145/36329058:POPL(1882-1912)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632905
Caton SHaas C(2024)Fairness in Machine Learning: A SurveyACM Computing Surveys10.1145/361686556:7(1-38)Online publication date: 9-Apr-2024
https://dl.acm.org/doi/10.1145/3616865
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents