Joseph Gardi

let's focus in one component. suppose you want to write the 3D renderer: i.e., the part of the game engine that draws the scene to the screen. if you ask gpt-4 to write such a thing in one go... it will fail hard. that's some big piece of software, involving lots of functions and data structures. vectors, matrices, rotations, line rastering, depth buffers. there's no AI model in the world that can write the whole thing without getting stuck in some bug in the way. (to be fair, perhaps soon, but not today!) now, assume we have an optimal prover as a tool. that is, a magic oracle that, given a proposition, outputs a correct proof. how could we exploit that to make gpt-4 or sonnet of today write a whole game engine autonomously? simple: rather than asking it to write the code, we ask it to write specs as types. for example, it could fully specify what it means to "render a scene" by using a dumb "ray intersection" approach. in plain english, that spec would be like: > given set of triangles, a cam, a screen, return, for each screen pos, the color of the first triangle that intersects the cam->pos ray the AI would then send that spec to the theorem prover, and the theorem prover would return a correct rasterization algorithm! the key insight is that writing a correct spec is *much* simpler and smaller than writing the full algorithm that satisfies it. the spec above, for example, can be written in a single line of code, while the correct implementation is thousands of lines of code. so, in short, to write a game engine, all that gpt-4 or sonnet would need to do is write a series of "specs as types". and yes, all the specs of a complete game engine certainly fit the context of gpt-4. but again, that's not the *only* way. that's just an example. if we actually had an "optimal theorem prover" at hands, we could literally just ask it to build a better gpt. as in, specify what a language model is as a type (i.e., define the concept of characters, next-token, loss, etc.) - that's reasonably easy to do. then, given that type to the hypothetical optimal theorem prover, and watch it invent a super smart language model architecture that has infinite effective context size. then, ask *that* thing to write the game engine for you (: similarly, things like ARC-AGI can be directly solved by such oracle, by just writing a type that says "give me a program f of size < X such that, for each ARC-AGI input x, produce its output y" of course, that's all assuming an optimal theorem prover (big assumption). but hopefully this helps you visualize how such a thing would imply all the things that people expect from an "AGI". so, by focusing on the problem of proof synthesis, we're indirectly working on the problem of superintelligence