Posts tagged research

Against Vibes: When is a Generative Model Useful

:: academia, research

Let’s suppose I wanted to answer a question: is the tool X useful for the task Y. If I were scientific about this, I would analyze the properties of tool X and develop a model, and the task Y and the requirements for it and develop a model, and I would use my models to predict the behaviour of tool X in the context of task Y. “Can I use timber instead of stainless steel as a support beam for this structure?” “Will this acid be an appropriate solvent for this reaction?” “Will this programming language provide these real-time guarantees?”

The discourse on generative models is not like this. Instead, you get claims like “software engineering is dead”, and attempts to shove generative models into literally everything without a thought. Search? Generative models. Code completion? Generative models. Summarization? Generative models. Voice to text? Generative models. Stock images? Generative models.

Any attempt to criticize this tends to go in circles and/or have people arguing past each other. Is a generative model useful for internet search? Well, look, it produces text that is plausibly related to the input prompt, so. So… what? That doesn’t answer the question. But the newest models are so much better! Better at.. what?

I was upset about this when it was being called “prompt engineering”, and found no sign of engineering, but instead a series of vibes about how to phrase a prompt in a particular version of a particular model, which sometimes produced output that is plausibly related to the input prompt and therefore plausibly close to what you might have intended. I’m upset now when people are making claims that agents are so useful, but can’t tell me when or why or how they’re useful beyond vibes about feeling more productive (vibes that have been refuted by real science contrasting objective measure of productivity vs. subjective reports), or examples of having produced a lot of plausible output.

(Okay, there are some researchers doing actual science and writing papers; I’m talking about the arguments being made as this stuff is integrating into schools, workplaces, etc.)

I want to know when generative models are useful. I don’t want to feel like they’re useful, that’s just a vibe. I’ve been a generative model skeptic basically from the beginning. I could not convince myself that generative models were useful. But I was also skeptical of my own subjective experience. I could imagine that a model capable of produce code from natural language would be useful, in some use cases that I had not found. I imagine there must be a model of when a generative model X is useful for task Y.

In this post, I’m not addressing ethical, political, or social questions. Those questions are important, and I want to address them separately from what the technology is capable of. Just for context: I think the widespread deployment of this technology is deeply problematic and irresponsible. I think further investment in it at its current scale is an almost criminal level of fiduciary negligence and will cause economic harm. I think the ethics of all of this are deeply troubling.

But for now, I just want to know what they’re technically capable of.

What is a model?

:: notes, research, academia

What is a model, particularly of a programming language? I’ve been struggling with this question a bit for some time. The word “model” is used a lot in my research area, and although I have successfully (by some metrics) read papers whose topic is models, used other peoples’ research on models, built models, and trained others to do all of this, I don’t really understand what a model is.

Before I get into a philosophical digression on what it even means to understand something, let’s ignore all that and try to discover what a model is from first principles.

What is syntax?

:: notes, research, academia

I’m in the middle of confronting my lack of knowledge about denotational semantics. One of the things that has confused me for so long about denotational semantics, which I didn’t even realize was confusing me, was the use of the word “syntax” (and, consequently, “semantics”).

For context, the contents of this note will be obvious to perhaps half of programming languages (PL) researchers. Perhaps half enter PL through math. That is not how I entered PL. I entered PL through software engineering. I was very interested in building beautiful software and systems; I still am. Until recently, I ran my own cloud infrastructure—mail, calendars, reminders, contacts, file syncing, remote git syncing. I still run some of it. I run secondary spam filtering over university email for people in my department, because out department’s email system is garbage. I am way better at building systems and writing software than math, but I’m interested in PL and logic and math nonetheless. Unfortunately, I lack lot of background and constantly struggle with a huge part, perhaps half, of PL research. The most advanced math course I took was Calculus 1. (well, I took a graduate recursion theory course too, but I think I passed that course because it was a grad course, not because I did well.)

So when I hear “syntax”, I think “oh sure. I know what that is. It’s the grammar of a programming language. The string, or more often the tree structure, used to represent the program text.”. And that led me to misunderstand half of programming languages research.

What is logical relations?

:: research, notes, academia

I have long struggled to understand what a logical relation is. This may come as a surprise, since I have used logical relations a bunch in my research, apparently successfully. I am not afraid to admit that despite that success, I didn’t really know what I was doing—I’m just good at pattern recognition and replication. I’m basically a machine learning algorithm.

So I finally decided to dive deep and figure it out: what is a logical relation?

As with my previous note on realizability, this is a copy of my personal notebook on the subject, which is NOT AUTHORITATIVE, but maybe it will help you.

What is realizability?

:: research, notes, academia

I recently decided to confront the fact that I didn’t know what “realizability” meant. I see it in programming languages papers from time to time, and could see little rhyme or reason to how it was used. Any time I tried to look it up, I got some nonsense about constructive mathematics and Heyting arithmetic, which I also knew nothing about, and gave up.

This blog post is basically a copy of my personal notebook on the subject, which is NOT AUTHORITATIVE, but maybe it will help you.

The A Means A

:: research, academia

I have argued about the definition of “ANF” many times. I have looked at the history and origins, and studied the translation, and spoken to the authors. And yet people insist I’m “quacking” because I insist that “ANF” means “A-normal form”, where the “A” only means “A”.

Here, I write down the best version of my perspective so far, so I can just point people to it.

How I Redex—Experimenting with Languages in Redex

:: research, tutorial

Recently, I asked my research assistant, Paulette, to create a Redex model. She had never used Redex, so I pointed her to the usual tutorials:

While she was able to create the model from the tutorials, she was left the question “what next?”. I realized that the existing tutorials and documentation for Redex do a good job of explaining how to implement a Redex model, but fail to communicate why and what one does with a Redex model.

I decided to write a tutorial that introduces Redex from the perspective I approach Redex while doing work on language models—a tool to experiment with language models. The tutorial was originally going to be a blog post, but it ended up quite a bit longer that is reasonable to see in a single page, so I’ve published it as a document here:

Experimenting with Languages in Redex

Untyped Programs Don’t Exist

:: research

Lately, I’ve been thinking about various (false) dichotomies, such as typed vs untyped programming and type systems vs program logics. In this blog post, I will argue that untyped programs don’t exist (although the statement will turn out to be trivial).

TLDR

All languages are typed, but may use different enforcement mechanisms (static checking, dynamic checking, no checking, or some combination). We should talk about how to use types in programming—e.g. tools for writing and enforcing invariants about programs—instead of talking about types and type checking as properties of languages.