Reversing Conways Game of Life using a Visual Transformer

DRAFT for now

TL;DR

Conway game of life is a determinsitic 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 posible answers to a deterministic checker (like LEAN). Its fine if the LLM halucinates somehting unhelpful because the checker will discard it. This is a really cool system and the main reasion I first wanted to work with Conway’s Game of Life was to play arround and implement somehting 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) byut I chose to do this with GoL becauyse it looked nicer.

In my mind I see axioms and proofs as somehitng 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 manipluate them into something else, like √2∉Q. Because all these theorems and proofs rest apon 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 apon 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 distribitions that represent how the board couldve looked at the previous time step. After outputing the distribitions (which don’t change; the model will always output the same distrubitons given the same input), the program picks many random configuations from the disribitions of posible 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 iriversible, most boards have multiple reversals. In other words, there often exist multiple boards that when played will result the same. 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 apon 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 deterministicly relate to it, ‘theorems’, until it reaches the depth I want it to.

my approach takes i