Konstantin Kueffner

Konstantin Kueffner

I am a PhD student at IST Austria, working under the supervision of Thomas A. Henzinger.

Publications

You can also find my articles on my Google Scholar profile.

Journal Articles

Fairness Shields: Safeguarding against Biased Decision Makers

Published in 9th International Conference on Formal Structures for Computation and Deduction, 2025

As AI-based decision-makers increasingly influence human lives, it is a growing concern that their decisions are often unfair or biased with respect to people’s sensitive attributes, such as gender and race. Most existing bias prevention mea- sures provide probabilistic fairness guarantees in the long run, and it is possible that the decisions are biased on specific in- stances of short decision sequences. We introduce fairness shielding, where a symbolic decision-maker—the fairness shield—continuously monitors the sequence of decisions of another deployed black-box decision-maker, and makes inter- ventions so that a given fairness criterion is met while the total intervention costs are minimized. We present four different algorithms for computing fairness shields, among which one guarantees fairness over fixed horizons, and three guarantee fairness periodically after fixed intervals. Given a distribution over future decisions and their intervention costs, our algo- rithms solve different instances of bounded-horizon optimal control problems with different levels of computational costs and optimality guarantees. Our empirical evaluation demon- strates the effectiveness of these shields in ensuring fairness while maintaining cost efficiency across various scenarios.

Download Paper

Abstraction-Based Decision Making for Statistical Properties

Published in 9th International Conference on Formal Structures for Computation and Deduction, 2024

Sequential decision-making in probabilistic environments is a fundamental problem with many applications in AI and economics. In this paper, we present an algorithm for synthesizing sequential decision-making agents that optimize statistical properties such as maximum and average response times. In the general setting of sequential decision-making, the environment is modeled as a random process that generates inputs. The agent responds to each input, aiming to maximize rewards and minimize costs within a specified time horizon. The corresponding synthesis problem is known to be PSPACE-hard. We consider the special case where the input distribution, reward, and cost depend on input-output statistics specified by counter automata. For such problems, this paper presents the first PTIME synthesis algorithms. We introduce the notion of statistical abstraction, which clusters statistically indistinguishable input-output sequences into equivalence classes. This abstraction allows for a dynamic programming algorithm whose complexity grows polynomially with the considered horizon, making the statistical case exponentially more efficient than the general case. We evaluate our algorithm on three different application scenarios of a client-server protocol, where multiple clients compete via bidding to gain access to the service offered by the server. The synthesized policies optimize profit while guaranteeing that none of the server’s clients is disproportionately starved of the service.

Download Paper

Monitoring Algorithmic Fairness under Partial Observations

Published in International Conference on Runtime Verification, 2023

Neural-network classifiers achieve high accuracy when predicting the class of an input that they were trained to identify. Maintaining this accuracy in dynamic environments, where inputs frequently fall outside the fixed set of initially known classes, remains a challenge. We consider the problem of monitoring the classification decisions of neural networks in the presence of novel classes. For this purpose, we generalize our recently proposed abstraction-based monitor from binary output to real-valued quantitative output. This quantitative output enables new applications, two of which we investigate in the paper. As our first application, we introduce an algorithmic framework for active monitoring of a neural network, which allows us to learn new classes dynamically and yet maintain high monitoring performance. As our second application, we present an offline procedure to retrain the neural network to improve the monitor’s detection performance without deteriorating the network’s classification accuracy. Our experimental evaluation demonstrates both the benefits of our active monitoring framework in dynamic scenarios and the effectiveness of the retraining procedure.

Download Paper

Monitoring Algorithmic Fairness

Published in International Conference on Runtime Verification, 2023

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 run- time verification of algorithmic fairness for systems whose models are unknown, but are assumed to have a Markov chain structure. We intro- duce 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. Our monitors are of two types, and use, respectively, frequentist and Bayesian statistical inference techniques. While the frequentist monitors compute estimates that are objectively correct with respect to the ground truth, the Bayesian mon- itors compute estimates that are correct subject to a given prior belief about the system’s model. 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 stu- dents while maintaining a reasonable financial burden on the society. Although they exhibit different theoretical complexities in certain cases, in our experiments, both frequentist and Bayesian monitors took less than a millisecond to update their verdicts after each observation.

Download Paper

Into the unknown: active monitoring of neural networks (extended version)

Published in International Journal on Software Tools for Technology Transfer, 2023

Neural-network classifiers achieve high accuracy when predicting the class of an input that they were trained to identify. Maintaining this accuracy in dynamic environments, where inputs frequently fall outside the fixed set of initially known classes, remains a challenge. We consider the problem of monitoring the classification decisions of neural networks in the presence of novel classes. For this purpose, we generalize our recently proposed abstraction-based monitor from binary output to real-valued quantitative output. This quantitative output enables new applications, two of which we investigate in the paper. As our first application, we introduce an algorithmic framework for active monitoring of a neural network, which allows us to learn new classes dynamically and yet maintain high monitoring performance. As our second application, we present an offline procedure to retrain the neural network to improve the monitor’s detection performance without deteriorating the network’s classification accuracy. Our experimental evaluation demonstrates both the benefits of our active monitoring framework in dynamic scenarios and the effectiveness of the retraining procedure.

Download Paper

Runtime Monitoring of Dynamic Fairness Properties

Published in Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency, 2023

A machine-learned system that is fair in static decision-making tasks may have biased societal impacts in the long-run. This may happen when the system interacts with humans and feedback pat- terns emerge, reinforcing old biases in the system and creating new biases. While existing works try to identify and mitigate long- run biases through smart system design, we introduce techniques for monitoring fairness in real time. Our goal is to build and de- ploy a monitor that will continuously observe a long sequence of events generated by the system in the wild, and will output, with each event, a verdict on how fair the system is at the current point in time. The advantages of monitoring are two-fold. Firstly, fair- ness is evaluated at run-time, which is important because unfair behaviors may not be eliminated a priori, at design-time, due to partial knowledge about the system and the environment, as well as uncertainties and dynamic changes in the system and the envi- ronment, such as the unpredictability of human behavior. Secondly, monitors are by design oblivious to how the monitored system is constructed, which makes them suitable to be used as trusted third-party fairness watchdogs. They function as computationally lightweight statistical estimators, and their correctness proofs rely on the rigorous analysis of the stochastic process that models the assumptions about the underlying dynamics of the system. We show, both in theory and experiments, how monitors can warn us (1) if a bank’s credit policy over time has created an unfair distri- bution of credit scores among the population, and (2) if a resource allocator’s allocation policy over time has made unfair allocations. Our experiments demonstrate that the monitors introduce very low overhead. We believe that runtime monitoring is an important and mathematically rigorous new addition to the fairness toolbox.

Download Paper

Toward a generalized notion of discrete time for modeling temporal networks

Published in Network Science Volume 9 Issue 4, 2021

Many real-world networks, including social networks and computer networks for example, are temporal networks. This means that the vertices and edges change over time. However, most approaches for mod- eling and analyzing temporal networks do not explicitly discuss the underlying notion of time. In this paper, we therefore introduce a generalized notion of discrete time for modeling temporal networks. Our approach also allows for considering nondeterministic time and incomplete data, two issues that are often found when analyzing datasets extracted from online social networks, for example. In order to demonstrate the consequences of our generalized notion of time, we also discuss the implications for the computation of (shortest) temporal paths in temporal networks. In addition, we implemented an R-package that pro- vides programming support for all concepts discussed in this paper. The R-package is publicly available for download.

Download Paper

A comprehensive Survey of the Actual Causality Literature

Published in Master Thesis, 2021

The study of causality has recently gained traction in computer science. Formally capturing causal reasoning would allow computers to answer “Why”-questions and would result in significant advances in fields such as verification, machine learning, explainability, legal reasoning and algorithmic fairness. To accomplish this, one needs to be able to infer type causal relationships, i.e. general statements about causal dependencies, from data and then use those relationships to identify the actual causes of an event in a given situation; such causes are referred to as token causes. To the best of our knowledge, there does not exist a comprehensive survey, reviewing the state of the art of formal systems for token causality. The present thesis addresses this deficit. The literature review that we have performed operates on three different levels of granularity. The first considered the literature landscape itself as an object of study, employing network analysis techniques to identify important publications, authors and research communities. The second is a classical literature review, where a subset of the collected literature is investigated in detail, to extract, describe and categorise the tools used for formalising causation. This includes the languages for encoding causal relationships, the various definitions that try to capture token causality, as well as the benchmark used to test the capabilities of those definitions. In the third part we describe and compare the four main token causality definitions, w.r.t. the most prominent benchmarks in the literature. This last part also required some original work, as not all the examples are found in the literature.

Download Paper