Changing the frame: Formal modeling with LLM assistance, Part 2
Blog / Opinion essays
The first part of this essay offers a vision of how to adapt our practices of formal modeling to the new kind of automation, potent but unpredictable, made possible by LLMs. In that part, several paradigms of formal modeling are analyzed from a distance, guided by the metaphor of more or less constrained frames. In this second and final part, a single paradigm—spreadsheet-like data modeling—is examined more closely. The ideal of formal modeling that is constrained but fluid is made vivid through a concrete example and a working demonstration in CatColab.1
Case study: Structuring spreadsheets
The most widely used software tool for formal modeling ever created, the spreadsheet enables people who might otherwise never encounter formal models to interactively create their own and explore the implications. It is a highly successful and empowering abstraction, used by both individuals and organizations. It is also a notorious source of ill-specified, unreliable processes.
We envision a spreadsheet-like tool that enables transforming not only the data but a frame constraining the data.
Adopting the frame metaphor from Part 1, spreadsheets exist within a fixed, unconstrained frame,2 with all of the conveniences and pitfalls that entails. We envision a spreadsheet-like tool that enables creating and transforming not only the data but a frame that constrains the data.
The idea of constrained data modeling has an obvious precedent: the relational database, another very successful species of software. Using a relational database, the modeler defines a frame via a schema. In the most common incarnation of a relational database as a SQL database, a schema specifies types of entities (tables) with data attributes (columns), as well as functional relations (foreign keys) between entity types. Once a schema is defined, the database system checks that the instance of the schema, given by actual tables of data, conforms to the schema, raising an error if a proposed transaction would violate any constraints. It is a testament to their utility and soundness that SQL databases have enjoyed such a long lifespan, existing in nearly the same form for forty years, when so many other computing technologies have endlessly churned while progressing only falteringly.
Although SQL databases are, from a strictly logical standpoint, more powerful than spreadsheets, the two kinds of tool have little overlap in users and usage. There are more and less deep reasons for this. Certainly, SQL databases are harder to use than spreadsheets. Users of SQL databases, mostly programmers, interact with the database using the SQL language, a domain-specific programming language, while spreadsheets provide an intuitive graphical interface based on direct manipulation. This is practically important, and in our work on structured spreadsheets, we aim to create interfaces that allow and encourage direct manipulation.
But the more fundamental reason that SQL databases are not a substitute for spreadsheets is that SQL databases are rigid where spreadsheets are fluid. SQL provides powerful languages to define schemas and query instances, but a far more limited language to change schemas. Database migrations usually comprise an ad hoc mix of SQL statements and generic code in an orchestrating programming language. Migrations are a frequent source of frustration even for professional engineers, who try to avoid changing their schemas whenever they can get away with it. In short, SQL databases make it easy to define a frame but hard to change the frame.
Such situations are typical across science and engineering: experts know well their objects of study and often devise sophisticated formalisms for them, but tend to undertheorize the relations between objects.3 Category theory encourages us to take relations seriously by not introducing a class of objects without also considering the morphisms between them. In the case of relational databases, formulating a category-theoretic account of schemas leads directly to a notion of morphism between schemas (in fact, several such notions). A morphism between schemas, defined declaratively, then induces a data migration between instances over those schemas.4
The vignettes that follow illustrate how constrained yet fluid modeling with tabular data enables more intelligible and predictable automation with LLM agents. We will not enter into technical details about the underlying mathematics and technology, which are being actively developed. Rather, the aim is to convey a sense of what is possible through examination of a concrete scenario.
Example: the DB1B dataset
Relational data is often artificially flattened into a smaller number of tables or even a single table, in deference to the dominant abstraction in data science, the data frame.5 A typical example is the DB1B dataset, a random sample of flight itineraries from reporting carriers, published quarterly as a set of three CSV files by the U.S. Bureau of Transportation Statistics. The intended schema for the data is conveniently summarized by a third-party note about airline industry datasets.
The three tables correspond to three types of entities, all related to itineraries: “tickets” (Ticket), covering the whole itinerary; “markets” (Market), covering a single direction of a ticket; and “coupons” (Coupon), covering individual flights.6 The entity types are linked by three mappings (foreign keys), as expressed by the diagram:
In addition, each entity type has a couple dozen data attributes. The data as provided looks like this:
We’ll proceed in three phases: inferring an initial frame for the data, then tightening the constraints set by the frame, and finally changing the frame more drastically from its original, implicit schema.
Inferring an initial frame
Given the three CSV files, we could prompt the LLM generically to “infer an appropriate schema for the data, then import the data” and hope for the best. That may well produce a decent result,7 but what would we learn from it? Instead, we pursue a more incremental and interactive strategy, starting with the loose frame advertised directly by the source material, then gradually building our understanding of the data and reifying that understanding by tightening the frame.
So we ask the LLM to “create a schema for the data capturing the stated foreign key relations and including all other columns as string-valued data attributes.” Since the columns in CSV files are untyped, the latter stipulation is safest for an initial frame. We also ask the LLM to import the data itself as an instance of the schema.
Even under this minimalist frame, it is already possible that the data could fail to conform to the schema by having links to entities that don’t exist. Since the DB1B data was presumably exported from a relational database enforcing foreign key constraints, we don’t expect that to happen, but it could happen if the random sampling were inconsistent with the relational structure. In any case, once the data is imported, the validity of the links will be automatically checked—not by the LLM, but by the type checker for instances, which is perfectly reliable. In our system, the LLM must propose changes to the schema and the instance in joint transactions that will be rejected unless the instance satisfies the constraints stated by the schema.
The successful result of the schema creation and data import is shown in the screenshots below.
Tightening the frame
Having set an initial frame and imported the data, we strengthen our understanding of the implicit model by attempting to add more constraints to the frame.
First of all, while it may not be obvious from the nomenclature, the entity types—Coupon, Market, and Ticket—form a hierarchy. Each ticket contains some number of markets, and each market contains some number of coupons. The hierarchy implies that, for each coupon, the ticket to which the coupon is attached should be equal to the coupon’s market’s ticket. We can state this logical requirement as a diagram (“the triangle commutes”):
Equivalently, as an equation in textual syntax:
\mathtt{MktID} \mathbin{⨟}\mathtt{ItinID} = \mathtt{ItinID} : \boxed{\mathtt{Coupon}} \to \boxed{\mathtt{Ticket}}
When we add this path equation to the schema, the type checker will verify whether it holds in the instance. Assuming it does, we can keep the equation as a constraint that should apply to any future data. Here’s what the equation looks like when added in CatColab:
Better, though, is to observe that the equation makes the ItinID column of Coupon logically redundant, since it can always be computed by following the links through Market to Ticket. So we can save on physical storage and avoid logical redundancy by deleting the ItinID column of Coupon entirely. There is no disadvantage to doing so, since we can reintroduce it as a definition
\mathtt{CouponItinID} \mathrel{\vcenter{:}}=\mathtt{MktID} \mathbin{⨟}\mathtt{ItinID} : \boxed{\mathtt{Coupon}} \to \boxed{\mathtt{Ticket}}
that will be computed on demand and updated automatically when the data changes. In a spreadsheet, such a definition is called a formula; in a relational database, a view.
Redundancies can also be found in the data attributes. One such constraint is helpfully if informally noted in the third-party summary:
Carriers report complete itineraries so this [reporting carrier code] should be equal for all markets and coupons in an itinerary.
Or, formally:
Experiments show that LLMs are adept at identifying plausible constraints, a useful complement to human inspection. Many, but not all, of the proposed constraints actually validate against the data. Some are more complex than path equations, involving aggregations or injectivity/surjectivity constraints. For example, every ticket has at least one market, and every market has at least one coupon. These are surjectivity constraints, denoted graphically by double-headed arrows:
Another important vector to tighten the frame is setting stronger types on the data attributes, rather than making them all strings. Some attributes should plainly be (positive) integers (Year, Quarter), (nonnegative) real numbers (Distance, MilesFlown), or booleans (RoundTrip, BulkFare). In this data, booleans are encoded as indicator variables (0 or 1), requiring a modest amount of common sense on the part of the human or LLM to distinguish them from integers. In all cases the type conversions are automatically checked against the instance data, and any type errors are reported.
A fragment of the typed data attributes at this stage, along with the LLM’s summary of its typing decisions, is shown below.
Changing the frame
So far, we have reified and tested hypotheses about the model by introducing types and constraints and eliminating redundant data, while keeping intact the basic entity-relation structure suggested by the original data. There are good reasons to alter the frame more drastically.
Inspecting the current schema, the experienced modeler of relational data will be struck that, in each table, the origin and destination airports are represented not only by a single column (Origin or Dest) but also by many attributes of the airport (e.g. OriginCityNum, OriginCountry, OriginState). This flattening of the same relational data across many tables is messy, inefficient, and error-prone. Good modeling practice suggests that we should reify the airports as a new type of entity (Airport) with data attributes of its own. The schema would then look something like:
One might then notice that several attributes of the U.S. state (e.g. Fips and Wac) are redundantly flattened into Airport, motivating the creation of another new type of entity (State) with its own attributes.
With a little common sense, changing the schema and migrating the data should be a straightforward if tedious job. We instruct the LLM to “refactor the schema and data instance by creating new Airport and State entities and factoring the appropriate data attributes through mappings to the new entities.” Excerpts of the two new tables, along with the LLM’s summary of its changes, are shown in the screenshots below.
While the schema is objectively improved on one measure—it is more “normal,” in the sense of relational database theory—we should not lose sight of the subjective nature of modeling. For example, rather than creating a dedicated table for U.S. states, we could take the position that these various names and codes for states, redundant as identifiers, have no place in a database about flight itineraries. We could drop them entirely and refer to states only by, say, their standard two-letter codes. Neither schema is more correct than the other, and a good tool for data modeling should not make us pay a heavy price for changing our minds.
Outlook
These vignettes show some of the potential for how LLMs, possessing the “common sense” of world-scale statistical models, can both be constrained by, and aid in finding constraints for, formal models. Reflecting the embryonic state of the work, this essay has many notable omissions, of which we highlight two. First, although the LLM is only permitted to modify the schema and instance through valid transactions, that the instance is valid according to the schema does not imply that either is substantively correct. Proposals from the LLM should be presented with structured diffs, based on version control. Second, the changes should themselves be formalized as morphisms between mathematical objects: currently, the LLM mutates the model through an imperative scripting interface; instead, it should write a migration in the sense of categorical database theory, which can then be tracked and reviewed like other formal artifacts. We will explore these and other directions as we seek a renaissance for formal modeling in a world where the means of producing models is rapidly changing.
References
Carlson, Kevin, and Evan Patterson. 2026. “Presheaves on Lax Double Functors; or, Instances of Models of Double Theories.” Applied Categorical Structures 34 (30). https://doi.org/10.1007/s10485-026-09866-y.
Johnson, Michael, Robert Rosebrugh, and R. J. Wood. 2002. “Entity-Relationship-Attribute Designs and Sketches.” Theory and Applications of Categories 10 (3): 94–112.
Lambert, Michael, and Evan Patterson. 2025. “Representing Knowledge and Querying Data Using Double-Functorial Semantics.” Electronic Proceedings in Theoretical Computer Science 429: 174–89. https://doi.org/10.4204/EPTCS.429.9.
Patterson, Evan, Owen Lynch, and James Fairbanks. 2022. “Categorical Data Structures for Technical Computing.” Compositionality 4 (5). https://doi.org/10.32408/compositionality-4-5.
Schultz, Patrick, David I. Spivak, Christina Vasilakopoulou, and Ryan Wisnesky. 2017. “Algebraic Databases.” Theory and Applications of Categories 32 (16): 547–619. https://arxiv.org/abs/1602.03501.
Spivak, David I. 2012. “Functorial Data Migration.” Information and Computation 217: 31–51. https://doi.org/10.1016/j.ic.2012.05.001.
Spivak, David I., and Robert E. Kent. 2012. “Ologs: A Categorical Framework for Knowledge Representation.” PLoS ONE 7 (1): e24274. https://doi.org/10.1371/journal.pone.0024274.
Footnotes
At the time of this writing, the main functionality presented in this essay is implemented and running live on the CatColab staging server. We caution that its current status is that of research software not fit for serious use. Still, if you’d like to try it out, you can do so by going to
next.catcolab.org. First, create an account, log in, and enable LLM integration in the user settings. Then, make a new model and set the model type to “Schema”. Finally, create an instance of the schema and an LLM conversation on either the schema or the instance. From there you can try replicating this scenario or running your own experiments. Good luck! In the coming months, we will release a more polished version of this functionality tocatcolab.org.↩︎Without being too precise, this frame is an infinite but finitely supported list of sheets. Each sheet contains an infinite but finitely supported grid of cells, and each cell contains a literal value or is computed by a formula referencing other cells.↩︎
This may seem a strange thing to say about relational databases, but note the level shift: relations in a schema are central to the standard formalism, but we are talking about relations between schemas.↩︎
Categorical databases and functorial migrations have long been studied by applied category theorists (Johnson, Rosebrugh, and Wood 2002; Spivak 2012; Schultz et al. 2017; Lambert and Patterson 2025; Carlson and Patterson 2026). Technology realizing this theory consistent with its philosophy (cf. Spivak and Kent 2012) has been slower to develop. In past work (Patterson, Lynch, and Fairbanks 2022), we implemented categorical databases (ACSets.jl) and functorial data migrations (DataMigrations.jl) as in-memory data structures and embedded DSLs in the Julia programming language. While it makes creating and changing schemas lighter weight than in SQL, this software suffers from usability problems of its own, even for its intended audience of programmers. Our present effort aims to demonstrate the potential of fluid formal modeling with relational data to non-specialists.↩︎
A “data frame” is a columnar data table, popularized by the R programming language and software packages like
pandasfor Python.↩︎The words “ticket,” “market,” and “coupon” are quoted because in the DB1B dataset they are used as airline industry jargon that may not align with their everyday use. The literate interface for defining schemas in CatColab encourages documenting the meaning of these terms in plain English.↩︎
Experience shows that a contemporary LLM will produce a decent result with minimal prompting. In fact, it will often go beyond what is explicitly asked to fully normalize the relational data. This quality of “over-eagerness,” variously a source of delight and irritation, seems to be a consequence of how LLMs are post-trained, rather than an inherent property of the technology.↩︎