Probas — Programmation probabiliste

Série pédagogique niveau 2 — Inférence exacte (Infer.NET) vs MCMC (PyMC), théorie de la décision, preuves Lean 4

Série Probas du dépôt CoursIA — modèles graphiques, réseaux bayésiens, IRT, TrueSkill, HMM, LDA, Gaussian Processes, MDPs, bandits, indice de Gittins, formalisation Lean 4 de l’utilité espérée et du Gittins index.

Probas — Programmation probabiliste et théorie de la décision

L’incertitude n’est pas l’absence d’information, c’est une distribution. Cette série forme sur deux axes complémentaires : inférer des distributions (Infer.NET message passing vs PyMC NUTS, sur les mêmes modèles : Gaussian Mixtures, IRT, TrueSkill, LDA, HMM, Kalman) et décider face à l’incertitude (utility espérée, MDPs, bandits, indice de Gittins — avec preuves formelles Lean 4 pour les identités théoriques). À la fin, vous maîtrisez la boîte à outils probabiliste complète et vous savez prouver formellement les résultats clefs.

Vue d’ensemble

La série Probas comporte 4 sous-séries principales + applications standalone, totalisant ~58 notebooks. Deux moteurs d’inférence sont volontairement juxtaposés (Infer.NET C# exact par message passing, PyMC Python MCMC par NUTS) sur les mêmes modèles pour faire valoir leurs compromis. Les deux arcs — bayésien (corpus principal 1-19/1-14) et décision (10 + 8 + 5 notebooks) — sont physiquement séparés (depuis #4725) tout en préservant le continuum pédagogique.

Sous-série	Notebooks	Stack	Focus
Infer (C#/.NET Interactive)	19 (+ Setup + accretion Infer-1b + _output.ipynb)	Infer.NET, EP/VMP	Corpus bayésien : fondations, modèles classiques (IRT, TrueSkill, LDA, HMM), frontières (causalité, GP, hiérarchiques, Kalman, change-point, survie)
PyMC (Python)	14 (+ Setup)	PyMC, NUTS	Mêmes modèles qu’Infer, en MCMC : NUTS, diagnostics (R-hat, ESS), posterior predictive checks
DecisionTheory/Infer (C#/.NET)	10 (Lean : 02, 02b, 08b)	Infer.NET + Lean 4	Utility espérée, EVPI, MDPs, bandits, preuves formelles Lean de vNM et Gittins (lake decision_theory_lean/)
DecisionTheory/DecPyMC (Python)	8 (socle 7 + capstone)	PyMC	Mêmes modèles de décision, en sampling
DecisionTheory/Actuariat (Python)	5	PyMC	Sous-série actuarielle T1-T5 : tarification, crédibilité, ruine, valeur de l’information
DecisionTheory/Causal-Bridges	1	Python/Z3	Do-Calculus, jumeaux causaux inter-domaines
Applications (standalone)	1	Python	Pyro_RSA_Hyperbole (Pyro RSA)

Kernels : dotnet-csharp · python3 · lean4 (side tracks Lean via WSL, cf decision_theory_lean/install_wsl_kernel.md) · GPU : non (Infer.NET/PyMC CPU-only) · Prérequis : algèbre linéaire, probabilités de base (variables aléatoires, Bayes), Python intermédiaire.

Parcours : Parcours 1 — local sobre · niveau 2

Corpus bayésien — Infer.NET (C#/.NET Interactive)

19 notebooks en .NET Interactive : du Setup aux frontières (causalité, GP, hiérarchiques, Kalman). Le moteur Infer.NET utilise EP/VMP (expectation propagation / variational message passing), donnant des résultats déterministes et rapides sur les modèles compatibles.

Corpus bayésien — Infer.NET — Notebooks avancés (10-14)

Crowdsourcing (vraie vraisemblance distribuée), séquences (HMM), recommanders (matrix factorization + side-info), debugging (inspection de la convergence EP), causal inference (do-calculus). Ces notebooks prolongent le corpus 2-9 vers des modèles à grande échelle ou des structures non-standard.

Corpus bayésien — Infer.NET — Frontières (15-19)

Gaussian Process creux, modèles hiérarchiques, filtre de Kalman, change-point detection, analyse de survie. Ces notebooks montrent qu’Infer.NET n’est pas cantonné aux modèles factor graphs simples et explore les domaines où l’inférence exacte/EP est compétitive.

Corpus bayésien — PyMC (Python)

14 notebooks en Python pymc : mêmes modèles 1-14 qu’Infer, en MCMC NUTS. Avantage : s’applique à presque tout modèle ; coût : stochasticité, temps de convergence variable, diagnostic R-hat/ESS nécessaire.

Théorie de la décision — Infer.NET + Lean 4

Arc autonome de théorie de la décision bayésienne : axiomes Von Neumann-Morgenstern, utilité espérée, EVPI, réseaux de décision, MDPs (itération valeur/politique), Thompson Sampling. Trois notebooks sont des companions Lean 4 (kernel WSL + lake decision_theory_lean) qui prouvent formellement :

• DecInfer-02-Lean-ExpectedUtility : direction sound du théorème vNM (utilité linéaire sur des loteries).
• DecInfer-02b-Lean-Coherence : cohérence de de Finetti — Dutch Book, caractérisation mono-livret des bornes de probabilité.
• DecInfer-08b-Lean-Gittins : indice de Gittins, SFABP (Single-Family Action-Bandit Processes).

Théorie de la décision — PyMC (Python)

Mêmes modèles de décision, en sampling PyMC : utilité, valeurs d’information, EVPI, réseaux.

Causal-Bridges — Do-Calculus inter-domaines

Notebook passerelle entre Probas, Search (CSP/SMT) et SymbolicAI : encode le Do-Calculus (Pearl) via Z3 pour raisonner sur des interventions (do(X=x)) en présence de variables non observées.

Applications — Notebooks standalone

Un notebook applicatif autonome, indépendant des deux arcs, vit dans Applications/ :

• Pyro_RSA_Hyperbole : Rational Speech Acts bayésien en Pyro (sémantique pragmatique).

L’entrée Infer.NET du corpus bayésien est Infer-1b (accretion du premier modèle, ex-Infer-101), dans Infer/.

Démarrage rapide

Pour Infer.NET (C#/.NET Interactive)

dotnet tool install --global Microsoft.dotnet-interactive
# Puis dans Jupyter : choisir le kernel ".NET (C#)"

Chaque notebook Infer commence par les déclarations #r "nuget: ..." et using Microsoft.ML.Probabilistic; — l’environnement se configure à l’exécution.

Pour PyMC (Python)

python -m venv .venv
source .venv/bin/activate     # ou .venv\Scripts\activate sous Windows
pip install pymc arviz numpy pandas matplotlib
jupyter notebook MyIA.AI.Notebooks/Probas/PyMC/

Pour les companions Lean 4 (DecInfer-02-Lean-ExpectedUtility.ipynb, DecInfer-02b-Lean-Coherence.ipynb, DecInfer-08b-Lean-Gittins.ipynb) : WSL + elan toolchain + kernel Lean4 Jupyter. Cf decision_theory_lean/install_wsl_kernel.md. Les preuves sont déjà validées localement (lake decision_theory_lean build SUCCESS) ; les notebooks servent de vitrine pédagogique.

Ressources complémentaires

• Catalogue : COURSE_CATALOG.generated.md — inventaire exhaustif de la série avec statuts READY/DEMO, kernels, GPU.
• README de série : Probas/README.md — vue d’ensemble, progression pédagogique complète, comparaison Infer/PyMC, ramifications vers DecisionTheory.
• Lake Lean : decision_theory_lean/ — preuves formelles des identités d’escompte (Gittins), vNM sound direction.
• Séries connexes :
  • GameTheory — théorie des jeux bayésienne (jeux bayésiens, jeux de réputation), certaines preuves Lean voisinent celles de decision_theory_lean/.
  • Search — algorithmes de recherche, CSP, MCTS (certains algorithmes probabilistes en bandit).
  • ML — machine learning, où les modèles probabilistes (Gaussian Processes, LDA) rejoignent les modèles discriminatifs.

Note sur le rendu Quarto (.NET + Lean + Python)

Cette page Quarto rend les notebooks Python natifs (PyMC + Causal-Bridges + Pyro_RSA) ainsi que leurs *_output.ipynb committés (règle C.2). Les notebooks .NET C# (Infer/* principaux + DecisionTheory/DecInfer/*) et les companions Lean 4 (*-Lean-*) ne sont pas exécutés par Quarto : leur rendu s’appuie sur les *_output.ipynb committés via le mode freeze: auto de _quarto.yml. Pour une exécution locale : kernel dotnet-csharp pour Infer.NET ; kernel Lean4 (WSL + elan) pour les companions. Ce point est la matière de la tranche 4 #4211 (GH Actions deploy) — un workflow dédié pourra automatiser exécution et publication, mais le MVP actuel se contente de freeze auto sans ré-exécution.

Pour aller plus loin

Une fois la série Probas maîtrisée, les parcours conseillés sont :

1. Vers l’inférence causale : DecisionTheory/Causal-Bridges — Do-Calculus, raisonnement causal.
2. Vers la théorie des jeux : GameTheory — équilibres bayésiens, jeux de réputation.
3. Vers le machine learning discriminant : ML — régression/probabilités conditionnelles, où les modèles probabilistes rejoignent le deep learning.
4. Vers la formalisation : decision_theory_lean/ — preuves formelles en Lean 4 des identités d’escompte et de Gittins.
5. Vers la simulation multi-agent : IIT — PyPhi, integrated information, où la théorie de la décision probabiliste alimente la théorie de l’information intégrée.