Run a first solver

This example runs Online Mirror Descent on the built-in Left/Right environment. Complete the installation first, then run commands from the LeanMFG checkout.

Run from the command line

lake exe mfglib left_right omd 20

The arguments select the environment, algorithm, and maximum iteration count. The command writes a JSON object with these fields:

Field	Meaning
`environment`	Name of the selected environment
`shape`	Policy dimensions: time, state, action
`bestIndex`	Index of the smallest recorded exploitability
`result.policies`	Initial policy followed by each computed policy
`result.exploitabilities`	Exploitability for each stored policy
`result.runtimes`	Elapsed seconds at each iteration
`result.stoppedEarly`	Whether the stopping tolerance was reached

The default stopping tolerance can end a run before iteration 20. SolveOptions describes the stopping rule.

Call the solver from Lean

The following program disables early stopping, runs 20 updates, and inspects the best recorded policy. The initial policy is uniform because the pi0 argument is none.

Solve.lean

import LeanMFG.Computational

open LeanMFG.Computational

def main : IO Unit := do
  let env := Environments.leftRight
  let .ok result ← (OnlineMirrorDescent.solve { alpha := 0.2 } env none
    { maxIter := 20, atol := none, rtol := none }).run
    | throw (IO.userError "solver failed")
  let best := result.bestIndex
  IO.println s!"Policy shape: {env.policyShape}"
  IO.println s!"Stored policies: {result.policies.size}"
  IO.println s!"Initial exploitability: {result.exploitabilities[0]!}"
  IO.println s!"Best iteration: {best}"
  IO.println s!"Best exploitability: {result.exploitabilities[best]!}"

Run the same file with:

lake env lean --run docs/examples/Solve.lean

Output:

text

Policy shape: #[2, 3, 2]
Stored policies: 21
Initial exploitability: 0.250000
Best iteration: 20
Best exploitability: 0.008187

The result contains 21 policies: the initial policy and 20 updates. result.policies[result.bestIndex]! selects the policy with the lowest recorded score. The solver reference describes the result type and error cases.

Interpret exploitability

For a policy $\pi$ , the library first computes its population flow. It then holds that flow fixed and compares the best-response value with the value of $\pi$ . The difference is the exploitability score.

A smaller score indicates a smaller estimated gain from a unilateral deviation. This numerical score is computed in binary64 arithmetic; the solver does not return a proved equilibrium certificate. See verification and tests for the current guarantees.

Change the environment or algorithm

lake exe mfglib --list
lake exe mfglib susceptible_infected fp 10

The algorithm names are fp, omd, pd, mfomo, and omi. For constructor parameters and saved configurations, see the finite-horizon guide.