after-hours

Ce que je construis quand je m'ennuie.

Personne ne me l'a demandé et rien ici n'est un devoir : c'est ce que devient une soirée libre, en apprentissage automatique, calcul formel et mathématiques appliquées. Chaque projet est autonome. Chaque chiffre de cette page est produit par du code du dépôt, et la CI rejoue les vérifications à chaque push.

Dépôt CI Poids et rendus

Flappy Bird à partir des pixels bruts

12,21 tuyaux par épisode sur 100 épisodes déterministes, record 61, entraîné en 23 minutes sur une seule RTX 4060

Un DQN entraîné qui joue à Flappy Bird — L'agent entraîné. Il ne voit rien d'autre que cette image : ni position, ni vitesse, ni coordonnées des tuyaux.

L'agent a stagné longtemps et aucun hyperparamètre n'y changeait rien. L'oiseau est jaune, le ciel bleu clair, et les deux sont presque équiluminants : la conversion en niveaux de gris que tout pipeline Atari utilise donnait à l'oiseau 22 niveaux de contraste sur 255, contre 64 aux tuyaux. Prendre le canal bleu en donne 181.

La même image en niveaux de gris puis en canal bleu — À gauche, ce que le jeu affiche. Au milieu, ce que le réseau recevait. À droite, ce qu'il reçoit désormais.

Courbes d'apprentissage pour les deux canaux d'observation — Même réseau, mêmes hyperparamètres, même graine. Seul le canal de couleur change.

DQN contre REINFORCE avec baseline de valeur — REINFORCE n'a jamais franchi un tuyau : 756 mises à jour de gradient contre 61 250 pour le DQN, à expérience comparable.

En niveaux de gris il a fallu 200k pas pour franchir un premier tuyau, et le score n'a jamais dépassé 0,80. En canal bleu, un tuyau à 50k pas et dix à 250k. Le compte rendu garde aussi la tentative qui a échoué, et une erreur d'échelle de ma part qui rendait la perte de valeur 224 fois plus grande que celle de la politique.

Un solveur 3-SAT sur GF(2)

0 verdict faux sur 500 instances confrontées à une recherche exhaustive

Une instance 3-SAT comme système linéaire sur GF(2), avant et après réduction — Chaque clause devient un polynôme ; chaque monôme distinct devient une inconnue. L'escalier rouge est le terme dominant de chaque équation, la structure triangulaire qui donne son nom à la méthode.

Les clauses deviennent des polynômes sur GF(2), une élimination triangulaire à la Gröbner propage ce qu'elle peut, et le branchement termine. Les verdicts sont vérifiés en validant l'affectation renvoyée, pas seulement la réponse SAT ou UNSAT.

Le plus intéressant est là où il refuse de se survendre. L'étape d'élimination seule est correcte mais faible : sur 285 instances réellement insatisfiables elle en a signalé une, et à n=20 elle résout 0,00 % des systèmes par elle-même, donc c'est le branchement qui fait tout le travail. Le ratio du banc d'essai se situe aussi en dessous de la transition de phase du 3-SAT aléatoire, ce qui veut dire qu'un bon taux de réussite y mesure la distribution des instances plutôt que le solveur. Le dossier conserve enfin un article de 2023 dont l'affirmation centrale est fausse, avec la ligne fautive localisée et expliquée.

Instances insatisfiables face au nombre que l'élimination a détecté — Sur 272 instances insatisfiables, l'élimination seule n'en a détecté aucune. Mesuré, pas estimé.

Algorithmes de tri en 3D

1407 et 801 images en 1080p24, rendues sans interface en 4 et 2 minutes

Tri à bulles animé dans Blender — Tri à bulles. Le marqueur rouge qui parcourt la rangée encore et encore, une place plus court à chaque passe, c'est le O(n²).

Tri fusion animé dans Blender — Tri fusion. La profondeur de récursion se lit comme une distance physique à la rangée de départ.

Les deux sont pilotés entièrement depuis l'API Python de Blender et se rendent en ligne de commande. Les scripts ne pouvaient auparavant pas être rendus du tout : ils suppriment la caméra et la lumière par défaut dès leur première ligne et ne fixent aucune plage d'images, si bien que la limite de 250 images de Blender capturait 18 % du tri à bulles sur un écran noir.

Algorithmes matriciels de zéro

11 vérifications contre NumPy, concordance à 1e-13

Transformées réécrites à la main contre numpy.fft — Une transformée de Cooley-Tukey radix-2 réécrite, vérifiée contre `numpy.fft` jusqu'à n=64.

Une FFT, un déterminant par complément de Schur, un inverse matriciel exact en arithmétique entière et une trace qui ne forme jamais le produit. NumPy sert partout d'oracle contre lequel chaque résultat est vérifié, jamais d'implémentation : le déterminant n'appelle pas numpy.linalg.det et les transformées n'appellent pas numpy.fft.

Aucun n'est rapide, et chaque notebook trace son propre coût pour que l'écart soit visible plutôt que sous-entendu. L'inverse est exact et non approché : A @ A_inverse est l'identité, pas quelque chose qui s'en approche.

L'impôt français, modélisé

Le point de bascule est à 59 800 € de brut annuel

Taux effectif face au barème, avec le point de bascule marqué — Le barème est un escalier ; le taux que l'on paie réellement est la courbe lisse en dessous.

À partir de quand un euro brut supplémentaire cesse-t-il de rapporter beaucoup ? Ajuster le taux effectif comme une approche exponentielle vers une asymptote, puis chercher où sa pente cesse de croître, demande la fonction W de Lambert, car l'équation prend la forme v·e^v = c. Les deux branches sont calculées et l'on retient celle qui tombe dans la plage de revenus. Lire le rapport complet.