Théorie de la Décision Bayésienne (Infer.NET)

← Série Probas | ↑ Arc Théorie de la Décision | Corpus bayésien Infer (C#) → | Lake Lean decision_theory_lean →

Arc autonome de théorie de la décision bayésienne en Infer.NET : les notebooks 1-10 et l’accrétion Lean 2b prolongent la modélisation probabiliste (le corpus bayésien ../../Infer/) jusqu’au choix d’action sous incertitude. Un posterior n’est pas une fin — c’est l’input d’une politique optimale. Cette série formalise ce passage, de l’utilité espérée aux processus markoviens, jusqu’à la preuve formelle Lean 4 de l’indice de Gittins.

Prérequis : le corpus bayésien ../../Infer/ (notamment Infer-4-Bayesian-Networks, Infer-7-Skills-IRT pour les posteriors Beta). Aucun prérequis en théorie de la décision : les axiomes de Von Neumann-Morgenstern sont introduits ex nihilo.

Stack : Infer.NET (.NET 9.0 + dotnet-interactive), EP/VMP par défaut. Les notebooks companions (2, 2b, 8b) utilisent le kernel Lean 4 (WSL) et le lake decision_theory_lean.

Pourquoi un arc autonome

Jusqu’à la restructuration de la série, la théorie de la décision était imbriquée dans le corpus bayésien Infer, ce qui masquait la dualité des deux fils : modéliser l’incertitude (inférence bayésienne) vs décider face à l’incertitude (théorie de la décision). L’extraction dans DecisionTheory/DecInfer/ rend ces deux arcs physiquement indépendants tout en préservant le continuum pédagogique (le fil décision s’appuie sur les posteriors du corpus bayésien). Le lake decision_theory_lean, à la racine de la série Probas, reste visible des deux pistes (Infer.NET et PyMC).

Vue d’ensemble

#	Notebook	Durée	Concepts
1	DecInfer-01-Utility-Foundations	50 min	Loteries, axiomes VNM, utilité espérée
2	DecInfer-02-Lean-ExpectedUtility	45 min	Companion natif (kernel Lean) : preuve formelle 0-sorry de la direction sound du théorème vNM dans le lake `decision_theory_lean`
2b	DecInfer-02b-Lean-Coherence	20 min	Companion natif (kernel Lean) : cohérence de de Finetti — Dutch Book à quatre tickets, caractérisation mono-livret ⟺ bornes de probabilité (lib `Coherence`)
3	DecInfer-03-Utility-Money	45 min	Paradoxe St-Petersbourg, CARA, CRRA
4	DecInfer-04-Multi-Attribute	50 min	MAUT, SMART, swing weights
5	DecInfer-05-Decision-Networks	55 min	Diagrammes d’influence, politique optimale
6	DecInfer-06-Value-Information	45 min	EVPI, EVSI, valeur de l’information
7	DecInfer-07-Expert-Systems	50 min	Systèmes experts, Minimax, regret
8	DecInfer-08-Sequential	60 min	MDPs, itération valeur/politique
08b	DecInfer-08b-Lean-Gittins	45 min	Preuves formelles Lean 4, indice de Gittins, SFABP
10	DecInfer-10-Thompson-Sampling	60 min	Thompson Sampling bayésien, posterior Beta-Bernoulli par le moteur, regret vs ε-greedy/UCB1

Durée totale : ~8h

Progression Pédagogique

flowchart TD
    A["<b>Fondations</b> (1-3)<br/>axiomes vNM · utilité de l'argent<br/>aversion au risque"]
    B["<b>Multi-attributs & réseaux</b> (4-5)<br/>MAUT · diagrammes d'influence"]
    C["<b>Valeur & robustesse</b> (6-7)<br/>EVPI/EVSI · Minimax/regret"]
    D["<b>Séquentiel</b> (8)<br/>MDPs · Bellman"]
    E["<b>Preuve & bandits</b> (9-10)<br/>Gittins (Lean) · Thompson Sampling"]
    BAY["Corpus bayésien<br/>../Infer/ (posteriors)"]
    LAKE["Lake decision_theory_lean<br/>(companions 2, 2b, 8b)"]
    BAY -->|"posterior = input"| A
    A --> B --> C --> D --> E
    E -.->|"formalisation"| LAKE
    %% color: explicite -- sans lui, libelle clair sur fond clair en mode sombre GitHub (#15022) ; ne pas harmoniser le ton avec le stroke (libelle sinon illisible)
    classDef lean fill:#fff3cd,stroke:#856404,stroke-width:2px,color:#856404;
    class LAKE lean;

Le socle des fondations (1-3) pose les axiomes de rationalité et la notion d’aversion au risque ; les notebooks 4-5 étendent aux décisions multi-critères et aux réseaux de décision (nœuds de chance/décision/utilité) ; 6-7 mesurent la valeur de l’information et la robustesse sous incertitude sévère ; 8 introduit le séquentiel (MDPs, équation de Bellman) ; 9-10 clôturent par les bandits bayésiens (Thompson Sampling calculé par le moteur Infer.NET) et la preuve formelle Lean 4 de l’indice de Gittins.

Détail des notebooks

DecInfer-01 : Fondements de l’utilité (axiomes VNM)

Durée : 50 min | Prérequis : corpus bayésien Infer-4

Les loteries comme représentation des choix stochastiques ; les axiomes de Von Neumann-Morgenstern (complétude, transitivité, continuité, indépendance) ; dérivation de la fonction d’utilité par calibration ; l’agent rationnel maximise E[U]. Applications : décision médicale, assurance, investissement.

DecInfer-02 : Companion Lean — théorème vNM (sound) + cohérence de de Finetti

Durée : 45 min | Kernel : Lean 4 (WSL) | Prérequis : DecInfer-01, bases Lean 4

Companion natif de DecInfer-01 : preuve formelle 0-sorry de la direction sound du théorème de représentation vNM (représentation ⟹ rationalité) dans le lake decision_theory_lean (lib Utility). Vérification in-kernel via #check + #print axioms. Les sections 7-8 d’origine — la cohérence de de Finetti (lib Coherence, EPIC #11703) : prix incohérents ⟹ Dutch Book à quatre tickets, et la caractérisation mono-livret SingleCoherent q ↔︎ ProbBounds q — ont été extraites vers le companion dédié DecInfer-02b-Lean-Coherence (G4b, #14873).

DecInfer-02b : Companion Lean — cohérence de de Finetti (Dutch Book)

Durée : 20 min | Kernel : Lean 4 (WSL) | Prérequis : DecInfer-02, bases Lean 4

Companion natif extrait des sections 7-8 de DecInfer-02 (G4b, #14873) : la cohérence de de Finetti (1937) dans la lib Coherence du lake decision_theory_lean. Un système de prix arbitrage-incohérent est exploitable par un Dutch Book à quatre tickets (non_additive_implies_dutch_book, witness constructif) ; dans le cadre mono-livret, la cohérence coïncide exactement avec les bornes de probabilité (single_coherent_iff_prob_bounds, quatre témoins explicites — un par borne violée). Vérification in-kernel via #check + #print axioms, 0 sorry.

DecInfer-03 : Utilité de l’argent et aversion au risque

Durée : 45 min | Prérequis : DecInfer-01

Paradoxe de Saint-Petersbourg (valeur espérée infinie), fonctions CARA et CRRA, coefficients Arrow-Pratt (aversion absolue/relative), dominance stochastique (1er et 2nd ordre), équivalent certain et prime de risque. Application : sélection de portefeuille (Livret A vs Fonds vs Actions).

La concavité de la fonction d’utilité — fondement de l’aversion au risque et de l’utilité marginale décroissante — s’illustre par les trois fonctions fondamentales U(x) = √x, U(x) = ln(x) (toutes deux strictement concaves) et U(x) = x (neutre au risque, en référence) tracées côte-à-côte sur la figure de la racine Probas :

Trois fonctions d’utilité fondamentales sur trois panneaux côte-à-côte : racine carrée U(x)=√x (concave), logarithme U(x)=ln(x) (concave), et linéaire U(x)=x (neutre au risque, en référence) — montrant l’utilité marginale décroissante : les deux courbes concaves s’aplatissent quand la richesse x augmente, tandis que la linéaire reste constante.

Figure reprise de la racine Probas (MANIFEST c.491 audit G.1, 1/1 ACCURATE). Source originale : DecPyMC-2-Utility-Money.ipynb, cellule 10 « Démonstration numérique : utilité marginale décroissante ». Voir aussi le README racine Probas § De la distribution à l’utilité pour le cadrage théorique (Pratt 1964, Arrow 1965).

DecInfer-04 : Utilité multi-attributs

Durée : 50 min | Prérequis : DecInfer-01, DecInfer-03

Décisions multi-critères, fonctions de valeur vs utilité, indépendance préférentielle, théorèmes d’additivité (Debreu-Gorman) et multiplicativité, méthode SMART (swing weights). Applications : achat automobile (prix, sécurité, conso, confort), choix de carrière.

DecInfer-05 : Réseaux de décision

Durée : 55 min | Prérequis : Infer-4 bayésien, Infer-1, Infer-4

Extension des réseaux bayésiens par les nœuds de décision (rectangle) et d’utilité (losange) ; arcs informationnels ; calcul de la politique optimale par backward induction ; décisions séquentielles. Applications : diagnostic médical avec décision de traitement, investissement avec étude de marché.

DecInfer-06 : Valeur de l’information

Durée : 45 min | Prérequis : DecInfer-01 à DecInfer-05

EVPI (valeur de l’information parfaite) et EVSI (valeur de l’information d’échantillon) ; quand l’information a-t-elle de la valeur ; efficacité relative d’un test (EVSI/EVPI). Applications : droits pétroliers (test sismique), diagnostic médical itératif.

DecInfer-07 : Systèmes experts et robustesse

Durée : 50 min | Prérequis : DecInfer-01 à DecInfer-06

Systèmes experts (architecture, historique) ; décision sous incertitude sévère (knightienne) ; critères Minimax, Minimax Regret, Maximax, Hurwicz ; robustesse aux erreurs de modélisation. Applications : diagnostic informatique, décisions financières robustes.

DecInfer-08 : Décisions séquentielles (MDPs)

Durée : 60 min | Prérequis : DecInfer-01 à DecInfer-07

Processus de Décision Markoviens (MDPs) ; équation de Bellman V(s) = max_a [R(s,a) + γ·Σ P(s'|s,a)·V(s')] ; itération de valeur et itération de politique ; alternatives (LP, Expectimax, RTDP) ; reward shaping ; POMDPs. Pont vers la série RL.

DecInfer-08b : Companion Lean — indice de Gittins

Durée : 45 min | Kernel : Lean 4 (WSL) | Prérequis : DecInfer-08, bases Lean 4

Companion natif de DecInfer-08 : preuves formelles en Lean 4. Formalisation du cadre SFABP (Simple Family of Alternative Bandit Processes), optimalité de l’indice de Gittins via l’argument des prevailing charges, limitations (geometric discount, NP-difficulté du calcul exact). Le théorème d’optimalité est énoncé dans le lake decision_theory_lean ; sa preuve complète exige une formalisation des MDP qui manque encore à Mathlib.

DecInfer-10 : Thompson Sampling bayésien

Durée : 60 min | Prérequis : Infer-7 bayésien (posterior Beta), Infer-8 (bandits, ε-greedy, UCB1)

Le bandit multi-bras vu comme un programme probabiliste Infer.NET : le moteur d’inférence (EP/VMP) calcule le posterior Beta-Bernoulli de chaque bras plutôt que d’appliquer la formule conjuguée à la main. Thompson Sampling : jouer le bras dont l’échantillon posterior est le plus élevé. Mesure du regret cumulé face à ε-greedy et UCB1 (Thompson exploite l’incertitude posterior). Extension au best-arm identification. La généralisation à des modèles non conjugués (où seule l’inférence approchée sait calculer le posterior) justifie l’usage du moteur.

Applications : A/B testing adaptatif, recommandation en ligne, essais cliniques séquentiels.

Ponts inter-series

Série	Lien	Relation
Corpus bayésien Infer	Posteriors (Beta, gaussianes)	Le posterior est l’input de la politique de décision
PyMC	DecPyMC-1 à DecPyMC-7	Même arc décision en Python/NUTS (Thompson MCMC, diagnostics ArviZ)
Lake `decision_theory_lean`	Companions 2, 2b, 8b	Preuves formelles Lean 4 (vNM, de Finetti, Gittins)
GameTheory	Décision sous incertitude	Miroir : adversaire rationnel vs processus stochastique
RL	MDPs (DecInfer-08)	L’agent apprend la politique par interaction

Conclusion

La théorie de la décision bayésienne ferme la boucle ouverte par le corpus bayésien : un posterior n’est utile que s’il informe une action. De l’utilité espérée (DecInfer-01) aux MDPs (DecInfer-08), cet arc montre que décider sous incertitude est un calcul rigoureux — et les companions Lean 4 (DecInfer-02, DecInfer-02b, DecInfer-08b) ancrent ce calcul dans la preuve formelle : l’indice de Gittins n’est pas une heuristique, c’est un théorème.

Bonne exploration de la théorie de la décision bayésienne !

Retour au sommet