Vers une imposition formalisée⠀?

Ésotériques, inutilisables, perchées, idéalistes : les méthodes formelles sont parfois critiquées par la communauté informatique à cause d’un certain élitisme qui rend difficile la communication entre chercheurs et développeurs. En effet, la barrière d’entrée est assez haute pour pouvoir utiliser les méthodes formelles lorsque l’on n’a pas fait de master de mathématique, spécialité théorie des catégories. L’immense majorité des développeurs, qui utilise des langages comme Python ou Javascript, n’est jamais exposée aux concepts un peu plus théoriques que j’essaie d’expliquer sur ce blog, et qui améliorent pourtant souvent la productivité de la programmation. Et ce n’est pas grave : vouloir utiliser ces outils et concepts compliqués sur n’importe quel problème s’apparente à chasser des mouches à l’aide d’un bazooka.

Cependant, de temps à autre, un problème réellement complexe survient, et l’outillage habituel se révèle insuffisant. C’est bien dans ces cas là qu’un peu de théorie peut sauver la mise ! Aujourd’hui, en guise d’illustration de cette affirmation, je vais vous raconter l’histoire d’un langage mystérieux, de la Direction Générale des Finances Publiques, de preuve automatique de théorèmes à propos de l’impôt sur le revenu et d’expression algorithmique de la loi. Cette histoire a débouché sur le projet Verifisc, et ouvre la voie à une réappropriation de la complexité du système fiscal français grâce à des outils accessibles à tous.

Calculer son impôt: un enjeu démocratique ?

En parallèle de mon sujet de thèse, j’essaie de toujours garder un œil ouvert sur de potentielles opportunités d’appliquer mon domaine de recherche à de nouveaux problèmes. Aussi, en janvier 2019, lorsque j’ai connaissance d’une conférence donnée par la professeure de droit Sarah Lawsky à la conférence POPL en 2018, je suis intrigué par le titre de la présentation : « Formal Methods and the Law ». En lisant les articles de cette chercheuse, je me rend compte que certaines parties de la loi décrivent des processus très précis, parfois à l’aide de calculs mathématiques : ce sont des algorithmes. Plus précisément, Lawsky prend l’exemple de certaines provisions du Code des impôts américains dont elle décrit précisément le sens à l’aide de formules logiques.

Je me pose alors la question de l’utilité d’une telle démarche : qu’est-ce que la formalisation du code des impôts nous permettrait de faire de plus que ce que l’on sait déjà faire ? Déjà, et comme le pointe Lawksy, cela permettrait de clarifier certaines dispositions législatives à l’intention ambiguë. Mais la valeur ajoutée de cette clarification, certes grande d’un point de vue juridique, me laisse sur ma faim. Je me demande alors si la formalisation ne pourrait pas nous aider à mieux comprendre comment le montant de l’impôt est calculé.

À ce stade, il est nécessaire de faire un tour d’horizon des outils qui existent autour de la manière dont l’impôt est calculé. Il existe déjà un simulateur permettant de calculer l’impôt sur le revenu à partir d’une déclaration fiscale. L’Insee produit également de nombreuses études étudiant l’effet de l’impôt sur le revenu et des allocations sur le revenu effectif des ménages. L’initiative OpenFisca, menée par Etalab, offre même une implémentation complète du système socio-fiscal français à destination des économistes qui mènent de telles études.

Cependant, dans tous ces travaux, on doit partir de données réelles correspondant à des foyers fiscaux $x_1,\ldots,x_n$ pour calculer des quantités $f(x_1),\ldots,f(x_n)$ (impôts, allocations, etc). Les données de départ conditionnent la portée de l’étude, et le secret fiscal rend l’accès aux données fiscales des ménages très difficile. Dès lors, comment étudier à l’avance les effets d’une réforme fiscale ? Le site LexImpact, construit sur OpenFisca, permet de visualiser rapidement les effets d’une modification des paramètres de la législation en place sur des cas types. Les parlementaires et leurs collaborateurs ont également la possibilité de simuler leur réforme sur un échantillon réduit de foyers fiscaux tirés de données réelles (quelques milliers).

Mais un échantillon de quelques milliers ou dizaines de milliers de foyers fiscaux est-il suffisant pour observer les effets d’une réforme fiscale dans tous les cas possibles ? Faisons un petit calcul : si l’on compte 20 tranches de revenus à considérer pour les ménages (de 1600 € à 1700 €, de 1700 € à 1800 €, etc), les 3 cas de situations matrimoniales (célibataire, couple, concubinage), un nombre de personnes à charge compris entre 0 et 5, la possibilité pour tout ou partie de ces personnes d’êtres invalides, on arrive à plusieurs milliers de cas différents à étudier ! De plus, sur un échantillon réduit, la majorité des données se concentreront dans des catégories « moyennes » sur-représentées, réduisant d’autant plus les chances d’avoir une couverture optimale de tous les cas possibles par le jeu de données. Et tout cela ne prend pas en compte l’étude des effets fiscaux sur un même foyer fiscal évoluant d’année en année, avec des variations de revenus, des changements de situation familiale, etc.

Partant de ce constat, je me rends compte que la problématique de l’étude de la législation fiscale et de ses effets sur la population dans sa diversité ne bénéficie pas d’un outillage d’analyse à la hauteur de l’impact qu’elle peut avoir sur la vie des citoyens. Une mauvaise interaction entre une tranche d’impôt et le seuil d’une allocation peut avoir des conséquences dramatiques sur la vie d’une famille, avec des pertes potentielles allant jusqu’à plusieurs centaines d’euros par mois. Mais ces hypothétiques situations malencontreuses existent-t-elles vraiment ? Si oui, comment les identifier systématiquement afin de les corriger ?

La complexité de la législation fiscale, produit d’une construction historique mais aussi de la nécessité de répondre à une grande diversité de situations issues du réel, risque d’échapper à ses créateurs tel un Frankestein juridique. La visibilité des effets de la fiscalité et des allocations en général est également un enjeu démocratique, comme en témoigne le récent débat à propos des cas types du rapport Delevoye sur la réforme des retraites. En attendant une remise à plat telle que celle proposée par Landais, Piketty et Saez en 2011, j’ai décidé de voir ce que mon domaine de recherche, les méthodes formelles, pouvaient apporter à cette problématique.

Un modèle socio-fiscal prouvé automatiquement

L’étude de la fiscalité et des allocations est un problème intrinsèquement mathématique, une fois posé de la bonne manière. En effet, on suppose dans toute la suite disposer d’informations sur les ménages similaires au contenu d’une déclaration de revenus ou des formulaires des simulateurs en ligne permettant d’évaluer ses droits aux différentes aides et allocations. La quantité d’argent due (au titre de l’impôt) ou reçue (par une allocation) n’est alors qu’une simple fonction mathématique des caractéristiques du ménage. Afin d’étudier cette fonction, j’ai décidé de l’encoder dans un solveur SMT appelé Z3.

Un solveur SMT est une instance particulière de ce que l’on appelle un prouveur automatique de théorèmes. Ces prouveurs automatiques marchent de la manière suivante :

• on encode un problème sous forme de contraintes portant sur des variables booléennes ou entières ($x_1 \leqslant 4$ et $x_2 + 3 > x_1$ par exemple) ;
• on demande ensuite au prouveur s’il existe des valeurs pour les variables du problème telles que toutes les contraintes soient satisfaites ;
• si la réponse est oui, alors le prouveur renvoie un tel assignement des variables. Si la réponse est négative, alors le prouveur garantit que ces contraintes ne peuvent pas être satisfaites.

Dans notre cas, les variables sont les caractéristiques du ménage : nombre d’enfants, revenus, etc. Les contraintes servent à modéliser deux choses. Premièrement, les règles de calcul de l’impôt et des allocations. Par exemple, « si le ménage est un couple avec deux enfants non-invalides, alors le quotient familial est égal à 3 ». Deuxièmement, les contraintes nous servent également à poser les questions que l’on veut à notre petit modèle socio-fiscal. En effet, si l’on cherche des ménages payant un impôt supérieur ou égal à 30% de leur revenu, il suffit d’ajouter cette contrainte au modèle. Le solveur SMT nous dira alors si un tel ménage existe, et si oui, nous en donnera un exemple.

Rentrons tout de suite dans le dur avec une problématique qui a des conséquences concrètes pour nombre de ménages : la taxation marginale et les effets de seuil. Imaginons qu’un individu du ménage voit son salaire augmenter d’une année sur l’autre. Il va alors payer plus d’impôt sur le revenu, mais aussi voir certaines allocations diminuer. La question que l’on se pose est la suivante : existe-t-il des situations où le ménage voit ses revenus effectifs diminuer, alors même que le salaire augmente ? Plus précisément, nous cherchons des taux marginaux effectifs de prélèvement supérieurs à 100 %.

Le solveur SMT a pu répondre à cette question : c’est oui ! Mais plus intéressant, cette réponse positive est accompagnée d’un exemple qui satisfait toutes les contraintes. Cet exemple ne correspond pas à des données réelles de ménages français dont disposerait le solveur, mais à une situation hypothétique déduite de l’étude des fonctions mathématiques de calcul des impôts et des allocations. Bien qu’hypothétiques, ces exemples n’en sont pas moins réalistes et mettent en valeur des angles morts législatifs, résultant de l’interaction malencontreuse de plusieurs dispositifs pensés séparément.

Ici, nous avons donc un couple en concubinage dont le premier individu gagne un salaire net de 1768,55 €, le deuxième individu étant sans activité. Le couple a deux enfants de 17 et 16 ans, scolarisés au lycée, et qui sont à la charge du deuxième individu sans activité. La famille loue un logement en zone III (hors agglomération de plus de 100 000 habitants) pour 784,09 € par mois. On suppose que le premier individu du couple est augmenté de 40 € par mois (soit 2,2 % du salaire) l’année suivante. Pour ce ménage, voici donc les montants de l’impôt sur le revenu et de diverses allocations, qui sont calculés à l’équilibre avant et après l’augmentation (on ne tient pas compte du fait que certaines allocations sont calculées à partir des revenus $N-2$ alors qu’avec le prélèvement à la source l’impôt est calculé sur les revenus $N$) :

Montant	Valeur avant	Valeur après	Différence
Salaire annuel	21 223,00 €	21 703,00 €	480,00 €
Revenu fiscal de référence	19 101,00 €	19 533,00 €	432,00 €
Impôt sur le revenu	846,00 €	981,00 €	135,00 €
Allocations familiales	132,00 €	132,00 €	0,00 €
Allocation rentrée scolaire	806,00 €	806,00 €	0,00 €
Bourses collège	0,00 €	0,00 €	0,00 €
Bourses lycée	876,00 €	0,00 €	- 876,00 €
Allocation Personnalisée au Logement	110,00 €	99,00 €	- 11,00 €
Prime d’activité	387,00 €	382,00 €	- 5,00 €
Net annuel touché	29 607,00 €	28 884,00 €	- 723,00 €

On voit ici qu’au lieu de gagner 40 € de plus par mois, le ménage en perd 60 € par mois par rapport à la situation précédente… Cette perte est expliquée à 75 % par la perte de la bourse lycée pour les deux enfants, qui possède un effet de seuil très brutal démultiplié par le nombre de personnes à charge qui en bénéficient.

Que nous apprend donc cet exemple ? Premièrement, qu’un seuil linéaire similaire à celui utilisé pour les allocations familiales devrait être généralisé à toutes les allocations afin d’éviter ce genre de situations. Deuxièmement, que c’est une combinaison de facteurs très précise qui déclenche cette situation : deux enfants au lycée en même temps, et un niveau de salaire autour de 1750 € net. Le concubinage, qui rajoute une hausse d’impôts expliquant 11 % de la perte d’argent, n’est pas le facteur central mais concerne quand même 20 % des français.

Cet exemple aurait pu être découvert à partir d’une étude classique sur des données réelles, mais aurait supposé un vaste échantillon pour tomber dessus par hasard. Un des atouts de cette nouvelle méthode d’analyse par rapport à l’état de l’art est donc de découvrir efficacement, de manière fiable et sans aucune donnée secrète les cas limites indésirables induits par le système socio-fiscal.

Le solveur SMT pourrait également être utilisé pour trouver la pente linéaire exacte à donner à la bourse afin d’éviter un taux marginal trop élevé. Mais que veut-dire « trop élevé » ? 70 % ? Plus ? Moins ? De plus, l’effet de seuil est ici démultiplié par le nombre d’enfants : pour maintenir un taux marginal faible autour du seuil, il faudrait une pente linéaire d’autant plus faible que l’on souhaite couvrir des familles plus nombreuses. On voit ici qu’il y a un arbitrage politique de haut niveau à faire : qu’est-ce que l’on juge acceptable ? Une fois cet arbitrage fait, le solveur SMT permet de garantir si la réalité de la formule de calcul est en accord avec les principes décidés par le législateur.

Je n’ai présenté ici qu’une seule méthode d’interroger le modèle encodé dans le solveur SMT. En fait, il est possible de poser n’importe quelle question de la forme « Existe-t-il une situation telle que … ? ». Quelques exemples d’applications possibles, fort intéressants d’un point de vue d’évaluation des politiques publiques :

• « Est-il possible pour un ménage de gagner/perdre plus de $x$ € à la suite de la réforme fiscale de cette année ? »
• « Est-il possible d’augmenter le taux de la deuxième tranche d’imposition de plus de 5 points sans qu’aucun ménage ne perde plus de 200 € par an ? »
• En supposant avoir encodé dans le solveur SMT un histogramme de la distribution de revenus, « Est-il possible de jouer sur les taux des tranches et de la décote de manière à percevoir 5 milliards d’euros par an en plus sans qu’aucun ménage ne voie son impôt augmenter de 3 % de ses revenus ? »

Science ou fiction ? Le prouveur automatique n’est pas magique, et plus le problème est complexe, plus sa résolution prend du temps et des ressources. Mon prototype actuel peut déjà consommer plus de 100 Go de RAM et tourner plusieurs jours ; la question du passage à l’échelle vers des questions plus compliquée représente donc un vrai défi technique. Mais les méthodes formelles ont plus d’un tour dans leur sac, et vont nous aider à nouveau pour présenter au SMT un problème réduit à sa substantifique moelle, débarrassé de toute complexité superflue.

Une implémentation du calcul de l’impôt formalisée

Il est déjà possible de faire beaucoup de choses avec un petit prototype comme celui que j’ai développé. Cependant, idéalement, on voudrait disposer de la fonction qui calcule l’impôt dans tous les cas de figures, pour tous types de revenus et de statuts, avec avec toutes les niches fiscales. Or, il existe déjà un programme informatique qui réalise cette tâche : celui qui est utilisé par la Direction Générale des Finances Publiques (DGFiP) pour calculer votre avis d’imposition !

Depuis la loi n° 2016-1321 du 7 octobre 2016 « pour une République numérique », le code source utilisé par une administration est considéré comme un document administratif soumis au droit d’accès et à la réutilisation publique. Le code implémentant le calcul des impôts a donc été publié par la DGFiP en 2016, à l’occasion d’un hackathon qui a vu émerger quelques idées intéressantes. Vous pouvez vous-même aller inspecter le code sur le dépôt officiel de la DGFiP. Il n’y a plus qu’à l’utiliser alors ? Pas vraiment.

En effet, le code est écrit dans un langage de programmation spécial, appelé « M » pour « Macro-langage ». C’est un langage développé par et pour la DGFiP pour l’écriture de l’implémentation du code des impôts modifié chaque année lors du vote du budget. Or à ce jour, la DGFiP n’a pas mis à disposition du public l’outillage qu’elle utilise pour exécuter ce code M. Le code est-il inutilisable pour autant ? En 2016, Etalab a publié un parseur pour le langage M, capable de traduire le code source M vers un abre de syntaxe abstrait qu’il est possible d’interpréter en Python. J’ai pu reproduire les études menées en 2016 à l’occasion du hackathon en utilisant moi-même ce parseur, mais j’ai également pu constater quelques problèmes. D’abord, le montant de l’impôt calculé avec le parseur était parfois faux, notamment lorsque le montant final devait prendre en compte le plafonnement d’un avantage fiscal ou du quotient familial. Mais plus problématique, ce parseur n’a pas été écrit avec pour objectif de donner une sémantique précise au langage M : les opérateurs M de l’arbre de syntaxe abstrait sont simplement remplacés lors de l’exécution par des opérateurs Python correspondant.

Pourquoi cela n’est-il pas suffisant ? Il faut se rappeler notre objectif : au delà de la simple exécution du code M, nous voulons aussi le traduire vers un prouveur automatique pour répliquer les résultats de notre prototype dans le cas général. Pour cela, il nous faut savoir exactement comment s’exécutent les programmes M dans tous les cas possibles. Cette connaissance porte un nom précis en étude des langages de programmation ; il s’agit de donner une sémantique au langage M. C’est donc ce que je me suis attelé à faire, en utilisant un mélange de rétro-ingénierie et d’informations supplémentaires qui m’ont été données par la DGFiP, avec laquelle j’ai pu régulièrement échanger pendant plusieurs mois. Ce travail a débouché sur deux choses :

• une sémantique formelle du langage M, présentée dans un article de recherche;
• un compilateur pour le langage M, Mlang, basé sur cette sémantique.

Je tiens à remercier pour leur aide précieuse :

• Raphaël Monat, doctorant au LiP6 et co-auteur de Mlang ;
• Christophe Gaie et tous ses collaborateurs de l’équipe SI-1E de la DGFiP, qui ont répondu avec bonne volonté à mes demandes d’information sur le langage M.

Pourquoi est-il important que le compilateur soit basé sur une sémantique formelle ? Car cette sémantique va nous permettre de valider les traductions du langage M vers d’autres langages de programmation. Par exemple, Mlang permet de générer statiquement une fonction Python qui reproduit le calcul de l’impôt tel qu’il est fait sur le simulateur officiel de la DGFiP. Quel différence avec le parseur précédemment écrit par Etalab ?

Je me suis aperçu que le langage M possédait une valeur spéciale, indéfini. Dans le parseur Etalab, indéfini est traduit par la valeur 0. Cependant, le travail de réalisation de la sémantique formelle a permis de réveler que indéfini ne se comportait pas comme 0 dans tous les cas : par exemple, la comparaison avec indéfini donne toujours indéfini (et non pas le résultat de la comparaison avec 0). Ces petits détails rendent le compilateur beaucoup plus robuste et augmentent le niveau d’assurance que l’on a sur les fichiers générés à partir du code M grâce à Mlang. Plus précisément, cela réduit le risque que le programme généré s’exécute différemment que le code M.

Au moment où ce billet est publié, le code généré par Mlang est cependant toujours faux. En effet, un effet secondaire de ce travail de formalisation et de validation a été de découvrir que le code M publié par la DGFiP ne contient pas toutes les informations nécessaires à répliquer le calcul de l’impôt. Techniquement, le code M est appelé plusieurs fois avec des valeurs particulières pour certaines variables. Cette subtilité technique n’avait pas été détectée au moment du hackathon et de la première publication du code. J’ai pu en informer la DGFiP, qui met actuellement des moyens en œuvre pour me permettre de récupérer dans leur système les informations concernant ces appels multiples du code M avec différents paramètres. Une fois ces informations récupérées, je pourrai achever le travail de formalisation et valider Mlang sur les jeux de tests officiels de la DGFiP.

Conclusion : à chaque application son implémentation du code des impôts ?

Le code M produit et publié chaque année par la DGFiP à l’issue du vote de la loi fiscale va ainsi pouvoir servir de base à tout une série d’implémentations de tout ou partie du code des impôts insérées dans diverses applications. En effet, Mlang offre la possibilité de générer à partir du code M et vers divers langages de programmation des programmes calculant une liste de variables de sorties en fonction d’une liste de variables d’entrées et de conditions spécifiques. Concrètement, si LexImpact a besoin d’une implémentation Javascript ou WebAssembly de la fonction qui calcule l’impôt de cas types en fonction des valeurs des tranches d’imposition, Mlang pourra la générer ! Dans ce cas précis, le calcul de l’impôt pourra même se faire dans le navigateur Internet et non sur un serveur.

Une autre application intéressante serait la traduction du code M vers des langages de simulation macro-économique comme TROLL ou SAS. En effet, ces langages sont utilisés par l’Insee afin de réaliser des modèles de l’économie française qui ont besoin de l’expression mathématique de l’impôt sur le revenu. Ces modèles pourraient donc chaque année se mettre à jour en récupérant la nouvelle version du code M compilée vers TROLL ou SAS, au lieu de devoir refléter eux aussi les changements de législation dans leur code.

Enfin, Mlang va pouvoir améliorer notre prototype de prouveur automatique du code des impôts. En effet, avant de le traduire vers un solveur SMT, il est nécessaire de réduire la complexité mathématique de la fonction à sa substantifique moelle pour éviter de faire exploser la consommation de ressources du solveur. Le cadre du compilateur Mlang et la sémantique formelle de M nous permettent de réaliser des optimisations fiables qui vont simplifier le programme sans en changer le sens, avec ou sans conditions supplémentaires. Au delà des optimisations classiques telles que l’élimination de code mort, il est aussi prévu d’utiliser l’outil d’interprétation abstraite MOPSA afin d’effectuer une analyse plus fine du programme. Raphaël Monat et moi espérons que, combinée à des stratégies de division de requêtes en sous-problème, cette optimisation du code M nous permette de faire passer à l’échelle notre prototype de preuve automatique de théorèmes sur le code des impôts.

Au delà de l’aventure technique, je pense qu’il y a plusieurs leçons à retirer de cette histoire. Premièrement, c’est le libre accès à la recherche et au code qui permet aux synergies et aux initiatives inhabituelles de se développer. La DGFiP est la première administration au monde à publier ainsi son implémentation du calcul de l’impôt, et je pense que ce projet apportera rapidement à cette administration des retombées positives. Tout mon code est également publié sous licence libre, car il est important qu’un outil qui permette l’analyse fine et automatisée de la fiscalité française soit accessible à toutes et tous, et non pas réservé à un acteur privé qui l’utiliserait pour son propre profit. Deuxièmement, je pense que ce projet montre une fois de plus que l’innovation vient souvent d’un travail de recherche fondamentale mené sur le long terme. Les outils utilisés ici (comme le prouveur Z3) ont des fondements théoriques solides établis sur des dizaines d’années, et je me tiens bien sûr sur les épaules de géants. J’espère que cet exemple d’application des méthodes formelles pourra attirer l’attention sur ce domaine peu marketable en ces temps de course à « l’intelligence artificielle ». Troisièmement et pour terminer, ma volonté avec ce projet est aussi de montrer que l’innovation peut aussi profiter directement au secteur public. Je salue ainsi l’existence du programme des entrepreneurs d’intérêt général dont fait partie l’initiative LexImpact. Un tel programme ne pourrait selon moi que gagner à se rapprocher de la recherche appliquée menée également pour l’intérêt général dans les laboratoires français. Alors que la perspective d’une carrière dans la recherche publique semble si morose pour nombre de jeunes gens très qualifiés, l’idée de pouvoir utiliser ses connaissances pour améliorer l’action de l’État me semblerait être un moteur puissant à utiliser afin d’éviter la fuite des cerveaux vers un secteur privé dont les activités, surtout dans le domaine de la tech, manquent parfois de sens.