Changing the frame: formal modeling with LLM assistance

Introduction

Frames and formal models today

A wide swathe of technical creative activity, from creating scientific models and engineering designs to writing computer programs to making spreadsheets, is aimed at expressing a model of something precisely enough to be operationalized on a computer. The model, or at least the part of it given algorithmic content, is thus in principle mathematizable. We will think of scientific models, engineering designs, computer programs, and spreadsheets all as kinds of formal models, even if the degree to which they are formalized mathematically varies in the current state of practice.

Any formal model exists within some frame,¹ defining the concepts and language within which the model is expressed and the rules to which this expression must conform. A typical frame for scientific modeling might be “a parameterized system of ordinary differential equations,” specific enough to unambiguously describe a class of models and to support uniform algorithms for fitting and simulation. The frame for a computer program is, to a first approximation, the programming language in which it’s written along with the ecosystem of libraries supporting it.

Frames can be more or less constrained. A relatively unconstrained frame has the obvious benefit of allowing creator flexibility to formally express their intent. A relatively constrained frame carries a more definite and opinionated viewpoint, stipulating stronger structure and assumptions. This makes it easier to say some things, while prohibiting the expression of other things. This is good to the extent that it blocks expressions that would be outright mistakes or, more subtly, would deviate from settled design decisions or conventions. Of course, it is bad to the extent that it prevents useful and desirable expressions not anticipated by the choice of frame.

Builders and users of computing technology seem to have revealed an overwhelming preference for unconstrained frames. From the beginning, the field of computing has, in its theory, emphasized the universality of programming languages; in its practice, language designers herald something more elusive, the “expressivity” of their languages. Meanwhile, the species of mathematized software most widely used by people who are not mathematicians or programmers—the spreadsheet—is highly unconstrained, a blank canvas for tabular data with no further requirements on data layout or typing. Advanced users can introduce their own logic, of arbitrary complexity, within cell formulas, which can vary across cells in arbitrary ways.

It is not hard to imagine what might lie behind this preference for unconstrained frames. Working in a constrained frame, if a creator reaches the boundary of the frame, they may be unable to express their intent at all within the formal model, an experience at best frustrating and at worst intolerable. In the most unconstrained frames, like a general-purpose programming language, it is usually possible to find some way to proceed, even if it involves blurring or subverting what were once crisp abstractions. Put simply, most people would rather muddle through than risk hitting an immovable wall.

Nevertheless, the costs borne under the status quo are severe, and growing. With the frame for the formal model having few hard constraints, the typical software project of even moderate complexity relies on a web of semi-formal and informal abstractions described by a mix of code and documentation but not fully specified by either. Rather, the abstractions are maintained—if they are maintained—by a shared understanding among the engineering team, created and renewed through careful communication. Competent programmers create bugs not by trivial logic errors but by failing to understand intricacies of what software abstractions assume or how they interact with each other.

As for spreadsheets, a notorious weakness of the spreadsheet frame is in transitioning from individual use to reliable organizational processes. Because the assumptions behind a spreadsheet are highly implicit, hidden within a web of cell dependencies and in the mind of the spreadsheet’s designer, it is all too easy to make ad hoc changes that silently break those assumptions. The lack of type constraints in spreadsheets is a frequent source of errors, including the perennial joke that Excel interprets every input it sees as a date. While different in many respects, what unites the standard paradigms for programming and spreadsheets is that by situating the formal model in a generic and unconstrained frame, the domain-specific abstractions that inevitably support the model possess little formal content; to compensate, disciplined human processes are required to safely use and change the model at any scale beyond a single person.

The effect of emerging LLM technology

Such is the status quo, an equilibrium beset by familiar problems but so far ultimately workable. New technology, in the form of generative machine learning based on LLMs, threatens the status quo by changing the tradeoffs involved. It also presents an opportunity to rethink how we design technologies for formal modeling.

In programming, the emergence of LLMs is decreasing the cost of generating more or less functional code, while exacerbating the challenge of maintaining a coherent set of abstractions and assumptions. The experienced programmer, when attempting to make a change, will notice when the change seems to depart from existing structures or assumptions and take the opportunity to rethink their approach, which can ultimately lead to revising past design decisions or changing the abstractions. The LLM, ever compliant, proceeds blithely along the path of least resistance. Moreover, while adept at mirroring surface-level patterns present in the codebase, the LLM is not privy to the web of shared mental representations that enable the effective engineering team to function.² Thus, at present, LLM coding agents appear to enable significant short-term productivity gains while gradually reducing the codebase’s overall concision and coherence. As LLMs become more prolific in office work, the lack of explicit structure and typing constraints in tools like spreadsheets will only exacerbate the fragility already present. In both cases, the distinction between creating, an active process that engages the mind and forces it to confront problems, and reviewing, a passive activity often experienced as boring, means that opportunities to catch mistakes or revisit assumptions are more likely to be missed when LLMs are heavily involved.

It has been suggested that the solution to this problem is that humans cease to interact directly with formal models at all. A formal model is useful, the thought goes, only insofar as it fulfills some externally validatable purpose; if it does so adequately, it does not matter how the model was constructed or how messy it might be internally. The LLM will mediate the interaction between the human and the formal model exclusively through natural language, so that the human never has to look inside.

Whether or not it is technically feasible, this vision misses much of the point of using formal models in the first place. Be they scientific models or computer programs or spreadsheets or abstract philosophical schemes, mathematical (or at least mathematizable) models have been among humanity’s most successful tools to augment our capacity for thinking. Not only does having good formal models increase our powers of deduction, prediction, and counterfactual reasoning, but the process of creating models forces us to sharpen and clarify our ideas, both for ourselves and to communicate with others. To abdicate a direct role in formal modeling would be to weaken human capability and agency.

The question then is not whether we should continue to directly interact with formal models but how the process of model building should adapt to a potent new source of automation and augmentation.

The future of formal modeling

All of the foregoing points to the same conclusion: that safe and reliable formal modeling pairing humans with LLM agents requires more constrained frames than are common today. Under our meaning of “frame,” this entails more than a Markdown file making vague suggestions; a frame specifies concepts, language, and assumptions that set the rules for formal modeling and are enforced when type checking a putative model.

How can we adopt more constrained frames while retaining the flexibility that has made the present paradigm of unconstrained modeling dominant? The question may seem paradoxical but the answer is, in a sense, simple: by insisting on more constrained frames, while making it possible to change the frame when needed.

It is easier to make this assertion than to say how it can be realized. Existing languages and tools that serve as frames for formal models tend to be very rigid. Changing them is costly and impractical. There are two reasons to believe that now is the right time to build more malleable tools for formal modeling.

First, as we have seen, LLMs have made it cheaper to generate code and other formal artifacts; consequently, they have made precise specification both more useful as input and more necessary to prevent abstraction drift. There is a growing recognition that existing practices must change. This recognition should create the will to explore new paradigms rather than tinker around the margins of existing ones.

Second, there is now a mature enough body of theoretical knowledge to actually create the new infrastructure that will allow fluidly defining and changing frames. This body of knowledge is broadly categorical logic, the intersection of category theory with mathematical logic and type theory. The role of logic and type theory as the mathematical underpinning for syntax in formal modeling is well known, and the use of categories as a denotational semantics for programming languages is familiar to experts. What is less appreciated, even among experts, is how category theory provides a meta-mathematical toolbox to enable modularity and reuse within and between frames, both in the narrow technical sense and in a more nebulous cultural sense affecting how we design formal languages. As we have noted, language designers have overwhelmingly sought to create ever more general and expressive languages, the ideal frame in which to say everything that can be said. This attitude is essentially reductionist. Category theory encourages us to see logic not as something prior to mathematics and science, but as a part of it, and to search for well-adapted mathematical universes in which to create models.³ These universes can look familiar, like functional programming or first-order logic, but can also natively encompass non-standard features crucial in certain domains, such as resource sensitivity, reversibility, nondeterminism, probability, and fallibility. Categorical logic offers a uniform technical toolbox to describe these paradigms without privileging any of them.

In the CatColab project, supported by the ARIA Safeguarded AI program, we are exploring this vision for scientific and cyberphysical modeling, programming in domain-specific logics, and tabular and relational data. It is beyond the scope of this post to describe these efforts in detail, nor do we claim to have a complete account of any of these vast topics. Rather, in the remainder of this post, we will hone in on one of the paradigms highlighted above—spreadsheet-like data modeling—as a case study in how to build tools, underpinned by categorical logic, that set constrained frames for formal modeling while also allowing the frame to be changed fluidly.

Case study: Structuring spreadsheets

Among the most successful species of software ever created, the spreadsheet enables people who might otherwise never encounter formal models to interactively build their own. It is also a notorious source of ill-specified, unreliable processes. Instead of taking the spreadsheet to exist within a fixed, unconstrained frame,⁴ we envision a spreadsheet-like tool that allows creating and transforming not just data itself but frames that constrain the data.

This idea has an obvious precedent: the relational database, another very successful type 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 checks that the instance of the schema, given by actual tables of data, conforms to the schema, raising an error if a transaction would violate the constraints. It is a testament to their utility and soundness that SQL databases have enjoyed such a long lifespan, in essentially the same form, when so many other computing technologies have endlessly churned.

While 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 formal 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 basic 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, and are a frequent source of frustration even for professional engineers. 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.⁵ 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 plethora of notions of morphism between schemas. A morphism between schemas, defined declaratively, then induces a data migration between instances over those schemas.⁶

The vignettes that follow illustrate how constrained yet fluid modeling with tabular data enables more reliable automation with LLM agents. We will not enter into technical details about the underlying mathematics and technology, which is being actively developed. Rather, the aim is to convey a sense of what is possible through concrete examples backed by working demonstrations.

Inferring an initial frame

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. As a typical example, consider 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.⁷ The entity types are linked by three mappings (foreign keys), as expressed by the diagram:

In addition, each of the entity types has a couple dozen data attributes.

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, 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 instead 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. The result is the schema shown in the diagram above, augmented with many data attributes of type String (not shown).

We then ask the LLM to import the data itself as an instance of the schema. Even under our 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 this data was presumably exported from a relational database enforcing foreign key constraints, we don’t expect this to happen, but it could still happen if, for example, the random sampling was not consistent 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—and any errant rows will be marked and reported.

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. This means 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{\boldsymbol{;}} \mathtt{ItinID} = \mathtt{ItinID} : \boxed{\mathtt{Coupon}\rule[-0.23em]{0pt}{0.23em}} \to \boxed{\mathtt{Ticket}\rule[-0.23em]{0pt}{0.23em}}$$

When we add this path equation to the schema, the type checker will confirm that it is true of the instance. Assuming it is, we can keep the equation as a constraint that should apply to any future data. 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 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} \coloneqq \mathtt{MktID} \mathbin{\boldsymbol{;}} \mathtt{ItinID} : \boxed{\mathtt{Coupon}\rule[-0.23em]{0pt}{0.23em}} \to \boxed{\mathtt{Ticket}\rule[-0.23em]{0pt}{0.23em}}$$

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 (footnote 1):

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 validate against the data, and 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 for tightening the frame is to set 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.

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 of the original semi-formal schema. We may wish 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 by a single column (Origin or Dest), but additionally 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.

With a little common sense, this should be a straightforward if tedious job, so we instruct the LLM to “refactor the schema by creating an Airport entity type with its own data attributes and factoring all information about origin/destination airports through maps to this new type.” A first check on this refactoring is by inspection of the target schema, which should look something like:

Notes

1. We will not attempt to be too precise about what is a “frame”—for us, a pre-theoretical concept—but the choice of word is intended to evoke both a “frame of reference,” meaning a chosen coordinate system or, more abstractly, a chosen point of view, and a “framework,” defined by Wikipedia as an “essential supporting structure on which other things are built.” ←

2. The use of Markdown files like AGENTS.md is a primitive means to mitigate this problem. ←

3. The evocative phrase “mathematical universe” we borrow from Ingo Blechschmidt’s paper on exploring “custom-tailored mathematical universes” using topos theory [Blechschmidt, 2022]. For technically minded readers, we remark that our usage is intended to encompass categorical-logical structures generally, not just toposes. ←

4. This frame is something like a countably infinite but finitely supported list of sheets. Each sheet contains a countably infinite but finitely supported grid of cells, and each cell contains a literal value or is computed by a formula referencing other cells. ←

5. 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. ←

6. Categorical databases and functorial migrations have been studied for the past fifteen years by applied category theorists [Spivak, 2012, Schultz et al., 2017, Lambert and Patterson, 2025, Carlson and Patterson, 2026], with a prehistory going back much further. Technology realizing this theory consistent with its philosophy (cf. [Spivak and Kent, 2012]) has been slower to develop. In past work [Patterson et al., 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. ←

7. 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. ←

References

Ingo Blechschmidt. Exploring mathematical objects from custom-tailored mathematical universes. In Gianluigi Oliveri, Claudio Ternullo, and Stefano Boscolo, editors, Objects, Structures, and Logics: FilMat Studies in the Philosophy of Mathematics, pages 63–95. Springer, 2022. doi:10.1007/978-3-030-84706-7_4. arXiv:2204.00948.

Kevin Carlson and Evan Patterson. Presheaves on lax double functors; or, Instances of models of double theories. Applied Categorical Structures, 34(30), 2026. doi:10.1007/s10485-026-09866-y. arXiv:2510.08861.

Michael Lambert and Evan Patterson. Representing knowledge and querying data using double-functorial semantics. Electronic Proceedings in Theoretical Computer Science, 429:174–189, 2025. doi:10.4204/EPTCS.429.9. arXiv:2403.19884.

Evan Patterson, Owen Lynch, and James Fairbanks. Categorical data structures for technical computing. Compositionality, 4(5), 2022. doi:10.32408/compositionality-4-5. arXiv:2106.04703.

Patrick Schultz, David I. Spivak, Christina Vasilakopoulou, and Ryan Wisnesky. Algebraic databases. Theory and Applications of Categories, 32(16):547–619, 2017. arXiv:1602.03501.

David I. Spivak and Robert E. Kent. Ologs: a categorical framework for knowledge representation. PLoS ONE, 7(1):e24274, 2012. doi:10.1371/journal.pone.0024274. arXiv:1102.1889.

David I. Spivak. Functorial data migration. Information and Computation, 217:31–51, 2012. doi:10.1016/j.ic.2012.05.001. arXiv:1009.1166.