Paper deep dive
Counting Worlds Branching Time Semantics for post-hoc Bias Mitigation in generative AI
Alessandro G. Buda, Giuseppe Primiero, Leonardo Ceragioli, Melissa Antonelli
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 95%
Last extracted: 4/26/2026, 11:19:49 PM
Summary
The paper introduces CTLF (Counting Worlds Branching Time Logic), a new formal logic designed for post-hoc bias mitigation in generative AI. Unlike standard temporal logics, CTLF uses a 'counting worlds' semantics to reason about the distribution of outputs in a series. It provides modal operators to verify if a current output series respects a target probability distribution, predict the likelihood of future bias, and determine the necessary number of outputs to remove to restore fairness. The framework is demonstrated using a toy example of biased image generation (gender bias in 'engineer' prompts).
Entities (5)
Relation Signals (3)
CTLF → addresses → Bias Mitigation
confidence 100% · CTLF, a branching-time logic designed to reason about bias in series of generative AI outputs.
Generative AI → exhibits → Bias
confidence 100% · Generative AI systems are known to amplify biases present in their training data.
CTLF → extends → LTLF
confidence 90% · The linear temporal logic LTLF offered in Antonelli et al. (2026)... In the present paper, we present CTLF an alternative counting world CTL-style strategy
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Generative AI systems are known to amplify biases present in their training data. While several inference-time mitigation strategies have been proposed, they remain largely empirical and lack formal guarantees. In this paper we introduce CTLF, a branching-time logic designed to reason about bias in series of generative AI outputs. CTLF adopts a counting worlds semantics where each world represents a possible output at a given step in the generation process and introduces modal operators that allow us to verify whether the current output series respects an intended probability distribution over a protected attribute, to predict the likelihood of remaining within acceptable bounds as new outputs are generated, and to determine how many outputs are needed to remove in order to restore fairness. We illustrate the framework on a toy example of biased image generation, showing how CTLF formulas can express concrete fairness properties at different points in the output series.
Tags
Links
- Source: https://arxiv.org/abs/2604.19431v1
- Canonical: https://arxiv.org/abs/2604.19431v1
Trouble viewing inline? Open PDF directly →
Full Text
40,909 characters extracted from source content.
Expand or collapse full text
Counting Worlds Branching Time Semantics for post-hoc Bias Mitigation in generative AI Alessandro G. Buda, Giuseppe Primiero, Leonardo Ceragioli, Melissa Antonelli alessandro.buda@iusppavia.it giuseppe.primiero@unimi.it leonardo.ceragioli@unimi.it melissa.antonelli@uni-tuebingen.de Abstract Generative AI systems are known to amplify biases present in their training data. While several inference-time mitigation strategies have been proposed, they remain largely empirical and lack formal guarantees. In this paper we introduce CTLF, a branching-time logic designed to reason about bias in series of generative AI outputs. CTLF adopts a counting worlds semantics where each world represents a possible output at a given step in the generation process and introduces modal operators that allow us to verify whether the current output series respects an intended probability distribution over a protected attribute, to predict the likelihood of remaining within acceptable bounds as new outputs are generated, and to determine how many outputs are needed to remove in order to restore fairness. We illustrate the framework on a toy example of biased image generation, showing how CTLF formulas can express concrete fairness properties at different points in the output series. Keywords: Computational Tree Logic, Counting World Semantics, Generative AI, Bias Mitigation. 1 Introduction The presence of bias in Generative AI is a widely recognized phenomenon, stemming primarily from the use of unbalanced training datasets. Furthermore, such original bias reflecting real world disparities is amplified by several factors related to the different components of AI systems, a phenomenon known as bias amplification Seshadri et al. (2023); Buda et al. (2025a). In the case of image generation, one of these factors is the poor representation of certain groups of individuals within the training datasets Hirota et al. (2022). Recent surveys provide comprehensive taxonomies of bias sources, evaluation methodologies, and bias mitigation strategies in LLMs Blodgett and others (2024); Guo et al. (2024); Haque et al. (2025). These works categorize mitigation approaches into data-level, model-level, and post-processing techniques, highlighting the growing importance of inference-time control, as retraining is costly and difficult to scale to larger models. Inference-only and post-hoc mitigation methods aim to reduce bias without retraining foundation models. A number of proposals have been offered in this direction: removing biased activations during inference to mitigate harmful outputs Zhou et al. (2024); token-level filtering mechanisms to enforce fairness constraints during generation Cheng et al. (2025); vector ensemble methods to reduce biased generations at inference time Monteiro Paes and others (2025); Siddique et al. (2025). Simulation-based analyses further evaluate the effectiveness of such inference-time interventions under controlled bias scenarios Kiashemshaki et al. (2025). Guardrail architectures provide an external safety layer around LLMs modularly combining content classification, policy enforcement, and fallback mechanisms to ensure trustworthy deployment Han et al. (2025). Broader reviews discuss layered safety frameworks and architectural constraints designed to intercept unsafe or biased outputs before user delivery Ayyamperumal and Ge (2024); Syed (2025). Empirical studies also examine bias in LLM-based bias detection systems themselves, revealing disparities between model judgments and human perception Lin et al. (2025). From the point of view of formal analysis and verification, it is useful to check whether, given a prompt with an expected distribution of a protected attribute at any point in the output production, is possible to determine bias amplification beyond a given acceptable threshold. When it is already known that the output will become unacceptable, continuing using the model may become useless or harmful. This requires predicting the evolution of the output series as early as possible. Following such verification process, one may want to start a post-hoc bias mitigation process which will work on the current output to remove portions of it in order to bring the distribution back within admissible limits. This requires to reason temporally on series of outputs and their possible extensions. The linear temporal logic LTLF offered in Antonelli et al. (2026) allows to infer frequencies of events on future states of the output. In the present paper, we present CTLF an alternative counting world CTL-style strategy to establish whether at any current state of a series of outputs the expected final series will lay behind the acceptable threshold for unbiased outputs, and if so how to intervene to mitigate the situation as early as possible. 2 A Toy Example Figure 1: Original Training Set, which will inform the Output’s Distribution Consider a dataset D of 2020 images with an unfair gender distribution (e.g., 75% M/25% F), see Figure 1. Leaving aside any amplification, we assume that when D is used to train a model M the output series O=o1,…,onO=\o_1,…,o_n\ on the prompt “Give me a picture of an engineer” repeated n times will reflect the same gender distribution of D. Knowing the current and expected distribution of the output and its cardinality, the objective is to mitigate O at inference stage to obtain an output subset O′⊂O ⊂ O with cardinality as close to n as possible with a desired gender distribution (e.g., 50%M/50%F50\%M/50\%F). Hence, we formulate the following questions: Figure 2: A Subset of the Output at the fourth item in the series. 1. At output m<nm<n, are we still within the intended distribution (e.g. a fair one)? See Figure 2 2. If so, what is the probability to be within the intended distribution at output m′m s.t. m<m′≤nm<m ≤ n? 3 If not, how many outputs do we need to remove to restore it? See Figure 3 Figure 3: A mitigated Output subset. In the following example we will refer to odds for the sake of readability, however it can be easily extended to frequencies and/or probabilities. Consider again Figure 1 as training where the initial odds are 15/5=3/115/5=3/1 in favor of males. Given the results up to o4 (see Figure 2), we are still within the intended (say fair) distribution of the gender property. To establish if the results are still within the intended distribution at o7, one requires calculating the odds of the output being male at all intermediate steps: 1. At o5o_5 they are 13/3>4/113/3>4/1; 2. At o6o_6 they can be 12/3=4/112/3=4/1 if we obtained a male at o5o_5, or 13/2>6/113/2>6/1 if we obtained a female subject; 3. At o7o_7 they can be 11/3<4/111/3<4/1 if we obtained a male subject both at o5o_5 and o6o_6, or 12/2=6/112/2=6/1 if we obtained a male at o5o_5, a female at o6o_6, and vice versa, or 13/113/1 if we obtained a female subject both at o5o_5 and o6o_6. Consider now the case depicted in Figure 3, where twelve outputs have been generated within the same unfair distribution of the training dataset (9/3=3/19/3=3/1 in favor of males). At o5o_5 the result is 3/23/2 in favor of male subjects. Given that we have already reached the maximum number of male subjects within the intended distribution for the set of generated outcomes, we should start mitigating by removing all the following outcomes that will result in male engineers. Our aim is to provide a semantics to reason logically about such distributions, their extensions and required mitigation when the desired output is no longer achieved. 3 The Logic CTLF and its counting semantics The logic LTLF is introduced in Antonelli et al. (2026) to reason about series of probabilistic events. We present an extension CTLF with additional operators and an alternative semantics. In what follows, we will use p1,p2,…p_1,p_2,… for atomic propositions. We assume that such atoms are linguistic representations of our probabilistic events; accordingly, as events are mutually exclusive and collectively exhaustive, the occurrence of an event (i.e. an atom in the language) implies the negation of any other event within the same sample space (i.e. a negation of an atom is equivalent to the disjunction of all other atoms in the same sample space). For example, for p=”male”, ¬p↔q p q=”female”, or ¬p↔q∨r p q r=”female or trans”. ϕ,ψ,γ,…φ,ψ,γ,… denote possibly molecular propositions. We use P to denote the set of propositional variables. Definition 1 (Language of CTLF). Formulas of CTLF are defined by the grammar below: ϕ::=p∣¬ϕ∣ϕ∧ϕ∣ϕ∨ϕ∣□qϕ∣■qϕ∣∘qϕ∣⊳qϕφ::=p φ φ φ φ φ _qφ _qφ _qφ _qφ ψ:=▽qϕ∣†qϕψ:= _qφ _qφ where p∈p∈ P and q∈ℚ[0,1]q _[0,1]. In the following, we rely on standard probability theory terminology. Intuitively, an event denotes an output on a prompt; a series of events denotes a series of outputs of size n; the outcome or value of an event denotes the occurrence of a given (possibly protected) property in an output. A world can be though as the occurrence of an event. ϕφ denotes a state formula. A propositional variable p is meant to denote linguistically the value of a protected attribute of output o of model ℳM, and it can be closed under negation (useful for binary protected attributes), conjunction and disjunction. We call this an event. Given a series of n events, □qϕ _qφ says that at the current state ϕφ has happened at least q×mq× m times, where m≤nm≤ n is the number of outputs so far. The formula ■qϕ _qφ expresses that at the current state ϕφ could have happened (possibly in a different series) at least q×mq× m times, where m≤nm≤ n is the number of outputs so far within a well-defined probability distribution ΦΣ _ . The formula ∘qϕ _qφ expresses that among the possible complete series of outputs, there is one such series in which at some point ϕφ has happened at least q×nq× n times, where n is the total number of outputs happening in that series. ⊳qϕ _qφ expresses that, given a complete series of outputs within a well-defined probability distribution, and a point in that series, the probability that ϕφ happens at the next time in that series is at least q, namely q×(n−m)q×(n-m) times. The formula ψ is a path formula. The formula ▽qϕ _qφ expresses that given a complete series of events ϕφ happens at least q×nq× n times. The formula †qϕ _qφ expresses that starting at a given event of a complete series with outputs in a well-defined probability distribution, the probability that such series is completed with outputs still in that distribution is at least q. Definition 2 (Model of CTLF). Let Σ be a well-defined probability distribution on an event space. We define a model ℳ=(W,W1,Wn,Re,Rf,)M=(W,W^1,W^n,R_e,R_f,V), where • W=w1.1,w1.2,…,w1.l,w2.1,w2.2,…,w2.l×l,…wn.1,…,wn.mW=\w_1.1,w_1.2,…,w_1.l,w_2.1,w_2.2,…,w_2.l× l,… w_n.1,…,w_n.m\ is a finite set of worlds s.t. l is the number of possible outcomes for each event, n is teh number of events for each series and m=lnm=l^n is the number of possible series of events. • W⊃W1=w1.1,w1.2,…,w1.lW⊃ W^1=\w_1.1,w_1.2,…,w_1.l\ is the set of root worlds, denoting the set of possible values for the first event of the series. Its cardinality is l; • W⊃Wn=wn.1,wn.2,…,wn.mW⊃ W^n=\w_n.1,w_n.2,…,w_n.m\ is the set of leaf worlds, i.e., the set of possible outcomes for the last event of the series, with cardinality m; • ReR_e is an anti-symmetric, beginning, reflexive, and transitive (backward) relation, i.e., a childhood relation between different events of the series, such that: – ∀w∈W1,w′Rew⇔w′=w∀ w∈ W^1,w R_ew w =w: root events have no parents; – for each pair wi.x,wj,y∈Ww_i.x,w_j,y∈ W if wi.xRewj.yw_i.xR_ew_j.y then i≥ji≥ j: non-root events are children of previous ones – for each wi.j∈Ww_i.j∈ W with i>1i>1, ∃!wi−1.k:wi.jRewi−1.k∃!w_i-1.k:w_i.jR_ew_i-1.k with k=⌈j/l⌉k= j/l , and, as seen, l is the number of possible outcomes for each event: each non-root event wi.jw_i.j at time i>1i>1 can have only one direct parent world at time i−1i-1, whose secondary index is given by the ceiling function of j/lj/l. Therefore, given a series of n events with l possible outcomes for each event, there exists only one path from each of the possible lnl^n outcomes for the last event through all events in the series to the root world. • RfR_f is an anti-symmetric, beginning, reflexive, and transitive (forward) relation, i.e., a parenthood relation between different events of the series, such that: – ∀w∈Wn,w′Rfw⇔w′=w∀ w∈ W^n,w R_fw w =w: leaf events have no children; – for each pair wi.x,wj,y∈Ww_i.x,w_j,y∈ W, if wi.xRfwj.yw_i.xR_fw_j.y then i≤ji≤ j: previous events are seen as parents of following ones; – for each wi.j∈Ww_i.j∈ W with i<ni<n , there exists a set wi+1.h+1,wi+1.h+2,…,\w_i+1.h+1,w_i+1.h+2,…, wi+1.h+lw_i+1.h+l\ with h=[(j−1)×l]h=[(j-1)× l], and l is the number of possible outcomes for each event, i.e., each non-leaf world wi.jw_i.j representing one possible outcome for the event at time i<ni<n has l direct children at time i+1i+1, with secondary indexes [(j−1)×l]+1,[(j−1)×l]+2,…,[(j−1)×l]+l[(j-1)× l]+1,[(j-1)× l]+2,…,[(j-1)× l]+l. Therefore, given a series of n events, with l possible outcomes for each event, and given a non leaf world wi.jw_i.j, representing the jjth possible outcome for the iith event in the series, there are ln−il^n-i possible path from wi.jw_i.j to the leaf worlds, passing across all the intermediate events. • :W↦()V:W ( P) is a valuation function assigning to each world in W a subset of P holding in such world. We denote with Wi=wi.1,wi.2,…,wi.lW^i=\w_i.1,w_i.2,…,w_i.l\ the set of possible outcomes for the iith event of the series. We now introduce the notion of path. Definition 3 (Path). Given W and Rf⊆W×WR_f W× W, we define a path between events i and j of the series (with i<ji<j) as: π[i.x,j.z]=⟨wi.x,wi+1.y,…,wj.z⟩:wk.v∈W,(wk.v,wk+1.w)∈Rf,∀k∈[i,j−1] _[i.x,j.z]=\ w_i.x,w_i+1.y,…,w_j.z :w_k.v∈ W,(w_k.v,w_k+1.w)∈ R_f,∀ k∈[i,j-1]\ An equivalent definition can be provided using ReR_e instead of RfR_f. A complete path π∗π^* is a path from the first to the last event of the series, including all the intermediate steps: π[x,z]∗=π[1.x,n.z]π^*_[x,z]= _[1.x,n.z] Definition 4 (Set of paths). Given W and Rf⊆W×WR_f W× W, and a world wi.jw_i.j, we define the set of paths originating in wi.jw_i.j as: Π[i.j]=⟨wi.j,…,wn.k⟩, ^[i.j]=\ w_i.j,…,w_n.k , …,…, ⟨wi.j, w_i.j, …,…, wn.m⟩.w_n.m \.\ The set Π∗=⟨w1.1,…,wn.k⟩,…,⟨w1.l,…,wn.m⟩ ^*=\ w_1.1,…,w_n.k ,…, w_1.l,…,w_n.m \ is the set of complete paths. Definition 5 (ΦΣ _ ). Given a probability distribution Σ assigning to any p∈p∈ P the frequency μ(p)μ(p), the function ΦΣ:Π∗↦(Π∗) _ : ^* ( ^*) associates the set of complete paths in W it returns any of its member π[x,z]∗π^*_[x,z] such that |wi.j∈π[x,z]∗:wi.j∈(p)||π[x,z]∗|=μ(p) |\w_i.j∈π^*_[x,z]:w_i.j (p)\||π^*_[x,z]|=μ(p) In other words, every path in the co-domain of ΦΣ _ shows for each p∈p∈ P a set of μ(p)×|π∗|μ(p)×|π^*| worlds in which p is true. We denote with ΠΣ[i.j] ^[i.j]_ the set of paths originating in wi.jw_i.j returned by ΦΣ _ , and with ΠΣ∗ ^*_ the set of complete paths returned by ΦΣ _ . We denote with v:π[i.x,j.z]↦()v: _[i.x,j.z] ( P) any function for the series of events corresponding to path π[i.x,j.z] _[i.x,j.z], identifying one among the possible m=lnm=l^n series of events, or possibly complete paths. Definition 6 (Reachable Worlds). Given a model ℳM, for any world wi.j∈Ww_i.j∈ W we denote: • Rewi.j=w′∈W:wi.jRew′R_e^w_i.j=\w ∈ W:w_i.jR_ew \, the set of all worlds accessible from wi.jw_i.j according to the transitive closure on ReR_e. • Rfwi.j=w′∈W:wi.jRfw′R_f^w_i.j=\w ∈ W:w_i.jR_fw \, the set of all worlds accessible from wi.jw_i.j according to the transitive closure on RfR_f. Definition 7 (Semantics for state and path formulas). For any CTLF-formula ϕφ, a model ℳM, a world w∈Ww∈ W, we define the relation ℳ,w⊨M,w inductively as follows: ℳ,wi.j⊨p⇔wi.j∈(p) ,w_i.j p w_i.j∈ V(p) ℳ,wi.j⊨¬ϕ⇔M,wi.j⊭ϕ ,w_i.j φ M,w_i.j φ ℳ,wi.j⊨ϕ1∧ϕ2⇔M,wi.j⊨ϕ1 and M,wi.j⊨ϕ2 ,w_i.j _1 _2 M,w_i.j _1\ and \ M,w_i.j _2 ℳ,wi.j⊨ϕ1∨ϕ2⇔M,wi.j⊨ϕ1 or M,wi.j⊨ϕ2 ,w_i.j _1 _2 M,w_i.j _1\ or \ M,w_i.j _2 ℳ,wi.j⊨□qϕ⇔|Rewi.j(ϕ)||Rewi.j|≥q. ,w_i.j _qφ |R_e^w_i.j(φ)||R_e^w_i.j|≥ q. ℳ,wi.j⊨■qϕ⇔|Rewi.k(ϕ)||Rewi.k|≥q for some πΣ∗ with wi.k⩽⩾j∈πΣ∗ and wi.k⩽⩾j∈Wi. ,w_i.j _qφ \! |R_e^w_i.k(φ)||R_e^w_i.k|≥ q\ for some π^*_ with \!w_i.k j∈π^*_ and w_i.k j∈ W^i\!. ℳ,wi.j⊨∘qϕ⇔|Rewi.j(ϕ)||π∗|≥q for some π∗. ,w_i.j _qφ |R_e^w_i.j(φ)||π^*|≥ q\ for some π^*. ℳ,wi.j⊨⊳qϕ⇔∣Rfwi+1.k(ϕ)∣Rfwi+1.k∣≥q for some πΣ∗ such that wi.j,wi+1,k∈πΣ∗, ,w_i.j _qφ R_f^w_i+1.k(φ) R_f^w_i+1.k ≥ q\ for some π^*_ such that w_i.j,w_i+1,k∈π^*_ , where Rewi.j(ϕ)=w′∈Rewi.j:ℳ,wi.j⊨ϕR_e^w_i.j(φ)=\w ∈ R_e^w_i.j:M,w_i.j φ\ and Rfwi.j(ϕ)=w′∈Rfwi.j:ℳ,wi.j⊨ϕR_f^w_i.j(φ)=\w ∈ R_f^w_i.j:M,w_i.j φ\ For any CTLF-formula ϕφ, a model ℳM, a (possibly complete) path π[i.x,j.z] _[i.x,j.z], we define the relation ℳ,π[i.x,j.z]⊨M, _[i.x,j.z] inductively as follows: ℳ,π[x,z]∗⊨▽qϕ⇔∣Rfw1.x(ϕ)∣π[x,z]∗∣≥q ,π^*_[x,z] _qφ R_f^w_1.x(φ) π^*_[x,z] ≥ q ℳ,π[i.x,j.z]⊨†qϕ⇔ℳ,π[x,z]∗⊇π[i.x,j.z]⊨▽q′ϕ with π[x,z]∗∈ΠΣ∗ and ∣ΠΣ[j.z]∣Π[j.z]∣≥q. , _[i.x,j.z] _qφ ,π^*_[x,z] _[i.x,j.z] _q φ with π^*_[x,z]∈ ^*_ and ^[j.z]_ ^[j.z] ≥ q. 4 Formalising our Example Example 1. Consider the model in Fig. 4 representing n=6n=6 generations of images on the prompt “Give me a picture of an engineer”, with l=2l=2 possible outcomes (M and F, for the sake of simplicity) for each generation, and m=26=64m=2^6=64 possible series of events. Connections between outcomes represent both the experimental (ReR_e), and the forward-looking (RfR_f) relations. Paths with valuations in ΦΣ _ , i.e., paths in ΠΣ∗ ^*_ , are marked with dashed lines. W=w1.1,w1.2,w2.1,…,w2.4,w3.1,…,w3.8,w4.1,…,w4.16,w5.1,…,w5.32,w6.1,…,w6.64W=\w_1.1,w_1.2,w_2.1,…,w_2.4,w_3.1,…,w_3.8,w_4.1,…,w_4.16,w_5.1,…,w_5.32,w_6.1,…,w_6.64\ Worlds w1.1w_1.1 and w1.2w_1.2 are the root worlds. For each non-root world there exists only one direct parent world belonging to the set of possible outcomes for the previous step in the series (e.g., world w3.5w_3.5 has only one direct parent world, w(3−1).⌈5/2⌉=w2.3w_(3-1). 5/2 =w_2.3), and there is only one complete path for each world connecting this to the corresponding root world (e.g., from w3.5w_3.5 to w2.3w_2.3, and then to w1.2w_1.2). The subset of W w6.1,…,w6.64\w_6.1,…,w_6.64\ is the set of leaf worlds. For each non leaf world there are l=2l=2 direct children worlds, representing the possible outcomes for the next event of the series (e.g. w2.3w_2.3 has two direct children, w2+1.[(3−1)×2]+1=w3.5w_2+1.[(3-1)× 2]+1=w_3.5, and w2+1.[(3−1)×2]+2=w3.6w_2+1.[(3-1)× 2]+2=w_3.6), and there are 26−2=162^6-2=16 possible path from w2.3w_2.3 to the corresponding leafs (from w2.3w_2.3 to w6.33,w6.34,w6.35,…w6.48w_6.33,w_6.34,w_6.35,… w_6.48. MFFMMFFMMFFMMFFMMFFMMFFMMFFMMFFMMMFMFFMMFFMMFFMMFFMMFFMMFFMMFMFMFFMMFFMMFFMMFFMMFFMMFFMMFFMMFFMFMFMFFMMFFMMFFMMFFMMFFMMFFMMFMFw1.1w_1.1w1.2w_1.2w2.1w_2.1w2.2w_2.2w2.4w_2.4w2.1w_2.1w2.3w_2.3w3.2w_3.2w2.1w_2.1w3.1w_3.1w3.4w_3.4w3.3w_3.3w3.7w_3.7w3.6w_3.6w3.5w_3.5w3.8w_3.8w4.3w_4.3w4.2w_4.2w4.1w_4.1w4.4w_4.4w4.5w_4.5w4.6w_4.6w4.7w_4.7w4.8w_4.8w4.9w_4.9w4.10w_4.10w4.11w_4.11w4.12w_4.12w4.13w_4.13w4.14w_4.14w4.15w_4.15w4.16w_4.16w5.1w_5.1w5.2w_5.2w5.3w_5.3w5.4w_5.4w5.5w_5.5w5.6w_5.6w5.7w_5.7w5.8w_5.8w5.16w_5.16w5.15w_5.15w5.14w_5.14w5.13w_5.13w5.12w_5.12w5.11w_5.11w5.10w_5.10w5.9w_5.9w5.17w_5.17w5.18w_5.18w5.19w_5.19w5.20w_5.20w5.21w_5.21w5.22w_5.22w5.23w_5.23w5.24w_5.24w5.25w_5.25w5.26w_5.26w5.27w_5.27w5.28w_5.28w5.29w_5.29w5.30w_5.30w5.31w_5.31w5.32w_5.32w6.1w_6.1w6.2w_6.2w6.3w_6.3w6.4w_6.4w6.5w_6.5w6.6w_6.6w6.7w_6.7w6.8w_6.8w6.10w_6.10w6.11w_6.11w6.12w_6.12w6.13w_6.13w6.14w_6.14w6.15w_6.15w6.16w_6.16w6.9w_6.9w6.17w_6.17w6.18w_6.18w6.19w_6.19w6.20w_6.20w6.21w_6.21w6.22w_6.22w6.23w_6.23w6.24w_6.24w6.26w_6.26w6.27w_6.27w6.28w_6.28w6.29w_6.29w6.30w_6.30w6.31w_6.31w6.32w_6.32w6.25w_6.25w6.33w_6.33w6.34w_6.34w6.35w_6.35w636w_636w6.37w_6.37w6.38w_6.38w6.39w_6.39w6.40w_6.40w6.42w_6.42w6.43w_6.43w6.44w_6.44w6.45w_6.45w6.46w_6.46w6.47w_6.47w6.48w_6.48w6.41w_6.41w6.49w_6.49w6.50w_6.50w6.51w_6.51w6.52w_6.52w6.53w_6.53w6.54w_6.54w6.55w_6.55w6.56w_6.56w6.58w_6.58w6.59w_6.59w6.60w_6.60w6.61w_6.61w6.62w_6.62w6.63w_6.63w6.64w_6.64w6.57w_6.57 Figure 4: A model representing 6 generations of images on the prompt “Give me a picture of an engineer”. Connections represent both the experimental (ReR_e), and the forward-looking (RfR_f) relations. Paths in ΠΣ∗ ^*_ are marked with dashed lines. Example 2. Consider again the model in Figure 4. The following hold: • w1.1⊨Mw_1.1 M because w1.1w_1.1 is in (M) a(M), i.e., M is true in w1.1w_1.1 • w1.1⊨¬Fw_1.1 F because w1.1⊭Fw_1.1 F, i.e., F is false in w1.1w_1.1 • w3.1⊨□1Mw_3.1 _1M because |Rew3.1(M)|/|Rew3.1|=1|R_e^w_3.1(M)|\ /\ |R_e^w_3.1|=1 • w3.2⊨□2/3Mw_3.2 _2/3M because |Rew3.1(M)|/|Rew3.1|=2/3|R_e^w_3.1(M)|\ /\ |R_e^w_3.1|=2/3 • w3.1⊨■1Fw_3.1 _1F and w3.2⊨■1Fw_3.2 _1F because there exists πΣ∗=⟨w1.2,…,w6.57⟩π^*_ =\ w_1.2,…,w_6.57 \ and there exists w3.8w_3.8 belonging to both πΣ∗π^*_ and W3W^3 such that |Rew3.8(F)|/|Rew3.8|=1|R_e^w_3.8(F)|\ /\ |R_e^w_3.8|=1 • w3.1⊨∘3/6M∧∘0/6Fw_3.1 _3/6M _0/6F because there exists π∗π^* , e.g., ⟨w[1.1]…w[6.1]⟩\ w_[1.1]… w_[6.1] \, such that w3.1w_3.1 is in π∗π^*, |Rew3.1(M)|/|π∗|=3/6|R_e^w_3.1(M)|\ /\ |π^*|=3/6, and |Rew3.1(F)|/|π∗|=0|R_e^w_3.1(F)|\ /\ |π^*|=0 • w3.1⊨⊳1Fw_3.1 _1F because there exists πΣ∗=⟨w1.1,…,w6.8⟩π^*_ =\ w_1.1,…,w_6.8 \ such that w3.1,w4.2w_3.1,w_4.2 are in πΣ∗π^*_ and |Rfw4.2(F)|/|Rfw4.2|=1|R_f^w_4.2(F)|\ /\ |R_f^w_4.2|=1 • w3.2⊨⊳2/3Fw_3.2 _2/3F because there exists πΣ∗=⟨w1.1,…,w6.12⟩π^*_ =\ w_1.1,…,w_6.12 \ such that w3.2,w4.3w_3.2,w_4.3 are in πΣ∗π^*_ and |Rfw4.3(F)|/|Rfw4.3|=2/3|R_f^w_4.3(F)|\ /\ |R_f^w_4.3|=2/3 • π[2,63]∗⊨▽1/6Mπ^*_[2,63] _1/6M because starting from the root world w1.2w_1.2 we can reach, by means of RfR_f across the path π[2,63]∗π^*_[2,63], only one world over six in which M holds, formally |Rfw1.2(M)|/|π[2,63]∗|=1/6|R_f^w_1.2(M)|\ /\ |π^*_[2,63]|=1/6 • π[1.1,3.1]⊨†1/8M _[1.1,3.1] _1/8M because π[1.1,3.1] _[1.1,3.1] is one of the paths originating in w1.1w_1.1 returned by ΦΣ _ , and there is only one possible path over eight starting from w3.1w_3.1 returned by ΦΣ _ . Example 3. Consider the results depicted in Figure 2. This situation can be represented in the model in Figure 4 as the path starting from w1.1w_1.1 (thus we can ignore the set of paths Π[1.2] ^[1.2]), passing across w[2.2]w_[2.2] and w[3.4]w_[3.4], and reaching w[4.7]w_[4.7]. This sub-series of event is still within a fair distribution, in fact we are in a path in ΠΣ∗ ^*_ (a dashed path in the figure). Using the defined language: w4.7⊨□1/2M∧□1/2F.w_4.7 _1/2M _1/2F.\ Both M and F have appeared in proportion ≥1/2≥ 1/2 among the ancestors, hence the output is balanced so far. We can further characterise the situation at w4.7w_4.7 in terms of the probability of completing the series within a fair distribution. The path π[1.1,4.7] _[1.1,4.7] is one of the paths originating from w1.1w_1.1 returned by ΦΣ _ , and from w4.7w_4.7 there are ln−i=22=4l^n-i=2^2=4 possible continuations, of which only 2 yield a Σ -compatible completion reaching 3M/3F3M/3F at event 6. Since |ΠΣ[4.7]|/|Π[4.7]|=2/4=1/2| ^[4.7]_ |\,/\,| ^[4.7]|=2/4=1/2, we have: π[1.1,4.7]⊨†1/2M _[1.1,4.7] _1/2M. This means that, given we are currently on a Σ -compatible path, the probability of completing the series within the fair distribution is exactly 1/21/2. Any single deviation at step 5 or 6 eliminates all remaining Σ -compatible completions. The two Σ -compatible completions can be further characterised using the forward-looking operator ⊳ . They are w4.7→w5.13(M)→w6.26(F)w_4.7→ w_5.13(M)→ w_6.26(F) and w4.7→w5.14(F)→w6.27(M)w_4.7→ w_5.14(F)→ w_6.27(M). In both cases |Rfw5,k(ϕ)|/|Rfw5,k|=1/2|R_f^w_5,k(φ)|\,/\,|R_f^w_5,k|=1/2, yielding: w4.7⊨⊳1/2F∧⊳1/2Mw_4.7 _1/2F\; \; _1/2M. Both next outputs preserve a fair completion, but each forces a unique outcome at step 6: the series is balanced but offers no redundancy. Consider now the mitigation scenario depicted in Figure 3, where 12 outputs are generated following the training distribution (9/3=3/19/3=3/1 in favour of males). Since at most 3 female outputs can appear in the full series, the largest achievable balanced subset has cardinality 6, yielding |π∗|=6|π^*|=6 for the fair-subset path. At o5o_5 the ratio is 3/23/2 in favour of males: as |Rew5,j(M)|=3=1/2×|π∗||R_e^w_5,j(M)|=3=1/2×|π^*|, we have: w5,j⊨∘1/2Mw_5,j _1/2M, meaning the male quota for the balanced subset is exhausted. Mitigation is nonetheless possible: there exists a Σ′ -compatible path with target distribution 50%M/50%F50\%M/50\%F passing through w5,jw_5,j such that πΣ′∗⊨∇1/2Fπ^*_ _1/2F, confirming that a 3M/3F3M/3F subset is achievable from our current position. The mitigation strategy consists in removing all subsequent male outputs (marked × in Figure 3), yielding a balanced subset O′⊂O ⊂ O of 6 outputs (π[1.1,6.26] _[1.1,6.26] in Figure 4). 5 Conclusions Our modalities were originally inspired by the counting semantics from Legastelois et al. (2017) and its use for a pragmatic of information Buda and Primiero (2025), by probabilistic interpreted systems Chen et al. (2016), by probability logics Nilsson (1986); Bacchus (1990); Fagin et al. (1990), as well as by the counting operators introduced in counting logics, which were mostly developed in connection with complexity Wagner (1986); Antonelli et al. (2024, 2023) and finite model theory Moskowakis (1957); Kontinen (2009). The strategy of checking againts admissible distributions is at the basis of a proof-theoretic and possible-worlds semantics for trustworthiness evaluation and preservation of non-deterministic computations Kubyshkina and Primiero (2024); D’Asaro et al. (2025); Ceragioli and Primiero (2026) Several directions for future work are worth pursuing. First, the current model treats all transitions within a given probability assignemnt as equally probable. A natural extension would assign explicit weights to the transitions, reflecting prior knowledge about the generation distribution. This would allow a more fine-grained account of the likelihood of individual outputs, and could be integrated into the semantics of the counting operators via a weighted reachability measure, enriching the expressive power of the logic without altering its overall structure. Second, a more significant extension concerns the case in which the reference probability distribution is not fixed in advance, but is refined at runtime as new outputs are observed. Rather than assuming the Markov chain as a known input, one could start from an initial distribution and update the transition probabilities each time a new output is produced: if a ”male” output is generated, the weight on the transition towards output ”female” is slightly increased for the subsequent step, progressively steering the generation towards the intended distribution. This setting is closely related to the study of parametric Markov chains Hutschenreiter et al. (2017), where transition probabilities are expressed as functions of a set of parameters that can be synthesised or updated to satisfy a given specification Jansen et al. (2022), and to recent work on the formal verification of Markov processes with learned parameters Maaz and Chan (2025). The resulting framework would be an adaptive model in which the counting worlds structure is progressively identified from observations. Establishing formal guarantees on the convergence of such updates and on the correctness of the verification and mitigation procedures in this dynamic setting constitutes an open problem of independent interest. Finally, a software implementation of the checking and mitigation procedures described in this paper is under development for the MIRAI Toolbox, which has already been applied to several classification tasks Coraglia et al. (2023); Buda et al. (2024, 2025b). The tool will take as input a stream of generative AI outputs, a target distribution and a fairness threshold, and will return either a certificate of compliance or a mitigation plan specifying which outputs to remove. This will allow the framework to be evaluated on real-world systems, including both text-to-image models and large language models. Acknowledgments This research was supported by the Ministero dell’Università e della Ricerca (MUR) through PRIN 2022 Project SMARTEST – Simulation of Probabilistic Systems for the Age of the Digital Twin (20223E8Y4X), the Project “Departments of Excellence 2023-2027” awarded to the Department of Philosophy “Piero Martinetti” of the University of Milan which provided funding for a research visit in 2025 to the last author. Declaration on Generative AI During the preparation of this work, the authors used DALL-E (OpenAI) for figures 1, 2 and 3 in order to: Generate images. After using these tool(s)/service(s), the author(s) reviewed and edited the content as needed and take(s) full responsibility for the publication’s content. References [1] M. Antonelli, U. Dal Lago, and P. Pistone (2023) On counting propositional logic and Wagner’s hierarchy. Theoretical Computer Science 966-967. Cited by: §5. [2] M. Antonelli, U. Dal Lago, and P. Pistone (2024) Towards logical foundations for probabilistic computation. Annals of Pure and Applied Logic 175 (9). Cited by: §5. [3] M. Antonelli, L. Ceragioli, A. Buda, and G. Primiero (2026) A linear temporal logic of frequencies on series of events. External Links: 2604.10669, Link Cited by: §1, §3. [4] S. G. Ayyamperumal and L. Ge (2024) Current state of LLM risks and AI guardrails. External Links: 2406.12934, Link Cited by: §1. [5] F. Bacchus (1990) Representing and reasoning with probabilistic knowledge a logical approach to probabilities. The MIT Press. Cited by: §5. [6] S. L. Blodgett et al. (2024) Bias and fairness in large language models: a survey. Computational Linguistics. Cited by: §1. [7] A. G. Buda, G. Coraglia, F. A. Genco, C. Manganini, and G. Primiero (2025-012025-01) Bias amplification chains in ml-based systems with an application to credit scoring. CEUR-WS. External Links: Link Cited by: §1. [8] A. G. Buda and G. Primiero (2025) A logic for using information. Logique Et Analyse 265 (n/a), p. 59–103. Cited by: §5. [9] A. G. Buda, G. Coraglia, F. A. Genco, C. Manganini, and G. Primiero (2024) Bias amplification chains in ml-based systems with an application to credit scoring. In Proceedings of the 3rd Workshop on Bias, Ethical AI, Explainability and the role of Logic and Logic Programming co-located with the 23rd International Conference of the Italian Association for Artificial Intelligence (AIxIA 2024), Bolzano, Italy, November 26, 2024, G. Coraglia, F. A. D’Asaro, A. Dyoub, F. A. Lisi, and G. Primiero (Eds.), CEUR Workshop Proceedings, p. 77–86. External Links: Link Cited by: §5. [10] A. G. Buda, G. Coraglia, F. A. Genco, C. Manganini, and G. Primiero (2025) Assessing the risk of discrimination with BRIO: A use case from the financial sector. In Proceedings of the 4th International Conference on Hybrid Human-Artificial Intelligence, HHAI 2025, Pisa, Italy, June 9-13, 2025, D. Pedreschi, M. Milano, I. Tiddi, S. Russell, C. Boldrini, L. Pappalardo, A. Passerini, and S. Wang (Eds.), Frontiers in Artificial Intelligence and Applications, p. 483–485. External Links: Link, Document Cited by: §5. [11] L. Ceragioli and G. Primiero (2026) Trustworthiness preservation by copies of machine learning systems. Int. J. Approx. Reason. 192, p. 109638. External Links: Link, Document Cited by: §5. [12] T. Chen, G. Primiero, F. Raimondi, and N. Rungta (2016) A computationally grounded, weighted doxastic logic. Stud Logica 104 (4), p. 679–703. External Links: Link, Document Cited by: §5. [13] X. Cheng, R. Chen, H. Zan, Y. Jia, and M. Peng (2025) BiasFilter: an inference-time debiasing framework for large language models. arXiv preprint arXiv:2505.23829. Cited by: §1. [14] G. Coraglia, F. A. D’Asaro, F. A. Genco, D. Giannuzzi, D. Posillipo, G. Primiero, and C. Quaggio (2023) BRIOxAlkemy: a bias detecting tool. In Proceedings of the 2nd Workshop on Bias, Ethical AI, Explainability and the role of Logic and Logic Programming co-located with the 22nd International Conference of the Italian Association for Artificial Intelligence (AI*IA 2023), Rome, Italy, November 6, 2023, G. Boella, F. A. D’Asaro, A. Dyoub, L. Gorrieri, F. A. Lisi, C. Manganini, and G. Primiero (Eds.), CEUR Workshop Proceedings, p. 44–60. External Links: Link Cited by: §5. [15] F. A. D’Asaro, F. A. Genco, and G. Primiero (2025) Checking trustworthiness of probabilistic computations in a typed natural deduction system. J. Log. Comput. 35 (6). External Links: Link, Document Cited by: §5. [16] R. Fagin, J.Y. Halpern, and N. Megiddo (1990) A logic for reasoning about probabilities. Information and Computation 87 (1-2), p. 78–128. Cited by: §5. [17] Y. Guo, M. Guo, J. Su, Z. Yang, and M. Zhu (2024) Bias in large language models: origin, evaluation, and mitigation. arXiv preprint arXiv:2411.10915. Cited by: §1. [18] S. Han, S. Avestimehr, and C. He (2025) Bridging the safety gap: a guardrail pipeline for trustworthy llm inferences. External Links: 2502.08142, Link Cited by: §1. [19] F. Haque, D. Xu, and X. Niu (2025) A comprehensive survey on bias and fairness in large language models. In Trends and Applications in Knowledge Discovery and Data Mining, S. Yuan, F. Malliaros, and X. Zheng (Eds.), p. 83–101. External Links: ISBN 978-981-96-8197-6 Cited by: §1. [20] Y. Hirota, Y. Nakashima, and N. Garcia (2022) Quantifying societal bias amplification in image captioning. In 2022 IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR), Vol. , p. 13440–13449. External Links: Document Cited by: §1. [21] L. Hutschenreiter, C. Baier, and J. Klein (2017-09) Parametric markov chains: pctl complexity and fraction-free gaussian elimination. Electronic Proceedings in Theoretical Computer Science 256, p. 16–30. External Links: ISSN 2075-2180, Link, Document Cited by: §5. [22] N. Jansen, S. Junges, and J. Katoen (2022) Parameter synthesis in markov models: a gentle survey. In Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, J. Raskin, K. Chatterjee, L. Doyen, and R. Majumdar (Eds.), p. 407–437. External Links: ISBN 978-3-031-22337-2, Document, Link Cited by: §5. [23] K. Kiashemshaki, M. J. Torkamani, N. Mahmoudi, and M. S. Bilehsavar (2025) Simulating a bias mitigation scenario in large language models. External Links: 2509.14438, Link Cited by: §1. [24] J. Kontinen (2009) A logical characterization of the counting hierarchy. ACM Trans. Comput. Log. 10 (1), p. 7:1–7:21. External Links: Link, Document Cited by: §5. [25] E. Kubyshkina and G. Primiero (2024) A possible worlds semantics for trustworthy non-deterministic computations. Int. J. Approx. Reason. 172, p. 109212. External Links: Link, Document Cited by: §5. [26] B. Legastelois, M. Lesot, and A. R. d’Allonnes (2017) Typology of axioms for a weighted modal logic. International Journal of Approximate Reasoning 90, p. 341–358. External Links: ISSN 0888-613X, Document, Link Cited by: §5. [27] L. Lin, L. Wang, J. Guo, and K. Wong (2025) Investigating bias in llm-based bias detection: disparities between llms and human perception. In Proceedings of COLING, Cited by: §1. [28] M. Maaz and T. C. Y. Chan (2025) Formal verification of markov processes with learned parameters. External Links: 2501.15767, Link Cited by: §5. [29] L. Monteiro Paes et al. (2025) Direct steering optimization for bias mitigation. arXiv preprint arXiv:2512.15926. Cited by: §1. [30] A. Moskowakis (1957) On a generalization of quantifiers. Fundamenta Mathematicae. Cited by: §5. [31] N. J. Nilsson (1986) Probabilistic logic. Artificial Intelligence 28 (1), p. 71–87. External Links: ISSN 0004-3702, Document, Link Cited by: §5. [32] P. Seshadri, S. Singh, and Y. Elazar (2023) The bias amplification paradox in text-to-image generation. External Links: 2308.00755, Link Cited by: §1. [33] Z. Siddique, I. Khalid, et al. (2025) Shifting perspectives: steering vector ensembles for robust bias mitigation in llms. arXiv preprint arXiv:2503.05371. Cited by: §1. [34] A. A. Syed (2025) Guardrails for large language models: a review of techniques and challenges. URF Journals. Cited by: §1. [35] K. W. Wagner (1986) The complexity of combinatorial problems with succinct input representation. Acta informatica 23 (3), p. 325–356. Cited by: §5. [36] H. Zhou, Z. Feng, Z. Zhu, J. Qian, and K. Mao (2024) UniBias: unveiling and mitigating llm bias through internal attention and ffn manipulation. External Links: ISBN 9798331314385 Cited by: §1.