Optimization under uncertainty: understanding orders and testing programs with specifications

1. Problem Statement

The paper addresses the fundamental challenge of optimization under uncertainty, a ubiquitous problem in engineering, economics, climate science, and machine learning. Standard optimization seeks to find elements in a finite set $A$ that minimize a function $f: A \to B$, where $B$ is equipped with a total order (e.g., real numbers).

However, real-world decision-making often violates the assumption of a single, totally ordered objective value due to two distinct types of uncertainty:

1. Value Uncertainty (Multi-Objective): The objective function returns a vector of values (e.g., cost vs. safety) where no single total order exists. Instead, a partial order applies, leading to sets of incomparable "Pareto optimal" solutions rather than a single best value.
2. Functorial Uncertainty: The function $f$ does not return a single value but a set of possible outcomes, a probability distribution, or an interval (modeled as $f: A \to U B$, where $U$ is an uncertainty functor). Comparing these uncertain values requires defining appropriate order relations on $U B$ and selecting measure functions (e.g., expected value, worst-case) to guide the minimization.

The core problem is that existing methods often rely on ad-hoc assumptions (like risk-neutrality via expected value) or lack formal specifications, making it difficult to verify correctness, test robustness, or understand the implications of different order relations.

2. Methodology

The authors employ Functional Programming (FP) as a rigorous framework for specification, implementation, and testing. They utilize Haskell to define generic algorithms and QuickCheck for property-based testing.

A. Formalizing Orders

• Total Order Baseline: They establish a baseline for single-objective minimization using min and argmin, defined by three properties: the result is a minimum value, the result is in the image of the function, and all elements achieving the minimum are returned.
• Partial Orders (Value Uncertainty): For multi-objective optimization (MOO), they define a dominance relation ($\prec$) on vectors. A solution is Pareto optimal if it is not dominated by any other solution. They introduce a "thinning" algorithm (bump) to compute the Pareto front incrementally.
• Functorial Orders: For uncertainty functors ($U$), they define a strict partial order ($\prec_u$) based on universal strict dominance: $ub_1 \prec_u ub_2$ if every outcome in $ub_1$ is strictly better than every outcome in $ub_2$.

B. Measure Functions and Monotonicity

To minimize $f: A \to U B$, a measure function $\mu: U B \to C$ (where $C$ is totally ordered) is required to rank uncertain values. The authors investigate which properties $\mu$ must satisfy to ensure the optimization is "sound" (i.e., does not return a solution strictly dominated by another available option).

• Pointwise Monotonicity (M1): If elements in a structure increase, the measure should not decrease.
• Structural Monotonicity (M2): If $ub_1 \prec_u ub_2$ (structurally strictly better), then $\mu(ub_1) < \mu(ub_2)$.
• Key Finding: The authors prove that M2 is the necessary and sufficient condition for soundness. Common measures like "length" or constant functions satisfy M1 but fail M2, leading to incorrect optimization results. Measures like sum, average, or worst-case satisfy M2.

C. Testing and Verification

Instead of relying on benchmarking against specific datasets, the authors use property-based testing. They generate random inputs and verify that the implemented algorithms satisfy the formal mathematical specifications (e.g., prop1.1, prop2.4, test3.1). This approach allows for the systematic validation of generic algorithms across different types of uncertainty functors (Lists, Probabilities, Intervals, PDFs).

3. Key Contributions

1. Unified Framework for Uncertainty: The paper provides a generic, type-class-based framework that unifies multi-objective optimization (value uncertainty) and stochastic/epistemic optimization (functorial uncertainty) under a single functional paradigm.
2. Formal Characterization of Measure Functions: It rigorously derives and proves that Structural Monotonicity (M2) is the critical property for measure functions in optimization under uncertainty. This clarifies why standard approaches (like using expected value without checking dominance) can fail in specific contexts.
3. Generic Algorithms:
   • A generic paretoOpt algorithm for computing Pareto fronts using a bump function.
   • Generic minu and argminu functions that accept a measure function and an uncertainty functor, returning sets of optimal uncertain values.
4. Specification-Driven Development: The paper demonstrates how functional programming allows for the precise specification of optimization problems. The code is the specification, and QuickCheck tests serve as the proof of correctness for the implementation logic.
5. Uncertainty Functors: They propose a formal definition of "Uncertainty Functors" as functors that preserve decidable equality and support a zip operation, linking optimization theory to category theory concepts (Traversable functors).

4. Results

• Multi-Objective Optimization: The authors successfully implemented and tested a generic Pareto front calculator. They demonstrated its application on a standard benchmark problem (minimizing two conflicting functions over a 2D control space), showing how sampling and evolutionary strategies can approximate the Pareto front.
• Functorial Optimization: Through extensive QuickCheck testing, they showed that:
  • Measures satisfying only M1 (e.g., constant functions, list length) fail to produce sound results, often returning dominated solutions.
  • Measures satisfying M2 (e.g., sum, expected value, worst-case) consistently satisfy the soundness specifications.
  • The framework works across different functors: Id (deterministic), List (non-deterministic), SP (Simple Probability), I (Intervals), and PDF (Histograms).
• Climate Policy Application: The paper illustrates how different risk attitudes (best-case vs. worst-case measures) lead to different Pareto fronts in climate policy models. This highlights that "optimal" policies are not absolute but depend on the chosen measure function, explaining why stakeholders with the same data may disagree on policy.

5. Significance

• Pedagogical and Practical Clarity: The paper moves optimization under uncertainty away from "black box" heuristics toward transparent, mathematically grounded methods. It clarifies which order relations are appropriate for specific uncertainty types.
• Trustworthy Software: By emphasizing formal specifications and property-based testing, the work offers a path to building more reliable optimization software for critical domains like climate policy and engineering control.
• Decision-Making Insight: It provides a formal mechanism to analyze the impact of risk attitudes. It shows that disagreements in policy (e.g., climate change mitigation) often stem from implicit differences in how uncertainty is measured (e.g., expected value vs. worst-case), rather than a lack of scientific data.
• Future Verification: The authors note that these specifications are suitable for formal verification in dependently typed languages (like Agda or Idris), paving the way for mathematically proven optimization libraries.

In summary, the paper argues that understanding orders is the key to solving optimization under uncertainty. By rigorously defining the relationship between uncertainty structures, dominance relations, and measure functions, the authors provide a robust, testable, and generic toolkit for handling complex decision problems.