Specification written in natural language

Natural language is less precise than one might think. Planning documents or specifications written in natural language have various limitations. The bottlenecks caused by these limitations are starting to stand out more clearly as the use of AI agents becomes routine.

Problems

It is difficult to express exactly what one has in mind. And even if one does express it accurately, the consequences often differ from what was expected.

“What you write down doesn’t mean exactly what you think it means. And when it does, it doesn’t have the consequences you expected.” —Daniel Jackson, Software Abstractions: Logic, Language, and Analysis

This has long been a problem, but I think this sentence pinpoints the bottleneck in the AI-human interaction loop that arises when instructing AI agents in natural language. (The book above has nothing to do with generative AI, but the quote fits so perfectly that I had to use it.)

Through a case of writing and improving a simple file system specification, I want to look at the limitations of specifications written in natural language, with a bit of exaggeration. I borrowed the example from Practical Alloy.

File system specification

A file system is a set of entities. File entities can store content. Directory entities can contain other files.

Most people already know what a file system is, what a file is, and what a directory is, so if you describe it like the above, they roughly get the idea. That is thanks to implicitly shared context. LLMs also generally understand it well because, thanks to pretraining data, they share similar context. (But because they understand it well only in a “general” sense, problems often arise. This is why you have to be careful when making wishes to Genie, the lamp spirit.)

To see how much implicitly shared context there is, how much information is omitted in a specification written in natural language, and how much room there is for interpreting that implicit context in “different ways,” what would happen if we interpreted the specification above with extreme rigor?

If we express the specification above as literally as possible in a modeling language called Alloy, it looks like this. (Even if you do not know Alloy syntax, it is fine as long as you can skim it and get the general feel, so there is no need to worry too much about it.)

// 파일 시스템은 엔티티의 집합
sig Entity {}

// 파일에 담길 내용
sig Content {}

// 파일은 엔티티의 일종. 내용을 담을 수 있음
sig File in Entity { content: one Content }

// 디렉토리는 엔티티의 일종. 다른 파일을 담을 수 있음
sig Dir in Entity { children: lone File }

If you “run” the specification above and ask it to show examples of file systems, numerous errors appear. The most obvious one is that there are entities that are both files and directories at the same time. That is because the specification never said an entity must not be both a file and a directory.

If, instead of the keyword in, we use extends, we can express that Dir and File are disjoint sets.

sig Dir extends Entity { children: lone File }
sig File extends Entity { content: one Content }

Running it again reveals another problem: there are entities that are neither directories nor files. That is because we never wrote that every entity is either a file or a directory. Using the keyword abstract lets us express the concept of a partition.

abstract sig Entity {}

Next problem: there is “content” that belongs to no file. We only said that files can contain content; we did not say that content cannot exist on its own without any file. Let us add fact and state that constraint explicitly.

fact 콘텐츠는_반드시_파일에_속해야_한다 {
	all c: Content | c in File.content
}

Next problem: there are files that belong to no directory. That is because we never said that every file must belong to a directory. We need to add fact.

fact 파일은_반드시_디렉토리에_속해야_한다 {
	all f: File | f in Dir.children
}

Next problem: there are files that belong to multiple directories at the same time. That is because we never said that a file must belong to only one directory. Let us modify fact.

fact 파일은_반드시_하나의_디렉토리에_속해야_한다 {
	all f: File | #children.f = 1
}

Next problem: a directory can contain no files or only one file. That is because we never said it can contain multiple files. Let us replace lone, the quantifier meaning 0 or 1, with set, the quantifier meaning 0 or more.

sig Dir extends Entity { children: set File }

Next problem: a directory cannot contain another directory. That is because the specification says a directory contains “files.” Let us fix that.

sig Dir extends Entity { children: set Entity }

Next problem: once we add the recursive relationship as above, we get directories that contain themselves. A constraint to prevent cycles can be expressed easily using the concept of transitive closure.

fact 순환은_존재하지_않는다 {
	no d: Dir | d in d.^children
}

Next problem: there are multiple root directories. Let us specify that there must be only one root directory. Actually, even that phrasing is not precise. Saying “there must be only one” does not imply “there must exist at least one.” If we want to state exactly what we mean, it is: “there must be exactly 1 root directory.”

one sig Root extends Dir {}

fact 루트를_제외한_모든_객체는_루트로부터_도달_가능하다 {
	Root.^children = Entity - Root
}

Next problem: there are directories that belong to multiple directories at the same time. Earlier we created the fact that “a file must belong to exactly one directory,” so let us revise that slightly.

fact 엔티티는_반드시_하나의_디렉토리에_속해야_한다 {
	all e: Entity | one children.e
}

After fixing it this way, we now get an error saying that such a file system cannot exist. That is because there is a contradiction in the specification: a root directory cannot have a parent directory (because the root is the topmost), but we also said that every entity (and a root is a kind of entity) must belong to exactly one directory. We need to change it to “every entity except the root.”

fact 루트를_제외한_엔티티는_반드시_하나의_디렉토리에_속해야_한다 {
	all e: Entity - Root | one children.e
}

Translating back into natural language

The original natural-language specification was this:

A file system is a set of entities. File entities can store content. Directory entities can contain other files.

The current specification written in Alloy is as follows.

abstract sig Entity {}

sig Dir extends Entity { children: set Entity }

sig Content {}

sig File extends Entity { content: one Content }

one sig Root extends Dir {}

fact 루트를_제외한_모든_객체는_루트로부터_도달_가능하다 {
	Root.^children = Entity - Root
}

fact 콘텐츠는_반드시_파일에_속해야_한다 {
	all c: Content | c in File.content
}

fact 루트를_제외한_엔티티는_반드시_하나의_디렉토리에_속해야_한다 {
	all e: Entity - Root | one children.e
}

fact 순환은_존재하지_않는다 {
	no d: Dir | d in d.^children
}

Let us translate this into natural language.

A file system is a set of entities. An entity is either a file or a directory, and no entity is both a file and a directory at the same time. A file always contains exactly 1 piece of content, and content cannot exist on its own without a file. A directory may be empty or may contain one or more other entities. A file system must have exactly one root directory, and every entity must be reachable from the root. A directory cannot recursively contain itself.

Improvements

Two improvements come to mind.

First, a model is not a model if it merely copies its subject as-is. A good model should selectively include only the important elements. The fact that “files contain content” is not central to this model, so it would be better to omit it.

Second, in the process of patching one problem after another in the specification, we ended up adding a bunch of constraints (fact), but in fact only two constraints are needed, and the rest follow logically from them (are implied). So it would be better to remove unnecessary constraints.

fact 루트를_제외한_모든_객체는_루트로부터_도달_가능하다 {
	Root.^children = Entity - Root
}

fact 부모는_최대_1개이다 {
	all f: Entity | lone children.f
}

To see whether the other constraints are in fact logically derivable while leaving only those two constraints, we can use check to check assertions (assert).

assert 루트를_제외한_모든_객체는_어딘가에_속한다 {
	all e: Entity - Root | one children.e
}

assert 루트는_어디에도_속하지_않는다 {
	no children.Root
}

assert 순환이_존재하지_않는다 {
	no d: Entity | d in d.^children
}

check 루트를_제외한_모든_객체는_어딘가에_속한다
check 루트는_어디에도_속하지_않는다
check 순환이_존재하지_않는다

If we run it, we can see the following message.

3 commands were executed. The results are:
#1: No counterexample found. 루트를_제외한_모든_객체는_어딘가에_속한다 may be valid.
#2: No counterexample found. 루트는_어디에도_속하지_않는다 may be valid.
#3: No counterexample found. 순환이_존재하지_않는다 may be valid.

This is not important in context, but if you are curious why it says “may be valid” rather than “is valid,” see small scope hypothesis.

Is this something to do in a human head?

This is a somewhat exaggerated example (for instance, the specification is deliberately written too vaguely), but let us list some lessons we can draw from it. What are the things that are essential for writing a good specification, yet difficult to overcome because of the limits of natural language?

Writing specifications concisely yet clearly
Quickly checking whether a specification has internal contradictions
Quickly checking whether two expressions are logically equivalent
Quickly checking whether the propositions implicitly entailed by a specification match what I expected

Using a formal modeling language does not immediately solve every problem, but I think it is one good means of gradually improving the situation. More important than the written specification itself (the result) is clear thinking during the process of writing the specification (the process), and I also think that this can gradually improve through the use of a rigorous language and rapid feedback.

The next-stage bottleneck

In modern society, to manage many schedules, you need a scheduling program. To perform complex calculations, you use an engineering calculator or a spreadsheet. Writing specifications or planning documents is also an extremely complex task, so we need tools that support the thinking process. But the tools we use when doing planning are, in most cases, PowerPoint or Figma. This is similar to a situation where someone doing complex calculations does not use a calculator, but only uses a tool that prettily renders formulas (for example, LaTeX). To use an analogy, what we need is not LaTeX but something like SymPy.

In the software development process, this problem did not stand out much until now because programming was the main bottleneck, but as that bottleneck begins to be removed by things like agent-based coding, I think the next-stage bottleneck is very likely to become planning.

Do planners need to learn Alloy?

Depending on the field, perhaps. But thanks to LLMs, it has become easy to convert natural-language specifications into Alloy code, so I do not think everyone necessarily needs to learn a modeling language. For example, one could imagine a semi-automated conversion procedure like the following.

A human enters a specification in natural language.
An LLM explains the ambiguous parts of the natural-language specification to the human in natural language, shows examples, refines its understanding of the human’s original intent more precisely, and progressively improves the Alloy code.
An LLM generates various cases (whether things that should happen according to the specification can actually happen, and whether things that should not happen according to the specification indeed do not happen), shows them to the human, and gets them verified.

If there were a tool that helped with specification writing through a process like this, it seems like it would also help train people to sharpen their thinking. I think sharpening one’s thinking is generally necessary not only for writing specifications but also for reducing the bottleneck in the AI-human interaction loop.

Related publications

Software Abstractions: Logic, Language, and Analysis
On the Effectiveness of Large Language Models in Writing Alloy Formulas
The Essence of Software
On the foolishness of natural language programming