Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Algorithmic Game Theory

427 missions · 182 completed

Missions

Completed

Machine Learning Operations Research Optimization·Captain: mikedeng1

Optimal Decision Making Under Strategic Behavior 3: A Three-Value Instance with General Costs Where No Optimal Policy Is Outcome MonotonicResearch Paper

Motivation

When a decision rule is announced in advance, people may change the features on which the rule acts. A lender, for example, may offer loans with different probabilities to applicants with different reported characteristics. An applicant then weighs the greater chance of receiving a loan against the cost of changing those characteristics. The decision maker must account for this response when choosing the rule. Tsirtsis and coauthors study this problem with a finite feature set and a policy that specifies the probability of a positive decision at each value.

If moving to a better-outcome feature costs more and moving to a worse-outcome feature costs nothing, the paper shows that at least one optimal policy can be chosen to respect the ordering of outcomes. Section 5 asks what remains of that conclusion when change costs are general. Its three-value example answers the question sharply: an optimal policy exists, but no optimal policy respects outcome monotonicity. The example isolates the role played by the cost assumption in the earlier result. Source, §§4–5

Setting

There are $m$ feature values $x_1,\ldots,x_m$ . An individual initially has value $x_i$ with probability $p(x_i)=P(x_i)$ . At feature value $x_j$ , the probability of a positive underlying outcome is $q(x_j)=P(y=1\mid x_j)$ . A decision policy $\pi$ assigns a positive-decision probability $\pi(x_j)\in[0,1]$ to each value. The decision maker incurs a cost $\gamma\in(0,1)$ for a positive decision. This is the paper's base model: the individual benefit is $b(x)=\pi(x)$ , and the outcome probability $P(y\mid x)$ does not change when an individual changes features. Source, §2, p. 3, equations (1)–(3)

An individual at $x_i$ may move to $x_j$ , paying change cost $c(x_i,x_j)$ . Their best response maximizes $\pi(x_j)-c(x_i,x_j)$ over all destinations. If several destinations tie, the paper selects one with the highest outcome probability $q(x_j)$ . The resulting population distribution depends on $\pi$ . The decision maker's strategic utility is the expected outcome surplus under that response:

u_{p,q,\gamma,c}(\pi)=\sum_{i=1}^{m}p(x_i) \bigl(q(\operatorname{br}_{c,q,\pi}(x_i))-\gamma\bigr) \pi(\operatorname{br}_{c,q,\pi}(x_i)).

This sum is equation (7) regrouped by each individual's initial value. An optimal policy maximizes it over every policy in $[0,1]^m$ . The paper assumes a positive cost for moving to a distinct feature whose outcome is at least as good as the starting feature; its Section 5 matrix meets that assumption. Source, §3, pp. 4–5, equations (5) and (7)

The example has $m=3$ , $\gamma=0.1$ , $p=(0.1,0.4,0.5)$ , and $q=(1,0.7,0.4)$ . Rows of the following matrix are starting features and columns are destinations:

c=\begin{pmatrix} 0&0.2&0.3\\ 0.3&0&0.7\\ 1.2&1.1&0 \end{pmatrix}.

Moving from $x_1$ to the lower-outcome $x_2$ costs $0.2$ . That violates the zero-cost requirement for such moves in the paper's outcome monotonic cost definition. A policy is called outcome monotonic here when a larger positive-decision probability implies a larger outcome probability: $\pi(x_i)<\pi(x_j)\Rightarrow q(x_i)<q(x_j)$ . Source, §§2, 4–5, pp. 3, 6, 9

Formalization targets

The printed optimal family

For every admissible policy $\pi$ with $\pi(x_1)=1$ , $\pi(x_2)\leq0.7$ , and $\pi(x_3)=1$ , the paper states that $\pi$ is optimal and that individuals initially at $x_2$ move to $x_1$ :

\forall\pi\in[0,1]^3, \quad\bigl(\pi(x_1)=1\land\pi(x_2)\leq0.7\land\pi(x_3)=1\bigr) \Longrightarrow \bigl(\pi\text{ is optimal}\land\operatorname{br}_{c,q,\pi}(x_2)=x_1\bigr).

The endpoint $\pi(x_2)=0.7$ matters: the move from $x_2$ to $x_1$ ties with staying in benefit less cost, and the paper's outcome tie rule chooses $x_1$ . Source, §5, p. 9

Goal: no outcome monotonic optimum

The principal target formalizes the Section 5 heading in this fixed instance:

\exists\pi\in[0,1]^3:\pi\text{ is optimal}, \qquad \forall\pi\in[0,1]^3:\pi\text{ is optimal}\Longrightarrow \neg\operatorname{OMPolicy}(q,\pi).

The existence clause rules out an empty optimal set. This formulation follows the heading's assertion that an outcome-monotonic optimum may fail to exist, while the printed family supplies concrete optima. Source, §5, p. 9

Significance

The result gives an explicit boundary for the earlier outcome-monotonic-policy guarantee. With the Section 5 costs, favoring the lowest-outcome value $x_3$ as much as the highest-outcome value $x_1$ can be optimal, because the response to a published policy changes where population mass receives decisions. Thus a search restricted to outcome-monotonic policies can miss every optimum in a general-cost instance. The milestone on the printed family records a full interval of optimal policies, including its tie endpoint. Source, §§4–5, pp. 6, 9

The paper proves its example informally; this mission asks for a machine-checked account of the fixed instance and the universal quantifiers behind “every” and “no.” The development also yields reusable definitions for finite strategic policies, the outcome-aware best response, and utility. The other missions in this series treat the additive-cost theorem and a stochastic-optimum example separately. No theorem in this mission is presented as an open research problem.

Difficulty

Checking that one displayed policy has high utility is insufficient to establish optimality over every policy in $[0,1]^3$ . The best response changes at equality thresholds, so utility is piecewise defined and may jump when the tie rule changes the destination. The closed bound $\pi(x_2)\leq0.7$ makes one such threshold part of the statement. A finite numerical grid misses both arbitrary real policies and the exact tie behavior. The negative goal also requires excluding outcome monotonicity for every maximizer, rather than exhibiting one nonmonotonic maximizer.

Formalization scope

The features are Fin 3 in the example, with Lean indices $0,1,2$ representing $x_1,x_2,x_3$ . The general model uses Fin m with a nonempty finite feature set. Probabilities, costs, and utility are real numbers; the example's decimals are exact rational reals. Policies range over all real-valued functions with each coordinate in $[0,1]$ , and optimality uses IsMaxOn on precisely that set. The best response is constructed from the maximizers of $\pi(x_j)-c(x_i,x_j)$ and then the largest $q(x_j)$ . If tied destinations also have equal $q$ , the least index is chosen; the example has distinct outcome probabilities, so this final convention never affects its claims.

Equation (1) prints strict outcome and policy comparisons as a biconditional, although the paper's later policy class permits equal policy values at distinct outcomes. This mission uses its one-way implication from a strict policy comparison to a strict outcome comparison. Failure of this weaker condition is a stronger counterexample than failure of the printed biconditional. The cost definition applies its printed pair and triple comparisons only to distinct values and records $c(x_i,x_i)=0$ , as required for free staying. The example's constants satisfy the paper's standing positive-upward-cost assumption. These readings are disclosed so the formal claim has a consistent, nonvacuous model.

A complete proof needs finite argmax reasoning, exact rational inequalities, a case analysis over real policy regions, and the semantics of IsMaxOn. The finite best-response and utility definitions can be reused for other strategic-decision instances. Contributions may establish the printed family, its transport claim, bounds for all admissible policies, or the final exclusion of monotonic maximizers. Policies are never restricted to a grid, and the best response is computed from the model data rather than supplied as a free variable. The paper's algorithms, complexity claims, empirical studies, and changes to $P(y\mid x)$ are outside this mission.

Selected references

S. Tsirtsis, B. Tabibian, M. Khajehnejad, A. Singla, B. Schölkopf, and M. Gomez-Rodriguez, Optimal Decision Making Under Strategic Behavior, Management Science, 2024. arXiv:1905.09239v5, the source version used here.

7 thms0 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

Cross-licensing in a Supply Chain with Asymmetric Manufacturers III: When the Supplier Prefers to Commit to Cross-Licensing Ex AnteResearch Paper

Motivation

A component supplier may ask two downstream manufacturers to license their improvements to each other. Sharing raises each product's quality, but it can also reduce a manufacturer's reason to invest in its own improvement. The supplier must choose the licensing rule before those investments and before setting the wholesale price. Wang, Huang, and Lee study this choice in a two-manufacturer supply chain with unequal innovation costs. Their 2023 manuscript identifies cost regions in which the supplier gains from committing to cross-licensing and a region in which the choice depends on a further threshold. The question matters whenever a shared component provider controls a contract that changes both downstream competition and the incentive to improve products.

This mission targets Proposition 4 of the authors' SSRN manuscript, version of 2023-04-27. The appendix of that manuscript contains the proof and the explicit equilibrium formulas used here. The manuscript was later published in Manufacturing & Service Operations Management; the theorem and page labels in this mission belong to the held SSRN version.

Setting

There is one supplier and two manufacturers, $M_1$ and $M_2$ . Manufacturer $i$ invests at innovation level $T_i\ge0$ and pays the quadratic cost $k_iT_i^2$ . Manufacturer 2 has the lower innovation cost: $49/144<k_2<k_1$ . If the manufacturers cross-license with effectiveness $\beta\in[0,1]$ , the quality improvements of their products are $T_1+\beta T_2$ and $T_2+\beta T_1$ . Without cross-licensing the same model uses $\beta=0$ . The market-size intercept is normalized to one and unit production costs to zero, as in Section 3 of the manuscript.

After investment, the supplier selects a nonnegative wholesale price $r$ . The manufacturers then choose nonnegative Cournot quantities $q_1,q_2$ . Manufacturer $i$ 's selling price is $1+T_i+\beta T_j-q_i-q_j$ , and its operating profit is $(1+T_i+\beta T_j-q_i-q_j-r)q_i$ . The supplier receives $r(q_1+q_2)$ . A downstream duopoly has both quantities positive; at a downstream monopoly, only one manufacturer produces. The paper solves this sequence backward and distinguishes two equilibrium investment patterns within the duopoly: an interior outcome $T^I$ and a boundary outcome $T^B$ . Their dividing cost is $\hat k_2(k_1\mid\beta)$ . The paper's named innovation outcome is $T^B$ for $k_2<\hat k_2(k_1\mid\beta)$ and $T^I$ otherwise.

Write $P(k_2,\beta)$ for the supplier's optimal wholesale revenue at that named innovation outcome. Thus $P(k_2,0)$ is the same downstream model with no licensing. The choice to commit to cross-licensing is determined by comparing these two revenues.

Formalization targets

The three cost regions

Proposition 4 divides admissible $k_2$ into three regions. In the boundary region, licensing weakly benefits the supplier:

k_2<\hat k_2(k_1\mid\beta)\quad\Longrightarrow\quad P(k_2,0)\le P(k_2,\beta).

The threshold $\hat k_2(k_1\mid\beta)$ decreases as $\beta$ rises, and this boundary region eventually has no admissible $k_2$ . In the middle region there is a single threshold $\tilde k_2$ , fixed by $k_1$ and $\beta$ , below which the supplier weakly prefers licensing:

\hat k_2(k_1\mid\beta)\le k_2<\hat k_2(k_1\mid0):\qquad P(k_2,0)\le P(k_2,\beta)\ \Longleftrightarrow\ k_2\le\tilde k_2.

In the third region the direction of the threshold reverses. For a threshold $\underline k_2$ fixed by $k_1$ and $\beta$ ,

k_2\ge\hat k_2(k_1\mid0):\qquad P(k_2,0)\le P(k_2,\beta)\ \Longleftrightarrow\ \underline k_2\le k_2.

When $\beta\ge2/5$ , $P(k_2,\beta)\le P(k_2,0)$ throughout that last region. All three displays are restricted to $49/144<k_2<k_1$ . The full proposition is the mission goal. The milestone list records the paper's threshold monotonicity, the two explicit supplier-profit formulas, and the cost-region facts used to state the comparison.

Significance

The result makes the supplier's contract decision depend on both innovation asymmetry and the effectiveness of sharing. It separates the direct benefit of higher quality from the loss associated with weaker investment incentives. In particular, the supplier can benefit from cross-licensing when the superior manufacturer's cost is low enough for a boundary investment outcome, yet full effectiveness does not make licensing uniformly attractive. These conclusions are specific to the supplier's choice before investment; the paper's earlier ex post comparison holds the innovations fixed and addresses a different decision.

The mathematical result is already proved in the authors' appendix. The work here is to formalize its exact conditions and the optimization value being compared, then obtain a machine-checked proof. A development can reuse the Cournot quantity response, wholesale-price optimization, and piecewise investment formulas for the paper's later welfare and manufacturer-profit results. The local draft theorem statements compile in Lean; the results themselves remain open proof obligations.

Difficulty

The supplier's price can change which manufacturers remain active, and the manufacturers choose investments while anticipating that price response. A simple comparison of demand intercepts at fixed investments therefore does not decide the initial contract: the investments on the two sides of the comparison can differ, and a cost change can move one side across the boundary between the two equilibrium regimes. The paper expresses the outcomes with rational functions containing $\sqrt3$ and analyzes three regions separated by $\hat k_2(k_1\mid\beta)$ and $\hat k_2(k_1\mid0)$ . A faithful formalization must also preserve the order of quantifiers: each single-crossing threshold is chosen once for fixed $k_1,\beta$ , before $k_2$ ranges over its region.

Formalization scope

The Lean model uses real parameters and explicit pairs ordered as $M_1,M_2$ . It encodes the paper's displayed quantity formula for $T_2\ge T_1$ , with $q_i,T_i,r\ge0$ and $0\le\beta\le1$ . Its standing cost condition is $49/144<k_2<k_1$ . The wholesale-price domain $r\ge0$ makes explicit the economic domain implicit in the manuscript. The two displayed investment formulas use Real.sqrt 3; no decimal approximation enters a statement. The named innovation outcome follows page A.2: boundary below $\hat k_2$ , interior otherwise. A separate mission targets its Nash-equilibrium characterization.

Most importantly, the supplier's optimal profit is the supremum of actual revenue over nonnegative prices at that innovation outcome. It is not defined to equal either closed form; a milestone asserts that the maximum is attained and identifies its value. This prevents the preference theorem from becoming a comparison true only by definition. The $\tilde k_2$ and $\underline k_2$ thresholds are existential single-crossing statements because the latter's printed formula on page A.3 is malformed. The proof's weak profit comparisons determine the formal inequality. At $\beta\ge2/5$ , the statement uses interior profit on both sides, correcting an apparent $\pi_s^B(\beta)$ slip in the final sentence of the proof.

Useful contributions include a proof of the attained supplier optimum, denominator positivity over the standing domain, exact inequalities involving $\sqrt3$ , and the two single-crossing results. The general price-optimization facts and market-response lemmas can be reused beyond this mission.

Selected references

J. Wang, T. Huang, and J. Lee, Cross-licensing in a Supply Chain with Asymmetric Manufacturers, SSRN manuscript 3053682, version of 2023-04-27, Proposition 4 and Appendix A.1–A.3. SSRN.
J. Wang, T. Huang, and J. Lee, Cross-licensing in a Supply Chain with Asymmetric Manufacturers, Manufacturing & Service Operations Management, 2023. DOI: 10.1287/msom.2019.0477.

8 thms0 active usersReviewed