Reversing Conway’s Game of Life using a Visual Transformer

TL;DR

Conway game of life is a deterministic cellular automata. I trained a system that produced possible candidate boards for what the previous time step looked like and checked them for correctness. With this I found some pretty cool patterns in the game.

Why I did this

I was interested in LLM-powered automatic proof machines and the ones I looked at have a statistical machine (the LLM) give possible answers to a deterministic checker (like LEAN). Its fine if the LLM hallucinates something unhelpful because the checker will discard it. This is a really cool system and the main reason I first wanted to work with Conway’s Game of Life was to play around and implement something like this.

Initially, I wanted to apply similar methods on a nondeterministic version of something like this(but with more options than one for what path it could take from the seed) but I chose to do this with GoL because it looked nicer.

In my mind I see axioms and proofs as something like this, that there exists some set of unprovable statements and definitions like x=x, []=0, and [0]=1, and we have some tools at our disposal to manipulate them into something else, like √2∉Q. Because all these theorems and proofs rest upon the same set axioms, and branch out from there, I imagine this as a tree.

(I got this image from here

(of course, because theorems will often build upon the work of more than one previous theorem, this doesn’t follow a tree in reality, but the analogy holds in this case)

The automatic theorem provers try to append a node to the right of this metaphorical tree, and check if the rest of the tree agrees with it. Within this analogy, I do something similar with my program for Conway’s Game of Life.

How it works

I have a vision transformer that takes in the board as a grayscale image, and outputs a series of distributions that represent how the board could’ve looked at the previous time step. After outputting the distributions (which don’t change; the model will always output the same distributions given the same input), the program picks many random configurations from the distributions of possible previous boards. It then check each of them through the Game of Life algorithm to see if they will result in the current board.

I originally considered reversing the board in patches, because the Game of Life rules only make local changes, but I figured the

Conways game of life is deterministic and while some boards are irreversible, most boards have multiple reversals. In other words, there often exist multiple boards that when played will lead to the same dynamics. Given a board, only one thing can happen forwards in time, and (often) many things can happen backwards in time.

If we reverse this we can get another tree - similar to the one of math theorems

<image of sideways tree with a blinker as a seed, and branching off it several patterns that result in blinkers, so forth>

My goal with this was to find a board that when the GoL function is iterated upon it a few times it results in something specific. I give my program a seed board, an ‘axiom’ if you will, and it correctly guesses what boards exist that deterministically relate to it, ‘theorems’, until it reaches the depth I want it to.