Ce que je construis en dehors des cours

Cinq projets autonomes en apprentissage automatique, calcul formel et mathématiques appliquées. Personne ne les a demandés, chaque chiffre est produit par du code présent dans le dépôt, et l'intégration continue rejoue les vérifications à chaque envoi.

Celui qui mérite d'être raconté

Un réseau convolutif apprenant Flappy Bird à partir des seules images rendues. Le plus grand gain de tout le projet est venu de l'observation et non d'un hyperparamètre. Réduire une image à un seul canal est courant, et la façon courante est un niveau de gris de luminance, mais l'oiseau est jaune et le ciel bleu clair, et ces deux couleurs sont presque équiluminantes : mesuré sur les sprites, l'oiseau se détache du ciel de 22 niveaux sur 255 en luminance, et de 181 dans le canal bleu.

Le niveau de gris livrait les obstacles à trois fois le contraste de l'oiseau lui-même, qui est pourtant l'objet dont la politique a le plus besoin de connaître la position. Tout le reste étant tenu fixe, même graine et mêmes hyperparamètres, prendre le canal bleu à la place a fait passer l'agent de 0,4 tuyau à 12,65 à 250 000 pas. L'exécution en niveau de gris n'a jamais dépassé 0,8 en 420 000 pas.

Les six

Site Les parcourir tous Chaque projet sur une page, avec les animations et les graphiques en taille réelle. Optimisation Programmation en nombres entiers Un simplexe en deux phases sur des rationnels exacts, puis séparation et évaluation. 200 programmes tirés au hasard donnent le même optimum qu'une énumération de tous les points entiers. Renforcement Flappy Bird à partir des pixels Un DQN atteignant 12,21 tuyaux en moyenne sur 100 épisodes, et une exécution REINFORCE qui n'en a jamais franchi un, expliquée. Algèbre 3-SAT sur GF(2) Les clauses comme polynômes dans l'anneau booléen. 500 instances vérifiées contre une recherche exhaustive, sans aucun verdict erroné. Maths Algorithmes matriciels repris de zéro FFT, déterminant par complément de Schur et inverse entier exact, vérifiés contre NumPy à 1e-13. Graphisme Les tris, rendus Tri à bulles et tri fusion animés image par image via l'API Python de Blender, de sorte que le motif d'accès soit observable. Appliqué L'impôt sur le revenu français Le taux effectif ajusté par tranche, la fonction W de Lambert situant le point d'inflexion à 59 800 EUR.

Comment les animations sont vérifiées

Les animations de tri et la séparation et évaluation partagent une chose : l’algorithme et son image sont deux programmes distincts. Chacun s’exécute en Python pur et émet une trace — une ligne par chose faite, dans le vocabulaire du problème, jamais dans celui de la géométrie. C’est ce qui permet à l’intégration continue de vérifier que l’algorithme a bien fait ce que l’image prétend, ce qu’une vidéo ne montrera jamais, et deux moteurs de rendu peuvent raconter la même exécution autrement. Les tris sont animés dans Blender ; l’arbre ci-dessous est dessiné en SVG dans votre navigateur, à partir des mêmes cinq verbes.

0	open	n0	depth 0
1	bound	n0	value 224/5
2	open	n1	parent n0, depth 1, branch x0 <= 2
3	bound	n1	value 312/7
4	open	n2	parent n1, depth 2, branch x1 <= 0
5	bound	n2	value 44
6	adopt	n2	value 44, point 2,0,1,0
7	open	n3	parent n1, depth 2, branch x1 >= 1
8	bound	n3	value 222/5
9	open	n4	parent n3, depth 3, branch x0 <= 1
10	bound	n4	value 310/7
11	open	n5	parent n4, depth 4, branch x1 <= 1
12	bound	n5	value 44
13	prune	n5	why bounded
14	open	n6	parent n4, depth 4, branch x1 >= 2
15	bound	n6	value 44
16	prune	n6	why bounded
17	close	n4
18	open	n7	parent n3, depth 3, branch x0 >= 2
19	prune	n7	why infeasible
20	close	n3
21	close	n1
22	open	n8	parent n0, depth 1, branch x0 >= 3
23	prune	n8	why infeasible
24	close	n0

La séparation et évaluation résolvant un sac à dos de quatre objets, rejouée depuis sa propre trace. Faites glisser le curseur, ou lancez la lecture. Un nœud est ouvert, borné par sa relaxation, puis élagué (gris), ou trouvé entier (or), ou coupé en deux. La relaxation donne 44⁄5 à la racine et la réponse est 44, réglée en neuf nœuds. Chaque borne est un rationnel exact : rien ici n’est jamais un flottant, donc une branche élaguée ne peut démontrablement pas contenir la réponse.

Ce que le solveur SAT montre réellement

Sa propre mesure est que l'étape algébrique est presque inerte : sur les instances insatisfiables testées, l'élimination seule n'en a détecté presque aucune, et c'est le branchement qui fait le travail. Le dépôt le dit plutôt que de l'enfouir. Il est en outre évalué en deçà de la transition de phase, où la plupart des instances sont satisfiables, ce que l'écrit signale lui-même comme un point ouvert.