diff --git a/Project.toml b/Project.toml index d5737c0..7cc7c9d 100644 --- a/Project.toml +++ b/Project.toml @@ -3,15 +3,15 @@ name = "Axiology" uuid = "868b87ec-ec5d-47a0-ab5f-c8a8ecbd97bd" authors = ["Jonathan D.A. Jewell "] -version = "0.1.0" +version = "0.1.1" license = "MPL-2.0" [deps] Statistics = "10745b16-79ce-11e8-11f9-7d13ad32a3b2" -LinearAlgebra = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e" [compat] -julia = "1.9" +Statistics = "1" +julia = "1.10" [extras] Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40" diff --git a/src/Axiology.jl b/src/Axiology.jl index 2a59d34..4577c86 100644 --- a/src/Axiology.jl +++ b/src/Axiology.jl @@ -4,80 +4,60 @@ """ Axiology -The Axiology.jl module provides a robust framework for integrating value theory -into machine learning models. In an era where AI systems increasingly influence -critical decisions, understanding and explicitly managing their ethical and -economic implications is paramount. This module allows practitioners and researchers -to define, optimize, and formally verify various values within their ML pipelines. - -The term "Axiology" (from Greek ἀξία, axía, "value"; and -λογία, -logia, "theory") -refers to the philosophical study of value. In this context, Axiology.jl brings -this study into the computational domain, providing tools to operationalize and -reason about values such as fairness, welfare, profit, efficiency, and safety. - -Key Features & Applications: ----------------------------- -1. **Value Type System**: Define diverse ethical and economic values (e.g., `Fairness`, - `Welfare`, `Profit`, `Efficiency`, `Safety`) as first-class citizens. This allows - for explicit representation of desired model behaviors beyond traditional performance metrics. -2. **Value Satisfaction Checking**: Assess whether a given ML model's behavior or - outcome `satisfy` predefined value criteria (e.g., is a model "fair" according - to a specific metric and threshold?). -3. **Multi-Objective Optimization**: Address the inherent trade-offs between - competing values (e.g., fairness vs. efficiency, profit vs. safety). The module - supports finding optimal model configurations that balance multiple objectives. -4. **Pareto Frontier Analysis**: Explore the set of non-dominated solutions in - multi-objective optimization, providing insights into the best possible trade-offs - between different values. -5. **Value Verification**: Lay the groundwork for formal verification of value properties, - ensuring that models adhere to their intended ethical and economic principles - under various conditions. - -Axiology.jl aims to foster more transparent, accountable, and ethically aligned AI systems -by moving beyond black-box optimization towards explicit value-driven design. It provides -a bridge between philosophical considerations of value and the practical implementation -of machine learning. +Value theory for machine-learning and decision systems: make the values a +system is meant to serve explicit, typed and checkable. + +Axiology (from Greek ἀξία, *axía*, "value", and -λογία, *-logia*, "study") is the +philosophical study of value. This package gives a small set of value concepts a +computational form so they can be stated, scored and compared: + +1. **Value types** — `Fairness`, `Welfare`, `Profit`, `Efficiency` and `Safety`, + all subtypes of `Value`, each carrying its metric, threshold or target, and a + weight. +2. **Satisfaction checks** — `satisfy(value, state)` reports whether a system + state (a `Dict` of predictions, utilities, profit, timings, …) meets the value. +3. **Fairness and welfare measures** — `demographic_parity`, `equalized_odds`, + `equal_opportunity`, `disparate_impact`, `individual_fairness`; + `utilitarian_welfare`, `rawlsian_welfare`, `egalitarian_welfare`. +4. **Multi-objective comparison** — `value_score`, `weighted_score`, + `normalize_scores`, `dominated` and `pareto_frontier` compare candidate + states across several values without hiding the trade-offs. +5. **Verification evidence** — `verify_value` checks the shape of a + caller-supplied attestation, and `verify_receipt` strictly checks an ECHIDNA + `echidna.prove.result/1` receipt. Neither runs a prover. `safety_verdict` + reports `:entailed`, `:refuted` or `:unresolved` so missing safety evidence + stays visible. # Example ```julia using Axiology -# Define a fairness criterion -fairness = Fairness( - metric = :demographic_parity, - protected_attributes = [:gender, :race], - threshold = 0.05 -) +fairness = Fairness(metric = :demographic_parity, + protected_attributes = [:group], + threshold = 0.05) -# Simulate a model's state or evaluation results -model_evaluation_state = Dict( - :predictions => [0.8, 0.7, 0.6, 0.9, 0.5, 0.75], - :protected => [:male, :female, :male, :female, :male, :female], - :actual_labels => [1, 1, 0, 1, 0, 1], - :disparity => 0.03 # Assuming a pre-calculated disparity for demographic_parity +state = Dict( + :predictions => [1, 0, 1, 1, 0, 1], + :protected => [:a, :a, :b, :b, :b, :a], ) -# Check if the model satisfies the defined fairness criterion -@assert satisfy(fairness, model_evaluation_state) # True if disparity < threshold +satisfy(fairness, state) # true: both groups have a positive rate of 2/3 -# Define multiple competing values for optimization -values_to_optimize = [ - Welfare(metric = :utilitarian, weight = 0.4), - Fairness(metric = :equalized_odds, weight = 0.3), - Efficiency(metric = :computation_time, weight = 0.3) +values = [ + Welfare(metric = :utilitarian, weight = 0.5), + Fairness(metric = :demographic_parity, threshold = 0.1, weight = 0.5), ] - -# (Conceptual) Find solutions on the Pareto frontier for a given system -# In practice, `system` would represent an ML model or decision-making process -# and `pareto_frontier` would search its configuration space. -# solutions = pareto_frontier(my_ml_system_configs, values_to_optimize) +candidates = [ + Dict(:utilities => [3.0, 3.0], :predictions => [1, 1], :protected => [:a, :b]), + Dict(:utilities => [9.0, 0.0], :predictions => [1, 0], :protected => [:a, :b]), +] +pareto_frontier(candidates, values) # both survive: one is fairer, the other has more welfare ``` """ module Axiology using Statistics -using LinearAlgebra # Core value types export Value, Fairness, Welfare, Profit, Efficiency, Safety @@ -88,6 +68,7 @@ export disparate_impact_metric, individual_fairness_metric export utilitarian_metric, rawlsian_metric, egalitarian_metric export pareto_metric, kaldor_hicks_metric, computation_time_metric export satisfy, maximize, verify_value +export verify_receipt, safety_verdict, PROVE_RESULT_SCHEMA export pareto_frontier, dominated, value_score export weighted_score, normalize_scores diff --git a/src/fairness.jl b/src/fairness.jl index 904bf1a..530a2bf 100644 --- a/src/fairness.jl +++ b/src/fairness.jl @@ -1,6 +1,23 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell +""" + demographic_parity(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64 + +Return the demographic-parity disparity: the largest difference in mean +prediction (the positive-prediction rate, for binary predictions) between any +two protected groups. `0.0` means perfect parity. + +Returns `0.0` when fewer than two groups are present. + +# Example + +```julia +predictions = [1, 0, 1, 1, 0, 1] +protected = [:A, :A, :B, :B, :B, :A] +demographic_parity(predictions, protected) # 0.0 (both groups have rate 2/3) +``` +""" function demographic_parity(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64 @assert length(predictions) == length(protected_attributes) "Lengths must match." unique_groups = unique(protected_attributes) @@ -17,6 +34,28 @@ function demographic_parity(predictions::AbstractVector, protected_attributes::A return maximum(rates) - minimum(rates) end +""" + equalized_odds(predictions::AbstractVector{<:Real}, labels::AbstractVector{<:Real}, + protected_attributes::AbstractVector)::Float64 + +Return the equalized-odds disparity: the larger of the maximum between-group +difference in true-positive rate (TPR) and in false-positive rate (FPR). +`0.0` means the groups are treated alike on both rates. + +A group with no positive labels has no defined TPR and is left out of the TPR +comparison; likewise a group with no negative labels is left out of the FPR +comparison. Each comparison needs at least two groups with a defined rate and +otherwise contributes `0.0`. Returns `0.0` when fewer than two groups are present. + +# Example + +```julia +predictions = [1, 0, 1, 1, 0, 1] +labels = [1, 0, 0, 1, 0, 1] +protected = [:A, :A, :B, :B, :B, :A] +equalized_odds(predictions, labels, protected) +``` +""" function equalized_odds(predictions::AbstractVector{<:Real}, labels::AbstractVector{<:Real}, protected_attributes::AbstractVector)::Float64 @assert length(predictions) == length(labels) == length(protected_attributes) "Lengths must match." @@ -51,6 +90,26 @@ function equalized_odds(predictions::AbstractVector{<:Real}, labels::AbstractVec return max(max_tpr_disparity, max_fpr_disparity) end +""" + equal_opportunity(predictions::AbstractVector{<:Real}, labels::AbstractVector{<:Real}, + protected_attributes::AbstractVector)::Float64 + +Return the equal-opportunity disparity: the maximum between-group difference in +true-positive rate (TPR) only. `0.0` means individuals who merit a positive +outcome receive one at the same rate in every group. + +Groups with no positive labels have no defined TPR and are left out; if fewer +than two groups have a defined TPR the result is `0.0`. + +# Example + +```julia +predictions = [1, 0, 1, 1, 0, 1] +labels = [1, 0, 0, 1, 0, 1] +protected = [:A, :A, :B, :B, :B, :A] +equal_opportunity(predictions, labels, protected) +``` +""" function equal_opportunity(predictions::AbstractVector{<:Real}, labels::AbstractVector{<:Real}, protected_attributes::AbstractVector)::Float64 @assert length(predictions) == length(labels) == length(protected_attributes) "Lengths must match." @@ -75,6 +134,29 @@ function equal_opportunity(predictions::AbstractVector{<:Real}, labels::Abstract return length(tprs) >= 2 ? maximum(tprs) - minimum(tprs) : 0.0 end +""" + disparate_impact(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64 + +Return the disparate-impact ratio: the lowest group selection rate divided by +the highest. `1.0` means equal selection rates; values near `0.0` mean strong +disparity. Under the "four-fifths rule" a ratio below `0.8` is commonly read as +evidence of adverse impact. + +Returns `1.0` when fewer than two groups are present or when no group is ever +selected. + +Note that this is a ratio where *higher is fairer*, the opposite orientation to +the disparity metrics above; `satisfy(::Fairness, …)` therefore reads a +`:disparate_impact` threshold as a minimum ratio (e.g. `threshold = 0.8`). + +# Example + +```julia +predictions = [1, 0, 1, 1, 0, 1] +protected = [:A, :A, :B, :B, :B, :A] +disparate_impact(predictions, protected) # 1.0 +``` +""" function disparate_impact(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64 @assert length(predictions) == length(protected_attributes) "Lengths must match." unique_groups = unique(protected_attributes) @@ -93,6 +175,28 @@ function disparate_impact(predictions::AbstractVector, protected_attributes::Abs return max_rate > 0.0 ? min_rate / max_rate : 1.0 end +""" + individual_fairness(predictions::AbstractVector, similarity_matrix::AbstractMatrix; + similarity_threshold::Float64 = 0.8)::Float64 + +Return the mean absolute prediction difference over all pairs of individuals +whose similarity exceeds `similarity_threshold` ("similar individuals should be +treated similarly"). `0.0` is best. + +`similarity_matrix` must be `n×n` for `n` predictions, with entries normally in +`[0, 1]`. Returns `0.0` when no pair is similar enough to compare. + +# Example + +```julia +predictions = [0.8, 0.2, 0.7, 0.3] +similarity = [1.0 0.9 0.1 0.2; + 0.9 1.0 0.2 0.1; + 0.1 0.2 1.0 0.85; + 0.2 0.1 0.85 1.0] +individual_fairness(predictions, similarity; similarity_threshold = 0.8) +``` +""" function individual_fairness(predictions::AbstractVector, similarity_matrix::AbstractMatrix; similarity_threshold::Float64 = 0.8)::Float64 n = length(predictions) @@ -111,6 +215,19 @@ function individual_fairness(predictions::AbstractVector, similarity_matrix::Abs return count > 0 ? total_diff / count : 0.0 end +""" + satisfy(value::Fairness, state::Dict)::Bool + +Return whether `state` meets the fairness criterion `value`. + +`state` must hold `:predictions`, plus `:protected` (or `:protected_attributes`) +for the group metrics, `:labels` for `:equalized_odds`/`:equal_opportunity`, and +`:similarity_matrix` for `:individual_fairness`. A missing key raises an error. + +For the disparity metrics the check is `disparity <= value.threshold`. For +`:disparate_impact` it is `ratio >= value.threshold`, so the threshold is a +minimum ratio there (the default `0.05` is far looser than the usual `0.8`). +""" function satisfy(value::Fairness, state::Dict)::Bool predictions = get(state, :predictions, nothing) protected = get(state, :protected, get(state, :protected_attributes, nothing)) diff --git a/src/fairness.jl.backup b/src/fairness.jl.backup deleted file mode 100644 index c5d5d8e..0000000 --- a/src/fairness.jl.backup +++ /dev/null @@ -1,493 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell - -# Fairness Metric Implementations -# -# This file provides a collection of functions for calculating various fairness -# metrics in machine learning models. Fairness is a critical ethical value that -# ensures ML systems do not perpetuate or amplify existing societal biases, -# leading to discriminatory outcomes for certain groups. -# -# The metrics implemented here help quantify different notions of fairness, -# each with its own definition and implications: -# - **Group Fairness Metrics**: These metrics assess fairness by comparing -# outcomes or error rates across predefined demographic groups (e.g., based -# on race, gender, age). Examples include Demographic Parity, Equalized Odds, -# and Equal Opportunity. -# - **Individual Fairness Metrics**: These metrics aim to ensure that similar -# individuals are treated similarly by the model, irrespective of their group -# membership. An example is Individual Fairness. -# -# Each metric function typically takes model predictions, true labels, and/or -# protected attributes as input, and returns a quantitative measure of disparity -# or unfairness. These can then be used with the `Fairness` value type in Axiology.jl -# to check satisfaction against a defined threshold or to optimize for fairness -# in a multi-objective setting. - -""" - demographic_parity(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64 - -Calculates the demographic parity disparity, a widely used group fairness metric. -Demographic parity (also known as statistical parity) requires that the proportion -of individuals receiving a positive prediction (or outcome) is approximately equal -across different protected groups, regardless of their actual characteristics. - -Formally, demographic parity is achieved when `P(Ŷ=1 | A=a) ≈ P(Ŷ=1 | A=b)` for -any two groups `a` and `b` defined by the protected attribute `A`. - -This function returns the maximum absolute difference in positive prediction rates -among all unique protected groups. A value of `0.0` indicates perfect demographic -parity, while higher values (up to `1.0`) indicate greater disparity. - -# Arguments -- `predictions::AbstractVector`: A vector of model predictions. Elements can be - binary (`0` or `1`) for hard classifications, - or probabilities (`Float64` between `0.0` and `1.0`) - for soft classifications. -- `protected_attributes::AbstractVector`: A vector of categorical protected group - indicators (e.g., `[:male, :female]`, - `["GroupA", "GroupB"]`, or integer IDs). - The length of this vector must match `predictions`. - -# Returns -- `Float64`: The maximum absolute difference in positive prediction rates observed - between any two unique groups. Ranges from `0.0` (perfect parity) to - `1.0` (maximum disparity). - -# Limitations and Critiques: -Demographic parity is often criticized because it may lead to unfair outcomes -if there are legitimate differences in base rates between groups (e.g., if one -group genuinely has a lower propensity for the positive outcome). It can -force a model to make inaccurate predictions to achieve parity, potentially -sacrificing individual accuracy. - -# Example - -```julia -predictions = [1, 0, 1, 1, 0, 1, 0, 1] # Model predictions (e.g., loan approved = 1) -protected = [:male, :female, :male, :female, :male, :female, :male, :female] # Protected attribute (gender) - -# Calculate disparity -disparity = demographic_parity(predictions, protected) -println("Demographic Parity Disparity: $(disparity)") # Expected to be > 0 if rates differ -``` -""" -function demographic_parity(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64 - @assert length(predictions) == length(protected_attributes) "Lengths of predictions and protected_attributes must match." - - unique_groups = unique(protected_attributes) - if length(unique_groups) < 2 - return 0.0 # No disparity if only one group is present - end - - # Compute positive prediction rate for each group - group_rates = Dict{Any,Float64}() - for group in unique_groups - group_mask = protected_attributes .== group - group_preds = predictions[group_mask] - group_rates[group] = isempty(group_preds) ? 0.0 : mean(group_preds) - end - - # Calculate the maximum pairwise absolute difference in positive rates - rates = collect(values(group_rates)) - return maximum(rates) - minimum(rates) -end - -""" - equalized_odds(predictions::AbstractVector{<:Real}, labels::AbstractVector{<:Real}, - protected_attributes::AbstractVector)::Float64 - -Calculates the equalized odds disparity, a group fairness metric that aims to ensure -that a model's true positive rates (TPR) and false positive rates (FPR) are equal -across all protected groups. This means that for individuals with the same true outcome, -the model should predict that outcome equally well regardless of their group membership. - -Formally, equalized odds is satisfied when `P(Ŷ=1 | A=a, Y=y) ≈ P(Ŷ=1 | A=b, Y=y)` -for any two groups `a` and `b`, and for both `y=0` (negative outcome) and `y=1` (positive outcome). - -This function computes the maximum absolute difference in TPRs and FPRs across all unique -protected groups, and returns the larger of these two disparities. A value of `0.0` -indicates perfect equalized odds, while higher values indicate greater disparity. - -# Arguments -- `predictions::AbstractVector{<:Real}`: A vector of binary model predictions (`0` or `1`). -- `labels::AbstractVector{<:Real}`: A vector of true binary labels (`0` or `1`). -- `protected_attributes::AbstractVector`: A vector of categorical protected group indicators. - The lengths of all input vectors must match. - -# Returns -- `Float64`: The maximum disparity observed in either true positive rates or - false positive rates across all unique protected groups. Ranges from `0.0` - (perfect equalized odds) to `1.0` (maximum disparity). - -# Connection to Equal Opportunity: -Equalized odds is a stricter condition than `equal_opportunity`, which only requires -equal TPRs. Satisfying equalized odds implies satisfying equal opportunity. - -# Example - -```julia -predictions = [1, 0, 1, 1, 0, 1, 0, 1] -labels = [1, 1, 0, 1, 0, 0, 1, 1] -protected = [:male, :female, :male, :female, :male, :female, :male, :female] - -# Calculate disparity -disparity = equalized_odds(predictions, labels, protected) -println("Equalized Odds Disparity: $(disparity)") -``` -""" -function equalized_odds(predictions::AbstractVector{<:Real}, labels::AbstractVector{<:Real}, - protected_attributes::AbstractVector)::Float64 - @assert length(predictions) == length(labels) == length(protected_attributes) "Lengths of predictions, labels, and protected_attributes must match." - - unique_groups = unique(protected_attributes) - if length(unique_groups) < 2 - return 0.0 - end - - tpr_disparities = Float64[] - fpr_disparities = Float64[] - - for group in unique_groups - group_mask = protected_attributes .== group - group_preds = predictions[group_mask] - group_labels = labels[group_mask] - - # True positives and false positives - tp = sum((group_preds .== 1) .& (group_labels .== 1)) - fp = sum((group_preds .== 1) .& (group_labels .== 0)) - tn = sum((group_preds .== 0) .& (group_labels .== 0)) - fn = sum((group_preds .== 0) .& (group_labels .== 1)) - - # True Positive Rate (TPR) and False Positive Rate (FPR) - # Handle division by zero for groups with no positive/negative true labels - tpr = (tp + fn) > 0 ? tp / (tp + fn) : 0.0 - fpr = (fp + tn) > 0 ? fp / (fp + tn) : 0.0 - - push!(tpr_disparities, tpr) - push!(fpr_disparities, fpr) - end - - max_tpr_disparity = maximum(tpr_disparities) - minimum(tpr_disparities) - max_fpr_disparity = maximum(fpr_disparities) - minimum(fpr_disparities) - - return max(max_tpr_disparity, max_fpr_disparity) -end - -""" - equal_opportunity(predictions::AbstractVector{<:Real}, labels::AbstractVector{<:Real}, - protected_attributes::AbstractVector)::Float64 - -Calculates the equal opportunity disparity, a group fairness metric. -Equal opportunity requires that the true positive rate (TPR) is equal across -all protected groups. This means that among the truly positive individuals, -the model should be equally likely to predict a positive outcome, regardless -of their group membership. It is a weaker condition than equalized odds. - -Formally, equal opportunity is satisfied when `P(Ŷ=1 | A=a, Y=1) ≈ P(Ŷ=1 | A=b, Y=1)` -for any two groups `a` and `b` defined by the protected attribute `A`. - -This function computes the maximum absolute difference in TPRs among all unique -protected groups. A value of `0.0` indicates perfect equal opportunity, while -higher values indicate greater disparity. - -# Arguments -- `predictions::AbstractVector{<:Real}`: A vector of binary model predictions (`0` or `1`). -- `labels::AbstractVector{<:Real}`: A vector of true binary labels (`0` or `1`). -- `protected_attributes::AbstractVector`: A vector of categorical protected group indicators. - The lengths of all input vectors must match. - -# Returns -- `Float64`: The maximum absolute difference in true positive rates observed - between any two unique groups. Ranges from `0.0` (perfect equal opportunity) - to `1.0` (maximum disparity). - -# Connection to Equalized Odds: -Equal opportunity focuses only on the TPR for positive outcomes, making it a -less strict requirement than `equalized_odds`, which also considers false -positive rates. - -# Example - -```julia -predictions = [1, 0, 1, 1, 0, 1, 0, 1] -labels = [1, 1, 0, 1, 0, 0, 1, 1] -protected = [:male, :female, :male, :female, :male, :female, :male, :female] - -# Calculate disparity -disparity = equal_opportunity(predictions, labels, protected) -println("Equal Opportunity Disparity: $(disparity)") -``` -""" -function equal_opportunity(predictions::AbstractVector{<:Real}, labels::AbstractVector{<:Real}, - protected_attributes::AbstractVector)::Float64 - @assert length(predictions) == length(labels) == length(protected_attributes) "Lengths of predictions, labels, and protected_attributes must match." - - unique_groups = unique(protected_attributes) - if length(unique_groups) < 2 - return 0.0 - end - - tprs = Float64[] - - for group in unique_groups - group_mask = protected_attributes .== group - group_preds = predictions[group_mask] - group_labels = labels[group_mask] - - # True positives and false negatives (for TPR calculation) - tp = sum((group_preds .== 1) .& (group_labels .== 1)) - fn = sum((group_preds .== 0) .& (group_labels .== 1)) - - # True Positive Rate (TPR) - # Handle division by zero for groups with no positive true labels - tpr = (tp + fn) > 0 ? tp / (tp + fn) : 0.0 - push!(tprs, tpr) - end - - return maximum(tprs) - minimum(tprs) -end - -""" - disparate_impact(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64 - -Calculates the disparate impact ratio, a group fairness metric often used -in regulatory and legal contexts. Disparate impact occurs when a policy -or algorithm disproportionately harms a protected group, even if there -is no explicit intent to discriminate. - -The disparate impact ratio is defined as the ratio of the positive prediction -rate for the unprivileged group to the positive prediction rate for the -privileged group. By convention, the unprivileged group is usually the one -with the lower positive prediction rate. - -Formally, DI = `min_rate / max_rate`, where `min_rate` and `max_rate` are -the minimum and maximum positive prediction rates across all protected groups. - -The "80% Rule": -A common guideline (e.g., in US employment law) suggests that disparate impact -may be present if the selection rate for a protected group is less than 80% -(or 4/5ths) of the rate for the group with the highest selection rate. -A ratio below `0.8` is typically considered to indicate adverse impact. - -# Arguments -- `predictions::AbstractVector`: A vector of model predictions (binary `0` or `1`, - or probabilities). -- `protected_attributes::AbstractVector`: A vector of categorical protected group indicators. - The lengths of both vectors must match. - -# Returns -- `Float64`: The disparate impact ratio. - - A value of `1.0` indicates no disparate impact. - - A value less than `1.0` indicates adverse impact (lower positive rate for - some group compared to others). - - A value greater than `1.0` would imply an advantage for the "unprivileged" group. - -# Example - -```julia -predictions = [1, 0, 1, 1, 0, 1, 0, 1] # Model predictions -protected = [:male, :female, :male, :female, :male, :female, :male, :female] # Protected attribute - -# Calculate disparate impact ratio -di_ratio = disparate_impact(predictions, protected) -println("Disparate Impact Ratio: $(di_ratio)") # Check if di_ratio < 0.8 -``` -""" -function disparate_impact(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64 - @assert length(predictions) == length(protected_attributes) "Lengths of predictions and protected_attributes must match." - - unique_groups = unique(protected_attributes) - if length(unique_groups) < 2 - return 1.0 # No impact if only one group is present - end - - # Compute positive prediction rate for each group - group_rates = Dict{Any,Float64}() - for group in unique_groups - group_mask = protected_attributes .== group - group_preds = predictions[group_mask] - group_rates[group] = isempty(group_preds) ? 0.0 : mean(group_preds) - end - - rates = collect(values(group_rates)) - min_rate = minimum(rates) - max_rate = maximum(rates) - - # Handle cases where max_rate might be zero to avoid division by zero - return max_rate > 0.0 ? min_rate / max_rate : 1.0 -end - -""" - individual_fairness(predictions::AbstractVector, similarity_matrix::AbstractMatrix; - similarity_threshold::Float64 = 0.8)::Float64 - -Calculates a metric for individual fairness. The principle of individual fairness -states that "similar individuals should receive similar predictions." This metric -quantifies the extent to which a model adheres to this principle by averaging the -absolute prediction differences for pairs of individuals deemed "similar" based -on a provided similarity matrix. - -# Arguments -- `predictions::AbstractVector`: A vector of model predictions (can be binary, probabilities, - or continuous values). -- `similarity_matrix::AbstractMatrix`: A square, symmetric matrix of pairwise similarities - between individuals in the dataset. `similarity_matrix[i, j]` - should represent the inherent similarity between individual `i` - and individual `j`. Values are typically in the range `[0, 1]`. - -# Keyword Arguments: -- `similarity_threshold::Float64`: A threshold used to determine if two individuals are - considered "similar". If `similarity_matrix[i, j]` is - greater than this threshold, the pair `(i, j)` is - included in the fairness calculation. Defaults to `0.8`. - -# Returns -- `Float64`: The average absolute prediction difference for all pairs of individuals - whose similarity exceeds `similarity_threshold`. - - A value of `0.0` indicates perfect individual fairness (similar individuals - receive identical predictions). - - Higher values indicate greater individual unfairness. - -# Interpretation of `similarity_matrix`: -The `similarity_matrix` is crucial and must be independently defined, often based -on domain knowledge or features deemed irrelevant to the outcome (e.g., a similarity -based on all attributes *except* the protected ones). Its construction implicitly -encodes what "similar individuals" means in context. - -# Example - -```julia -predictions = [0.1, 0.2, 0.8, 0.9, 0.15] -# Example similarity matrix where high values mean similar (e.g., cosine similarity of features) -similarity = [ - 1.0 0.9 0.1 0.05 0.85; - 0.9 1.0 0.15 0.1 0.8; - 0.1 0.15 1.0 0.95 0.0; - 0.05 0.1 0.95 1.0 0.0; - 0.85 0.8 0.0 0.0 1.0 -] - -# Calculate individual fairness with default similarity threshold -fairness_score = individual_fairness(predictions, similarity) -println("Individual Fairness Score: $(fairness_score)") -``` -""" -function individual_fairness(predictions::AbstractVector, similarity_matrix::AbstractMatrix; - similarity_threshold::Float64 = 0.8)::Float64 - n = length(predictions) - @assert size(similarity_matrix) == (n, n) "Similarity matrix must be n×n where n is the length of predictions." - @assert similarity_threshold >= 0.0 && similarity_threshold <= 1.0 "Similarity threshold must be in [0, 1]." - - - total_diff = 0.0 - count = 0 - - for i in 1:n - for j in (i+1):n # Avoid double counting and self-similarity - if similarity_matrix[i, j] > similarity_threshold # Consider similar if similarity > threshold - total_diff += abs(predictions[i] - predictions[j]) - count += 1 - end - end - end - - return count > 0 ? total_diff / count : 0.0 -end - -""" - satisfy(value::Fairness, state::Dict)::Bool - -Checks if a given system state (e.g., model predictions and attributes) -satisfies a specified `Fairness` criterion. This function acts as an -evaluator, determining whether the observed disparity for the chosen -fairness metric falls within the acceptable `value.threshold`. - -# Arguments -- `value::Fairness`: A `Fairness` object specifying the metric, protected attributes, - and threshold to evaluate against. -- `state::Dict`: A dictionary representing the current system state or model evaluation - results. The required keys in this dictionary depend on the - `value.metric`: - - All metrics require: - - `:predictions`: `AbstractVector{<:Real}` - Binary predictions or probabilities. - - `:protected` or `:protected_attributes`: `AbstractVector` - Protected group indicators. - - Metrics requiring true labels also need: - - `:labels`: `AbstractVector{<:Real}` - True binary labels. (e.g., for `equalized_odds`, `equal_opportunity`). - - Metrics requiring similarity also need: - - `:similarity_matrix`: `AbstractMatrix{<:Real}` - Pairwise similarity matrix. (e.g., for `individual_fairness`). - -# Returns -- `Bool`: `true` if the system state satisfies the `Fairness` criterion (i.e., - the calculated disparity is less than or equal to `value.threshold`), - `false` otherwise. For `disparate_impact`, it returns `true` if the - ratio is `>= 0.8`. - -# Throws -- `ErrorException`: If a required key for a specific metric is missing from `state`. -- `ErrorException`: If an unknown fairness metric is specified in `value.metric`. - -# Example - -```julia -# Example for demographic parity -fairness_dp = Fairness(metric = :demographic_parity, threshold = 0.05) -state_dp = Dict( - :predictions => [1, 0, 1, 1, 0, 1, 0, 1], - :protected => [:male, :female, :male, :female, :male, :female, :male, :female] -) -println("Demographic Parity Satisfied: $(satisfy(fairness_dp, state_dp))") - -# Example for equalized odds -fairness_eo = Fairness(metric = :equalized_odds, threshold = 0.1) -state_eo = Dict( - :predictions => [1, 0, 1, 1, 0, 1, 0, 1], - :labels => [1, 1, 0, 1, 0, 0, 1, 1], - :protected => [:male, :female, :male, :female, :male, :female, :male, :female] -) -println("Equalized Odds Satisfied: $(satisfy(fairness_eo, state_eo))") - -# Example for individual fairness -fairness_if = Fairness(metric = :individual_fairness, threshold = 0.2) -sim_matrix = [1.0 0.9 0.1; 0.9 1.0 0.2; 0.1 0.2 1.0] # Dummy similarity -state_if = Dict( - :predictions => [0.1, 0.2, 0.8], - :similarity_matrix => sim_matrix -) -println("Individual Fairness Satisfied: $(satisfy(fairness_if, state_if))") -``` -""" -function satisfy(value::Fairness, state::Dict)::Bool - # Extract data from state - predictions = get(state, :predictions, nothing) - protected = get(state, :protected, get(state, :protected_attributes, nothing)) - labels = get(state, :labels, nothing) - similarity_matrix = get(state, :similarity_matrix, nothing) - - isnothing(predictions) && error("State must contain :predictions for fairness evaluation.") - isnothing(protected) && value.metric != :individual_fairness && error("State must contain :protected or :protected_attributes for group fairness evaluation.") - isnothing(similarity_matrix) && value.metric == :individual_fairness && error("State must contain :similarity_matrix for individual fairness evaluation.") - - - # Compute disparity based on metric - disparity = if value.metric == :demographic_parity - demographic_parity(predictions, protected) - elseif value.metric == :equalized_odds - isnothing(labels) && error("equalized_odds metric requires :labels in state.") - equalized_odds(predictions, labels, protected) - elseif value.metric == :equal_opportunity - isnothing(labels) && error("equal_opportunity metric requires :labels in state.") - equal_opportunity(predictions, labels, protected) - elseif value.metric == :disparate_impact - # Disparate impact is handled differently: returns true if ratio >= 0.8 - di_ratio = disparate_impact(predictions, protected) - return di_ratio >= value.threshold # Threshold for DI is usually 0.8 or 0.7 - elseif value.metric == :individual_fairness - individual_fairness(predictions, similarity_matrix) - else - error("Unknown fairness metric: $(value.metric). Please ensure it is a valid metric from FairnessMetric enum.") - end - - # Check against threshold for all metrics except disparate_impact (which returns true/false directly) - return disparity <= value.threshold -end diff --git a/src/fairness_minimal.jl b/src/fairness_minimal.jl deleted file mode 100644 index 34bb9c2..0000000 --- a/src/fairness_minimal.jl +++ /dev/null @@ -1,26 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell - -""" - demographic_parity(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64 - -Calculates the demographic parity disparity. -""" -function demographic_parity(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64 - @assert length(predictions) == length(protected_attributes) "Lengths must match." - - unique_groups = unique(protected_attributes) - if length(unique_groups) < 2 - return 0.0 - end - - group_rates = Dict{Any,Float64}() - for group in unique_groups - group_mask = protected_attributes .== group - group_preds = predictions[group_mask] - group_rates[group] = isempty(group_preds) ? 0.0 : mean(group_preds) - end - - rates = collect(values(group_rates)) - return maximum(rates) - minimum(rates) -end diff --git a/src/fairness_nodocs.jl b/src/fairness_nodocs.jl deleted file mode 100644 index c5e3a62..0000000 --- a/src/fairness_nodocs.jl +++ /dev/null @@ -1,258 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell - -""" - demographic_parity(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64 - -Compute the demographic parity disparity across protected groups. - -Demographic parity requires that the positive prediction rate (the proportion of -individuals receiving a favorable outcome) is equal across all protected groups. -This function calculates the maximum difference in positive prediction rates -between any two groups, with a value of 0.0 indicating perfect parity. - -# Arguments -- `predictions::AbstractVector`: Binary predictions or scores for each individual. -- `protected_attributes::AbstractVector`: Group membership for each individual - (e.g., gender, race). - -# Returns -- `Float64`: The maximum difference in positive prediction rates between groups. - Returns 0.0 if there are fewer than 2 groups. - -# Example - -```julia -predictions = [1, 0, 1, 1, 0, 1] -protected = [:A, :A, :B, :B, :B, :A] -disparity = demographic_parity(predictions, protected) -``` -""" -function demographic_parity(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64 - @assert length(predictions) == length(protected_attributes) "Lengths must match." - unique_groups = unique(protected_attributes) - if length(unique_groups) < 2 - return 0.0 - end - group_rates = Dict{Any,Float64}() - for group in unique_groups - group_mask = protected_attributes .== group - group_preds = predictions[group_mask] - group_rates[group] = isempty(group_preds) ? 0.0 : mean(group_preds) - end - rates = collect(values(group_rates)) - return maximum(rates) - minimum(rates) -end - -""" - equalized_odds(predictions::AbstractVector{<:Real}, labels::AbstractVector{<:Real}, - protected_attributes::AbstractVector)::Float64 - -Compute the equalized odds disparity across protected groups. - -Equalized odds requires that both the true positive rate (TPR) and false positive -rate (FPR) are equal across all protected groups. This function calculates the -maximum disparity in either TPR or FPR between groups, with a value of 0.0 -indicating perfect equalized odds. - -# Arguments -- `predictions::AbstractVector{<:Real}`: Binary predictions (typically 0 or 1) for - each individual. -- `labels::AbstractVector{<:Real}`: True binary labels (typically 0 or 1) for each - individual. -- `protected_attributes::AbstractVector`: Group membership for each individual - (e.g., gender, race). - -# Returns -- `Float64`: The maximum disparity in TPR or FPR between groups. Returns 0.0 if - there are fewer than 2 groups. - -# Example - -```julia -predictions = [1, 0, 1, 1, 0, 1] -labels = [1, 0, 0, 1, 0, 1] -protected = [:A, :A, :B, :B, :B, :A] -disparity = equalized_odds(predictions, labels, protected) -``` -""" -function equalized_odds(predictions::AbstractVector{<:Real}, labels::AbstractVector{<:Real}, - protected_attributes::AbstractVector)::Float64 - @assert length(predictions) == length(labels) == length(protected_attributes) "Lengths must match." - unique_groups = unique(protected_attributes) - if length(unique_groups) < 2 - return 0.0 - end - tpr_disparities = Float64[] - fpr_disparities = Float64[] - for group in unique_groups - group_mask = protected_attributes .== group - group_preds = predictions[group_mask] - group_labels = labels[group_mask] - tp = sum((group_preds .== 1) .& (group_labels .== 1)) - fp = sum((group_preds .== 1) .& (group_labels .== 0)) - tn = sum((group_preds .== 0) .& (group_labels .== 0)) - fn = sum((group_preds .== 0) .& (group_labels .== 1)) - tpr = (tp + fn) > 0 ? tp / (tp + fn) : 0.0 - fpr = (fp + tn) > 0 ? fp / (fp + tn) : 0.0 - push!(tpr_disparities, tpr) - push!(fpr_disparities, fpr) - end - max_tpr_disparity = maximum(tpr_disparities) - minimum(tpr_disparities) - max_fpr_disparity = maximum(fpr_disparities) - minimum(fpr_disparities) - return max(max_tpr_disparity, max_fpr_disparity) -end - -""" - equal_opportunity(predictions::AbstractVector{<:Real}, labels::AbstractVector{<:Real}, - protected_attributes::AbstractVector)::Float64 - -Compute the equal opportunity disparity across protected groups. - -Equal opportunity is a weaker form of equalized odds that focuses only on the -true positive rate (TPR). It requires that individuals who truly deserve a -positive outcome have an equal chance of receiving it, regardless of their -protected group membership. This function calculates the maximum difference in -TPR between groups, with a value of 0.0 indicating perfect equal opportunity. - -# Arguments -- `predictions::AbstractVector{<:Real}`: Binary predictions (typically 0 or 1) for - each individual. -- `labels::AbstractVector{<:Real}`: True binary labels (typically 0 or 1) for each - individual. -- `protected_attributes::AbstractVector`: Group membership for each individual - (e.g., gender, race). - -# Returns -- `Float64`: The maximum difference in TPR between groups. Returns 0.0 if there - are fewer than 2 groups. - -# Example - -```julia -predictions = [1, 0, 1, 1, 0, 1] -labels = [1, 0, 0, 1, 0, 1] -protected = [:A, :A, :B, :B, :B, :A] -disparity = equal_opportunity(predictions, labels, protected) -``` -""" -function equal_opportunity(predictions::AbstractVector{<:Real}, labels::AbstractVector{<:Real}, - protected_attributes::AbstractVector)::Float64 - @assert length(predictions) == length(labels) == length(protected_attributes) "Lengths must match." - unique_groups = unique(protected_attributes) - if length(unique_groups) < 2 - return 0.0 - end - tprs = Float64[] - for group in unique_groups - group_mask = protected_attributes .== group - group_preds = predictions[group_mask] - group_labels = labels[group_mask] - tp = sum((group_preds .== 1) .& (group_labels .== 1)) - fn = sum((group_preds .== 0) .& (group_labels .== 1)) - tpr = (tp + fn) > 0 ? tp / (tp + fn) : 0.0 - push!(tprs, tpr) - end - return maximum(tprs) - minimum(tprs) -end - -""" - disparate_impact(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64 - -Compute the disparate impact ratio across protected groups. - -Disparate impact measures whether the selection rate (positive prediction rate) -for a protected group is substantially less than for other groups. This function -returns the ratio of the minimum selection rate to the maximum selection rate -across all groups. A value of 1.0 indicates no disparate impact, while values -closer to 0.0 indicate greater disparity. The "80% rule" commonly used in hiring -suggests that a ratio below 0.8 may indicate adverse impact. - -# Arguments -- `predictions::AbstractVector`: Binary predictions or scores for each individual. -- `protected_attributes::AbstractVector`: Group membership for each individual - (e.g., gender, race). - -# Returns -- `Float64`: The ratio of minimum to maximum selection rates across groups. - Returns 1.0 if there are fewer than 2 groups or if the maximum rate is 0.0. - -# Example - -```julia -predictions = [1, 0, 1, 1, 0, 1] -protected = [:A, :A, :B, :B, :B, :A] -ratio = disparate_impact(predictions, protected) -# A ratio < 0.8 may indicate disparate impact under the 80% rule -``` -""" -function disparate_impact(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64 - @assert length(predictions) == length(protected_attributes) "Lengths must match." - unique_groups = unique(protected_attributes) - if length(unique_groups) < 2 - return 1.0 - end - group_rates = Dict{Any,Float64}() - for group in unique_groups - group_mask = protected_attributes .== group - group_preds = predictions[group_mask] - group_rates[group] = isempty(group_preds) ? 0.0 : mean(group_preds) - end - rates = collect(values(group_rates)) - min_rate = minimum(rates) - max_rate = maximum(rates) - return max_rate > 0.0 ? min_rate / max_rate : 1.0 -end - -""" - individual_fairness(predictions::AbstractVector, similarity_matrix::AbstractMatrix; - similarity_threshold::Float64 = 0.8)::Float64 - -Compute the individual fairness metric based on similarity between individuals. - -Individual fairness requires that similar individuals receive similar treatment. -This function measures the average absolute difference in predictions between -pairs of individuals whose similarity exceeds a given threshold. Lower values -indicate better individual fairness (more similar predictions for similar -individuals). - -# Arguments -- `predictions::AbstractVector`: Predictions or scores for each individual. -- `similarity_matrix::AbstractMatrix`: An n×n matrix where `similarity_matrix[i, j]` - indicates the similarity between individuals i and j. - Values should typically be in [0, 1]. -- `similarity_threshold::Float64`: The minimum similarity required for two individuals - to be considered "similar" and compared. Defaults to 0.8. - -# Returns -- `Float64`: The average absolute difference in predictions between similar individuals. - Returns 0.0 if no pairs of individuals exceed the similarity threshold. - -# Example - -```julia -predictions = [0.8, 0.2, 0.7, 0.3] -similarity = [1.0 0.9 0.1 0.2; - 0.9 1.0 0.2 0.1; - 0.1 0.2 1.0 0.85; - 0.2 0.1 0.85 1.0] -fairness = individual_fairness(predictions, similarity, similarity_threshold=0.85) -``` -""" -function individual_fairness(predictions::AbstractVector, similarity_matrix::AbstractMatrix; - similarity_threshold::Float64 = 0.8)::Float64 - n = length(predictions) - @assert size(similarity_matrix) == (n, n) "Similarity matrix must be n×n." - @assert similarity_threshold >= 0.0 && similarity_threshold <= 1.0 "Threshold must be in [0, 1]." - total_diff = 0.0 - count = 0 - for i in 1:n - for j in (i+1):n - if similarity_matrix[i, j] > similarity_threshold - total_diff += abs(predictions[i] - predictions[j]) - count += 1 - end - end - end - return count > 0 ? total_diff / count : 0.0 -end diff --git a/src/optimization.jl b/src/optimization.jl index ca5a7e3..4b69600 100644 --- a/src/optimization.jl +++ b/src/optimization.jl @@ -1,10 +1,49 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell +""" + _require_nonzero_target(value::Value, field::AbstractString) + +Throw an `ArgumentError` explaining that a score normalised by a zero `field` +is undefined, instead of letting the division return `Inf` or `NaN`. +""" +function _require_nonzero_target(value::Value, field::AbstractString) + throw(ArgumentError("value_score($(nameof(typeof(value)))) divides by `$(field)`, " * + "which is 0.0, so the score is undefined; construct the value " * + "with a non-zero `$(field)` to score it.")) +end + +""" + value_score(value::Value, state::Dict)::Float64 + +Score how well `state` does on `value`, higher is better. The scale depends on +the value type: + +- `Fairness`: `1 - disparity / threshold`, floored at `0.0`, so `1.0` is perfect + parity and `0.0` means the disparity reached the threshold. With + `threshold == 0.0` only exact parity scores `1.0`; anything else scores `0.0`. + `:disparate_impact` scores the ratio itself (clamped to `[0, 1]`) and + `:individual_fairness` scores `1 - mean difference`. +- `Welfare`: the welfare function of `:utilities`, scaled to `[0, 1]` by + `:max_welfare` when the state provides a positive one; otherwise the **raw, + unbounded** welfare value. +- `Profit`: `:profit / target`. +- `Efficiency`: `1 - :computation_time / target` (floored at `0.0`), + `1.0`/`0.0` for `:is_pareto_efficient`, or `:net_gain / target`. +- `Safety`: `1.0` when safe, else `0.0` (absent keys count as safe, as in + `satisfy(::Safety, ::Dict)`). + +The group fairness metrics read `:protected`, or `:protected_attributes` when +`:protected` is absent. + +Scores normalised by a target (`Profit`, `Efficiency` `:computation_time` and +`:kaldor_hicks`) throw an `ArgumentError` when that target is `0.0` rather than +returning `Inf` or `NaN`. Note that `Profit()` has `target = 0.0` by default. +""" function value_score(value::Value, state::Dict)::Float64 if value isa Fairness predictions = get(state, :predictions, nothing) - protected = get(state, :protected, nothing) + protected = get(state, :protected, get(state, :protected_attributes, nothing)) labels = get(state, :labels, nothing) similarity_matrix = get(state, :similarity_matrix, nothing) @@ -36,6 +75,8 @@ function value_score(value::Value, state::Dict)::Float64 # For disparity metrics, a lower disparity is better. Convert to score where 1.0 is optimal. # Normalize disparity relative to threshold. If disparity > threshold, score becomes < 0. + # A zero threshold tolerates no disparity at all: 0/0 would otherwise give NaN. + iszero(value.threshold) && return iszero(disparity) ? 1.0 : 0.0 return max(0.0, 1.0 - disparity / value.threshold) elseif value isa Welfare @@ -70,6 +111,7 @@ function value_score(value::Value, state::Dict)::Float64 elseif value isa Profit profit = get(state, :profit, nothing) isnothing(profit) && error("State must contain :profit for Profit value_score.") + iszero(value.target) && _require_nonzero_target(value, "target") # Normalize profit relative to target return profit / value.target @@ -77,6 +119,7 @@ function value_score(value::Value, state::Dict)::Float64 if value.metric == :computation_time time = get(state, :computation_time, nothing) isnothing(time) && error("State must contain :computation_time for Efficiency value_score.") + iszero(value.target) && _require_nonzero_target(value, "target") # Lower time is better - invert and normalize return max(0.0, 1.0 - time / value.target) elseif value.metric == :pareto @@ -86,6 +129,7 @@ function value_score(value::Value, state::Dict)::Float64 elseif value.metric == :kaldor_hicks net_gain = get(state, :net_gain, nothing) isnothing(net_gain) && error("State must contain :net_gain for Efficiency value_score.") + iszero(value.target) && _require_nonzero_target(value, "target") return net_gain / value.target else error("Unknown efficiency metric: $(value.metric) for value_score.") @@ -101,6 +145,24 @@ function value_score(value::Value, state::Dict)::Float64 end end +""" + weighted_score(values::Vector{<:Value}, state::Dict)::Float64 + +Return the weight-averaged `value_score` of `state` across `values`, using each +value's `weight`. Returns `0.0` when every weight is zero. + +This collapses several objectives into one number, so it is only meaningful +when the individual scores share a scale; un-normalised `Welfare` scores (no +`:max_welfare` in `state`) and `Profit`/`Efficiency` ratios can dominate the +average. A poor score on one value can also be bought back by another, even a +critical `Safety`. + +The collapse is lossy: different score profiles map to the same number, so no +function can recover the profile from the result (it has no section — the +mechanised statement is `no-section-of-collapsing-map` in +`hyperpolymath/echo-types`). Use `dominated`/`pareto_frontier` to compare +without collapsing. +""" function weighted_score(values::Vector{<:Value}, state::Dict)::Float64 total_weight = sum(v.weight for v in values) @@ -113,6 +175,12 @@ function weighted_score(values::Vector{<:Value}, state::Dict)::Float64 return weighted_sum / total_weight end +""" + normalize_scores(scores::AbstractVector)::Vector{Float64} + +Min-max normalise `scores` to `[0, 1]`. If every score is equal the result is +all ones. Throws an `ArgumentError` for an empty vector. +""" function normalize_scores(scores::AbstractVector)::Vector{Float64} if isempty(scores) throw(ArgumentError("Cannot normalize an empty vector of scores.")) @@ -128,6 +196,13 @@ function normalize_scores(scores::AbstractVector)::Vector{Float64} return [(s - min_score) / (max_score - min_score) for s in scores] end +""" + dominated(solution_a::Dict, solution_b::Dict, values::AbstractVector{<:Value})::Bool + +Return whether `solution_a` is Pareto-dominated by `solution_b`: `solution_b` +scores at least as well as `solution_a` on every value in `values` and strictly +better on at least one, comparing `value_score`s. +""" function dominated(solution_a::Dict, solution_b::Dict, values::AbstractVector{<:Value})::Bool better_on_all = true strictly_better_on_one = false @@ -147,6 +222,18 @@ function dominated(solution_a::Dict, solution_b::Dict, values::AbstractVector{<: return better_on_all && strictly_better_on_one end +""" + pareto_frontier(solutions::Vector{<:Dict}, values::AbstractVector{<:Value})::Vector{Dict} + pareto_frontier(system::Dict, values::AbstractVector{<:Value})::Vector{Dict} + +Return the solutions that no other solution dominates on `values` (see +`dominated`), in their original order. + +The `system::Dict` form takes candidate solutions from `system[:solutions]`, or +treats `system` itself as the only candidate. Neither form generates +candidates; it filters the ones supplied. Comparison is pairwise, `O(n²)` in +the number of solutions. +""" function pareto_frontier(solutions::Vector{<:Dict}, values::AbstractVector{<:Value})::Vector{Dict} if isempty(solutions) return eltype(solutions)[] @@ -174,7 +261,7 @@ function pareto_frontier(solutions::Vector{<:Dict}, values::AbstractVector{<:Val end function pareto_frontier(system::Dict, values::AbstractVector{<:Value})::Vector{Dict} - # Generate candidate solutions by exploring the parameter space + # Candidate solutions are supplied by the caller; none are generated here. solutions = Dict[] # If system provides candidate solutions, use them diff --git a/src/types.jl b/src/types.jl index e557ad3..6b20da7 100644 --- a/src/types.jl +++ b/src/types.jl @@ -451,3 +451,17 @@ Prints a concise string representation of a `Safety` object to the given I/O stream. """ Base.show(io::IO, s::Safety) = print(io, "Safety(\"$(s.invariant)\")") + +# Enum variant documentation. Each variant names a metric; the value +# constructors themselves take the plain Symbol (e.g. `:demographic_parity`). +@doc "`FairnessMetric` variant for demographic parity; pass `:demographic_parity` to `Fairness`." demographic_parity_metric +@doc "`FairnessMetric` variant for equalized odds; pass `:equalized_odds` to `Fairness`." equalized_odds_metric +@doc "`FairnessMetric` variant for equal opportunity; pass `:equal_opportunity` to `Fairness`." equal_opportunity_metric +@doc "`FairnessMetric` variant for the disparate-impact ratio; pass `:disparate_impact` to `Fairness`." disparate_impact_metric +@doc "`FairnessMetric` variant for individual fairness; pass `:individual_fairness` to `Fairness`." individual_fairness_metric +@doc "`WelfareMetric` variant for utilitarian (sum) welfare; pass `:utilitarian` to `Welfare`." utilitarian_metric +@doc "`WelfareMetric` variant for Rawlsian (maximin) welfare; pass `:rawlsian` to `Welfare`." rawlsian_metric +@doc "`WelfareMetric` variant for egalitarian (negated variance) welfare; pass `:egalitarian` to `Welfare`." egalitarian_metric +@doc "`EfficiencyMetric` variant for Pareto efficiency; pass `:pareto` to `Efficiency`." pareto_metric +@doc "`EfficiencyMetric` variant for Kaldor-Hicks efficiency; pass `:kaldor_hicks` to `Efficiency`." kaldor_hicks_metric +@doc "`EfficiencyMetric` variant for computation time; pass `:computation_time` to `Efficiency`." computation_time_metric diff --git a/src/welfare.jl b/src/welfare.jl index 1bde665..a0c06dd 100644 --- a/src/welfare.jl +++ b/src/welfare.jl @@ -3,16 +3,38 @@ using Statistics +""" + utilitarian_welfare(utilities::AbstractVector)::Float64 + +Return the utilitarian (Benthamite) social welfare: the sum of individual +utilities. An empty vector has welfare `0.0`. +""" function utilitarian_welfare(utilities::AbstractVector)::Float64 isempty(utilities) && return 0.0 # Return 0.0 for empty utility vector return sum(utilities) end +""" + rawlsian_welfare(utilities::AbstractVector)::Float64 + +Return the Rawlsian (maximin) social welfare: the utility of the worst-off +individual. Raises an error for an empty vector, where no worst-off individual +exists. +""" function rawlsian_welfare(utilities::AbstractVector)::Float64 isempty(utilities) && error("Cannot compute Rawlsian welfare for an empty utility vector.") return minimum(utilities) end +""" + egalitarian_welfare(utilities::AbstractVector{<:Real})::Float64 + +Return an egalitarian welfare score: the negated sample variance of the +utilities, so that more equal distributions score higher and perfect equality +scores `0.0`. Fewer than two individuals score `0.0`. + +This measures equality only; it does not reward higher utility levels. +""" function egalitarian_welfare(utilities::AbstractVector{<:Real})::Float64 if length(utilities) < 2 # Variance of a single element or empty set is undefined or 0 (which is equality). @@ -23,6 +45,25 @@ function egalitarian_welfare(utilities::AbstractVector{<:Real})::Float64 return -var(utilities) end +""" + satisfy(value::Value, state::Dict)::Bool + +Return whether the system state `state` meets the criterion expressed by +`value`. Each `Value` subtype reads its own keys from `state`: + +- `Fairness`: see `satisfy(::Fairness, ::Dict)`. +- `Welfare`: `:utilities` (required); passes when the chosen welfare function is + at least `:min_welfare` (default `0.0`). +- `Profit`: `:profit` (required); passes when it reaches `value.target` and every + `value.constraints` entry is itself satisfied by `state`. +- `Efficiency`: `:computation_time` (`<= target`), `:is_pareto_efficient` + (must be `true`) or `:net_gain` (`>= target`), according to `value.metric`. +- `Safety`: `:is_safe` and `:invariant_holds`. **Both default to `true` when + absent**, so an empty state counts as safe; supply them explicitly. The + `value.invariant` text is descriptive and is not evaluated. + +Missing required keys raise an error. +""" function satisfy(value::Welfare, state::Dict)::Bool utilities = get(state, :utilities, nothing) isnothing(utilities) && error("State must contain :utilities for Welfare satisfaction check.") @@ -42,6 +83,12 @@ function satisfy(value::Welfare, state::Dict)::Bool return computed_welfare >= min_welfare end +""" + satisfy(value::Profit, state::Dict)::Bool + +Return whether `state[:profit]` reaches `value.target` and every constraint in +`value.constraints` is satisfied by the same `state`. +""" function satisfy(value::Profit, state::Dict)::Bool current_profit = get(state, :profit, nothing) # Use nothing to distinguish from actual 0.0 profit isnothing(current_profit) && error("State must contain :profit for Profit satisfaction check.") @@ -55,6 +102,13 @@ function satisfy(value::Profit, state::Dict)::Bool return profit_ok && constraints_ok end +""" + satisfy(value::Efficiency, state::Dict)::Bool + +Return whether `state` meets the efficiency criterion: `:computation_time <= +target`, `:is_pareto_efficient == true`, or `:net_gain >= target`, according to +`value.metric`. +""" function satisfy(value::Efficiency, state::Dict)::Bool if value.metric == :computation_time time = get(state, :computation_time, nothing) @@ -73,6 +127,13 @@ function satisfy(value::Efficiency, state::Dict)::Bool end end +""" + satisfy(value::Safety, state::Dict)::Bool + +Return `state[:is_safe] && state[:invariant_holds]`. Both keys default to +`true` when absent, so an empty state is reported as safe; callers must supply +them. `value.invariant` is not evaluated. +""" function satisfy(value::Safety, state::Dict)::Bool # Check if safety invariant is satisfied in state is_safe = get(state, :is_safe, true) # Optimistic assumption if not provided @@ -81,6 +142,22 @@ function satisfy(value::Safety, state::Dict)::Bool return is_safe && invariant_holds end +""" + maximize(value::Value, initial_state::Dict)::Float64 + +Return the objective that `value` would maximise, evaluated at `initial_state` +(higher is better). This *evaluates* the objective at the given state; it does +not search a configuration space or change the state. + +- `Welfare`: the chosen welfare function of `:utilities`. +- `Profit`: `:profit`. +- `Efficiency`: `-:computation_time`, `1.0`/`0.0` for `:is_pareto_efficient`, + or `:net_gain`. +- `Fairness`: `1 - disparity` for the disparity metrics, the ratio for + `:disparate_impact`; `0.0` when the required data is missing. +- `Safety`: `1.0` when safe, else `0.0` (with the same `true` defaults as + `satisfy(::Safety, ::Dict)`). +""" function maximize(value::Welfare, initial_state::Dict)::Float64 utilities = get(initial_state, :utilities, nothing) isnothing(utilities) && error("initial_state must contain :utilities for Welfare maximization.") @@ -96,12 +173,23 @@ function maximize(value::Welfare, initial_state::Dict)::Float64 end end +""" + maximize(value::Profit, initial_state::Dict)::Float64 + +Return `initial_state[:profit]`. +""" function maximize(value::Profit, initial_state::Dict)::Float64 profit = get(initial_state, :profit, nothing) isnothing(profit) && error("initial_state must contain :profit for Profit maximization.") return profit end +""" + maximize(value::Efficiency, initial_state::Dict)::Float64 + +Return the efficiency objective for `value.metric`: negated computation time, +`1.0`/`0.0` for Pareto efficiency, or the Kaldor-Hicks net gain. +""" function maximize(value::Efficiency, initial_state::Dict)::Float64 if value.metric == :computation_time time = get(initial_state, :computation_time, nothing) @@ -120,6 +208,13 @@ function maximize(value::Efficiency, initial_state::Dict)::Float64 end end +""" + maximize(value::Fairness, initial_state::Dict)::Float64 + +Return a fairness objective where higher is fairer: `1 - disparity` for the +disparity metrics and the ratio itself for `:disparate_impact`. Returns `0.0` +when the data the metric needs is missing. +""" function maximize(value::Fairness, initial_state::Dict)::Float64 # Extract data from state predictions = get(initial_state, :predictions, nothing) @@ -153,13 +248,35 @@ function maximize(value::Fairness, initial_state::Dict)::Float64 end end +""" + maximize(value::Safety, initial_state::Dict)::Float64 + +Return `1.0` when `initial_state` is safe and `0.0` otherwise, with the same +defaults as `satisfy(::Safety, ::Dict)`. +""" function maximize(value::Safety, initial_state::Dict)::Float64 is_safe = get(initial_state, :is_safe, true) invariant_holds = get(initial_state, :invariant_holds, true) return (is_safe && invariant_holds) ? 1.0 : 0.0 end +""" + verify_value(value::Value, proof::Dict)::Bool + +Check a caller-supplied verification *attestation* for `value` and return its +`:verified` flag. + +This function does not run a prover or check a proof. It validates the shape of +the attestation — `proof[:verified]` must be present and a `Bool` — and returns +it. For a critical `Safety` value a positive attestation must also name its +`:prover`; any `:details` are logged. Producing the proof, and trusting it, is +the caller's responsibility. + +When `proof` is a parsed ECHIDNA `echidna.prove.result/1` receipt (it has a +`"schema"` key), the stricter `verify_receipt` is applied instead. +""" function verify_value(value::Value, proof::Dict)::Bool + _is_receipt(proof) && return verify_receipt(value, proof) # Require verified field to be a Bool verified = get(proof, :verified, nothing) isnothing(verified) && error("proof must contain :verified field") @@ -168,7 +285,14 @@ function verify_value(value::Value, proof::Dict)::Bool return verified end +""" + verify_value(value::Safety, proof::Dict)::Bool + +As `verify_value(::Value, ::Dict)`, and additionally require a `:prover` entry +when `value.critical` and the attestation is positive. +""" function verify_value(value::Safety, proof::Dict)::Bool + _is_receipt(proof) && return verify_receipt(value, proof) # Require verified field to be a Bool verified = get(proof, :verified, nothing) isnothing(verified) && error("proof must contain :verified field") @@ -184,9 +308,129 @@ function verify_value(value::Safety, proof::Dict)::Bool # Log prover information if details are available details = get(proof, :details, nothing) if !isnothing(details) - @info "Safety proof from prover: $prover" details + @info "Safety attestation names prover: $prover" details end end return verified end + +""" + PROVE_RESULT_SCHEMA + +The schema identifier of the ECHIDNA prove-result receipt that +`verify_receipt` accepts: `"echidna.prove.result/1"`. +""" +const PROVE_RESULT_SCHEMA = "echidna.prove.result/1" + +# The statuses the /1 schema defines; a new status needs a new schema id. +const _PROVE_STATUSES = ("verified", "failed", "error", "timeout", "unknown") + +""" + _receipt_get(receipt::AbstractDict, key::AbstractString) + +Look `key` up in a parsed receipt whose keys may be `String`s (e.g. JSON.jl) +or `Symbol`s (e.g. JSON3.jl); return `nothing` when it is absent. +""" +_receipt_get(receipt::AbstractDict, key::AbstractString) = + haskey(receipt, key) ? receipt[key] : get(receipt, Symbol(key), nothing) + +""" + _is_receipt(proof::AbstractDict)::Bool + +Return whether `proof` carries a `schema` key and so should be read as a +prove-result receipt rather than a plain `:verified` attestation. +""" +_is_receipt(proof::AbstractDict)::Bool = + haskey(proof, "schema") || haskey(proof, :schema) + +""" + _receipt_field(receipt::AbstractDict, key::AbstractString, T::Type) + +Return the required receipt field `key`, throwing an `ArgumentError` when it +is missing or is not a `T`. +""" +function _receipt_field(receipt::AbstractDict, key::AbstractString, T::Type) + v = _receipt_get(receipt, key) + v isa T || throw(ArgumentError("$(PROVE_RESULT_SCHEMA) receipt field `$(key)` must be a $(T), got $(repr(v))")) + return v +end + +""" + verify_receipt(value::Value, receipt::AbstractDict; + goal::Union{Nothing,AbstractString} = nothing, + allow_axioms = String[])::Bool + +Check a parsed ECHIDNA `echidna.prove.result/1` receipt (the one-line JSON +object printed by `echidna prove --output json`) and return whether it +establishes its goal without unaccepted assumptions. + +The receipt must be well formed under the schema — `schema`, `status` +(`verified`, `failed`, `error`, `timeout` or `unknown`), `prover`, `goal` and +`trust.axioms` — or an `ArgumentError` is thrown; unknown extra fields are +ignored, as the schema requires. The result is `true` only when + +- `status == "verified"` and `prover` is non-empty; +- every entry of `trust.axioms` (axioms and escape hatches such as `sorry`, + `Admitted` or `postulate` that ECHIDNA found) is listed in `allow_axioms`; +- the receipt's `goal` equals `goal`, when `goal` is given. + +Parse the JSON with any parser (`String` or `Symbol` keys both work); this +package does not run ECHIDNA. A receipt is transported evidence that a prover +checked the goal *file*: whether that file states the property `value` +expresses is the caller's claim, and passing `goal` is how that binding is made +explicit. ECHIDNA reports `trust.confidence` as `null` because it checks no +independent certificate; this function does not use it. + +The receipt-versus-warrant reading follows ECHIDNA's +`docs/PROVE-RESULT-CONTRACT.adoc` and the factive/non-factive distinction of +`hyperpolymath/epistemic-types`. +""" +function verify_receipt(value::Value, receipt::AbstractDict; + goal::Union{Nothing,AbstractString} = nothing, + allow_axioms = String[])::Bool + schema = _receipt_get(receipt, "schema") + schema == PROVE_RESULT_SCHEMA || + throw(ArgumentError("not a $(PROVE_RESULT_SCHEMA) receipt (schema = $(repr(schema)))")) + status = _receipt_field(receipt, "status", AbstractString) + status in _PROVE_STATUSES || + throw(ArgumentError("status $(repr(status)) is not defined by $(PROVE_RESULT_SCHEMA)")) + prover = _receipt_field(receipt, "prover", AbstractString) + receipt_goal = _receipt_field(receipt, "goal", AbstractString) + trust = _receipt_field(receipt, "trust", AbstractDict) + axioms = _receipt_field(trust, "axioms", AbstractVector) + all(a -> a isa AbstractString, axioms) || + throw(ArgumentError("$(PROVE_RESULT_SCHEMA) receipt field `trust.axioms` must hold strings")) + + status == "verified" || return false + isempty(prover) && return false + isnothing(goal) || receipt_goal == goal || return false + allowed = Set{String}(String.(allow_axioms)) + return all(a -> String(a) in allowed, axioms) +end + +""" + safety_verdict(value::Safety, state::Dict)::Symbol + +Return a three-valued verdict on `value` for `state`: + +- `:refuted` when `state[:is_safe]` or `state[:invariant_holds]` is `false`; +- `:entailed` when both are present and `true`; +- `:unresolved` otherwise — the evidence is missing, so safety is neither + established nor ruled out. + +Unlike `satisfy(::Safety, ::Dict)`, which treats absent keys as safe, this keeps +missing evidence visible. Non-`Bool` values throw an `ArgumentError`. The verdict +names follow `hyperpolymath/ResidualEvidenceTypes.jl` (`ENTAILED` / `REFUTED` / +`UNRESOLVED`); this package does not depend on it. +""" +function safety_verdict(value::Safety, state::Dict)::Symbol + flags = (get(state, :is_safe, nothing), get(state, :invariant_holds, nothing)) + for f in flags + isnothing(f) || f isa Bool || + throw(ArgumentError("Safety evidence (:is_safe, :invariant_holds) must be Bool, got $(repr(f))")) + end + any(f -> f === false, flags) && return :refuted + all(f -> f === true, flags) && return :entailed + return :unresolved +end diff --git a/test/hardening.jl b/test/hardening.jl new file mode 100644 index 0000000..a53923d --- /dev/null +++ b/test/hardening.jl @@ -0,0 +1,123 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell + +# Regression tests for undefined scores, the :protected_attributes alias, +# and public-API documentation coverage. + +@testset "Hardening" begin + @testset "Zero-target scores throw instead of returning Inf/NaN" begin + @test_throws ArgumentError value_score(Profit(), Dict(:profit => 100.0)) + @test_throws ArgumentError value_score(Profit(target = 0.0), Dict(:profit => 0.0)) + @test_throws ArgumentError value_score(Efficiency(metric = :kaldor_hicks, target = 0.0), + Dict(:net_gain => 1.0)) + @test_throws ArgumentError value_score(Efficiency(metric = :computation_time, target = 0.0), + Dict(:computation_time => 1.0)) + @test_throws ArgumentError weighted_score(Value[Profit()], Dict(:profit => 100.0)) + # satisfy is unaffected: a zero profit target is a meaningful floor. + @test satisfy(Profit(), Dict(:profit => 100.0)) + end + + @testset "Zero fairness threshold demands exact parity" begin + f = Fairness(metric = :demographic_parity, threshold = 0.0) + parity = Dict(:predictions => [1, 0, 1, 0], :protected => [:a, :a, :b, :b]) + skewed = Dict(:predictions => [1, 1, 1, 0], :protected => [:a, :a, :b, :b]) + @test value_score(f, parity) == 1.0 + @test value_score(f, skewed) == 0.0 + @test !isnan(weighted_score(Value[f], parity)) + end + + @testset "value_score accepts :protected_attributes like satisfy does" begin + f = Fairness(metric = :demographic_parity, threshold = 0.5) + a = Dict(:predictions => [1, 1, 1, 0], :protected => [:a, :a, :b, :b]) + b = Dict(:predictions => [1, 1, 1, 0], :protected_attributes => [:a, :a, :b, :b]) + @test value_score(f, a) == value_score(f, b) == 0.0 + @test satisfy(f, a) == satisfy(f, b) + end + + @testset "Every exported name is documented" begin + # Base.Docs.hasdoc only exists from Julia 1.11; the docs registry + # (Base.Docs.meta) answers the same question on every supported version. + docs = Base.Docs.meta(Axiology) + undocumented = [n for n in names(Axiology) + if n !== :Axiology && !haskey(docs, Base.Docs.Binding(Axiology, n))] + @test isempty(undocumented) + # Positive control: the check must be able to see a missing docstring. + @test !haskey(docs, Base.Docs.Binding(Axiology, :_no_such_binding)) + end + + @testset "ECHIDNA prove-result receipts" begin + s = Safety(invariant = "no harmful recommendations", critical = true) + # The documented example object from echidna docs/PROVE-RESULT-CONTRACT.adoc. + ok() = Dict{String,Any}("duration_ms" => 1, "echidna_version" => "x", + "goal" => "ok.twasm", "message" => "PROVED in 0ms", + "prover" => "TypedWasm", "schema" => PROVE_RESULT_SCHEMA, + "status" => "verified", + "trust" => Dict{String,Any}("axioms" => Any[], "confidence" => nothing)) + @test verify_receipt(s, ok()) + @test verify_value(s, ok()) # dispatches to the receipt check + @test verify_receipt(s, ok(); goal = "ok.twasm") + @test !verify_receipt(s, ok(); goal = "other.lean") + for st in ("failed", "error", "timeout", "unknown") + r = ok(); r["status"] = st + @test !verify_receipt(s, r) + end + r = ok(); r["prover"] = "" + @test !verify_receipt(s, r) + r = ok(); r["trust"]["axioms"] = Any["sorry"] + @test !verify_receipt(s, r) + @test verify_receipt(s, r; allow_axioms = ["sorry"]) + # Symbol-keyed parses (e.g. JSON3) are read the same way. + sym = Dict{Symbol,Any}(Symbol(k) => v for (k, v) in ok()) + sym[:trust] = Dict{Symbol,Any}(:axioms => Any[], :confidence => nothing) + @test verify_receipt(s, sym) + # Malformed receipts are rejected, not read as failures. + r = ok(); r["schema"] = "echidna.prove.result/2" + @test_throws ArgumentError verify_receipt(s, r) + r = ok(); r["status"] = "proved" + @test_throws ArgumentError verify_receipt(s, r) + r = ok(); delete!(r, "goal") + @test_throws ArgumentError verify_receipt(s, r) + r = ok(); r["trust"] = Dict{String,Any}("axioms" => "sorry") + @test_throws ArgumentError verify_receipt(s, r) + r = ok(); r["unexpected_future_field"] = 42 # unknown fields are ignored + @test verify_receipt(s, r) + # Plain attestations keep their old meaning. + @test verify_value(Welfare(), Dict(:verified => true)) + end + + @testset "safety_verdict keeps missing evidence visible" begin + s = Safety(invariant = "test") + @test safety_verdict(s, Dict()) === :unresolved + @test safety_verdict(s, Dict(:is_safe => true)) === :unresolved + @test safety_verdict(s, Dict(:is_safe => true, :invariant_holds => true)) === :entailed + @test safety_verdict(s, Dict(:is_safe => false)) === :refuted + @test safety_verdict(s, Dict(:is_safe => true, :invariant_holds => false)) === :refuted + @test_throws ArgumentError safety_verdict(s, Dict(:is_safe => 1)) + @test satisfy(s, Dict()) # unchanged: absent keys count as safe + end + + @testset "weighted_score is lossy (distinct profiles, same score)" begin + values = Value[Efficiency(metric = :pareto, weight = 1.0), + Safety(invariant = "test", weight = 1.0)] + a = Dict(:is_pareto_efficient => true, :is_safe => false) + b = Dict(:is_pareto_efficient => false, :is_safe => true) + @test [value_score(v, a) for v in values] != [value_score(v, b) for v in values] + @test weighted_score(values, a) == weighted_score(values, b) == 0.5 + # ...and the Pareto comparison still tells them apart: neither dominates. + @test !dominated(a, b, values) && !dominated(b, a, values) + end + + @testset "Module docstring example holds" begin + fairness = Fairness(metric = :demographic_parity, protected_attributes = [:group], + threshold = 0.05) + state = Dict(:predictions => [1, 0, 1, 1, 0, 1], :protected => [:a, :a, :b, :b, :b, :a]) + @test satisfy(fairness, state) + values = [Welfare(metric = :utilitarian, weight = 0.5), + Fairness(metric = :demographic_parity, threshold = 0.1, weight = 0.5)] + candidates = [ + Dict(:utilities => [3.0, 3.0], :predictions => [1, 1], :protected => [:a, :b]), + Dict(:utilities => [9.0, 0.0], :predictions => [1, 0], :protected => [:a, :b]), + ] + @test length(pareto_frontier(candidates, values)) == 2 + end +end diff --git a/test/runtests.jl b/test/runtests.jl index ed2b69e..e9fbc0a 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -823,8 +823,8 @@ using Axiology @testset "Critical safety with prover and details" begin s = Safety(invariant="test", critical=true) - proof = Dict(:verified => true, :prover => :Lean, :details => "Formally verified") - @test verify_value(s, proof) + proof = Dict(:verified => true, :prover => :Lean, :details => "attestation from an external prover") + @test (@test_logs (:info, r"names prover") verify_value(s, proof)) end @testset "Non-critical safety does not require prover" begin @@ -958,3 +958,5 @@ using Axiology @test Safety <: Value end end + +include("hardening.jl") diff --git a/test_load.jl b/test_load.jl deleted file mode 100644 index 6965e09..0000000 --- a/test_load.jl +++ /dev/null @@ -1,19 +0,0 @@ -# Test loading fairness.jl -using Statistics - -println("About to include fairness.jl...") -try - include("src/fairness.jl") - println("SUCCESS: fairness.jl loaded") -catch e - println("ERROR loading fairness.jl:") - showerror(stdout, e, catch_backtrace()) - println() - - # Try to get more details - println("\nChecking line 30:") - lines = readlines("src/fairness.jl") - for i in 28:32 - println("Line $i: ", repr(lines[i])) - end -end