Law and Flexible Formalizations

Changing technologies render tax law’s intricacy legible in new ways. Advances in large language models, natural language processing, and programming languages designed for the domain of tax law make formalizations of tax law that capture much of its substance and structure both possible and realistic. These new formalizations can be used for many different purposes—what one might call flexible formalizations. Flexible formalizations will make law subject to computational analysis, permitting statutes to be tested for consistency for consistency and unintended outcomes, and allowing automated explanations of reasoning with formalizations.

This post builds upon existing work in computational law and digitalizing legislation. Flexible formalizations are not AI in the sense of big data or machine learning. But machine learning might help produce flexible formalizations, and blending rule-based computation with machine learning could change both substantive tax law and tax enforcement and administration more powerfully than either alone. While this post focuses on tax law, similar considerations would come into play for any rule-based, complex area of law.

Tax law in the United States has long been formalized in, for example, IRS forms, which provide computational steps for taxpayers to follow in order to comply with the law. But these are rigid formalizations: they reduce the law to algorithms in a way that is useful only or primarily for the precise purpose for which the formalizations were created. In contrast, flexible formalizations are formalizations of law that are not tailored to a particular use but rather serve as the underpinning of any kind of task for which formalization or computer analysis is helpful. The envisioned formalizations would be machine executable, not just machine readable. Additionally, the law should be formalized using formal methods. The balance of this post focuses not on the mechanics or implementation of flexible formalizations, but rather on how this formalization will or should shape the law.

I am not, of course, arguing that law should be, or even could be, entirely computer code. Some parts of the law are usefully formalized, and some are not. Some laws suggest, benefit from, or even require algorithms to be implemented, but law is more than just algorithms. However, formalizing law as part of the drafting process for tax laws could have significant benefits.

Tax statutes, like other statutes, contain intended ambiguities (such as the meaning of a term like ‘gift’). Intended ambiguities are entirely consistent with formalizing law, and ambiguities will remain even after the law is formalized. One common way to handle a term with an ambiguous meaning is to leave the term as an input. The formalization might take no position on what, for example, constitutes a gift; it would simply have a place for the user to enter the amount of the gift, once the person figures out what that number should be using the instructions to the form or other guidance. This is the current approach on tax forms for various arguably ambiguous terms.

Tax statutes, however, also sometimes contain what seem to be unintended ambiguities (such as the order in which calculations are supposed to be performed, or whether a particular portion of the statute is part of a “definition”). Often, the statutes cannot be applied at all without resolving these ambiguities. Tax statutes also sometimes contain outright errors. If Congress formalizes proposed legislation as part of the drafting process, many of these ambiguities and errors, which now must be corrected by administrative agencies or courts, could be detected and fixed before the law is ever enacted.

Formalizing tax law could also make tax avoidance and evasion easier for taxpayers. If the law becomes executable by computer, the marginal cost of developing a new tax shelter could drop to essentially nothing, with potentially enormous costs to the government and the disc. Removing complexity as a friction slowing down the development of tax shelters will therefore require changes to the law surrounding tax shelters.

One possible response would be for the government to use the formalizations to generate tax shelters, before ever spotting them ‘in the wild,’ for the purpose of banning them. Congress could give Treasury direct authority to generate and ban the shelters. The government could also potentially use the formalizations to spot previously unidentified tax shelters when reviewing returns.

Congress could also use these formalizations to prevent laws that create the potential for tax shelters from ever being enacted. Congress could check how envisioned changes would interact with the rest of tax law, determine whether proposed legislation would create opportunities for tax shelters, and modify the language of the statute to avoid those shelters.

It would, however, be ineffective and inadvisable to try to ban computer-created tax shelters. Computers will be used to generate tax shelters; they may already be being used to generate tax shelters. It would be nearly impossible to define what using a computer to generate a shelter means. And it would be incredibly difficult if not impossible to prove whether a computer had been used even if a definition of ‘using a computer’ or ‘using AI’ could be determined.

Flexible formalizations could also reduce administrative costs. For example, the Internal Revenue Service often must create new forms when new law is passed. If the law were already formalized, no additional work would be needed to convert the law into algorithms. Taxpayers could simply use a computer program to enter whatever inputs were necessary. This approach might appear to reduce transparency: the numbers go in, and the answer pops out—with no sense of what calculations are being executed. However, the vast majority of taxpayers file electronically and thus already have the experience of putting numbers in and getting an answer out, with no actual computations on the part of the human being.

Moreover, flexible formalization could increase transparency. The computer code underlying the calculations should be completely public and transparent. And beyond that, as the computer code itself would remain impenetrable to many people, the computer code could be used to create explanations, written in a style as technical or nontechnical as desired, that could accompany the numerical bottom-line output. Formal methods, unlike generative AI, are not deterministic, not probabilistic. Formal proofs—that is, machine generated proofs—can therefore be used to generate natural-language descriptions of the steps the program has taken to reach its conclusions.

Flexible formalizations may well lead to even greater tax complexity. But flexible formalizations could also mean that even as provisions became complex, drafters who formalized the legislation can be confident that the different parts of the provision fit together and that the provision fits with the overall law. Lawmakers can test out different formalizations, looking for consistency within the law and confirming that the outcome of the proposed provisions is as desired.

Finally, to take full advantage of the potential of flexible formalization, and to avoid the dangers of formalization residing only in private hands, the government should develop the ability in-house to formalize the law and to use these formalizations fully. Any formalizations should also be public, so that the general public can help test, challenge, and improve those formalizations. The relevant expertise will thus be located within the government itself as well as with the public—a people’s formalization.

Sarah B. Lawsky is Howard Friedman '64 JD Professor of Law at Northwestern Pritzker School of Law.

This post is published as part of the series ‘How AI Will Change the Law’.