3 ms·
This just means that it operates on the (debug text form of the) intermediate representation of a compiler.
by j2kun 1y ago
This just means that it operates on the (debug text form of the) intermediate representation of a compiler.
- proof_by_vibes 1y agoNot necessarily. Theorem provers provide goals that can serve the same function as "debug text." Instead of interpreting the natural language chosen by the dev who wrote the compiler, these goals provide concrete, type-accurate statements that indicate the progress of an ongoing proof.
- j2kun 1y agoI'm referring to what the authors actually claim they did in the paper. They operated on XLA-generated textual IR. Cf. the second paragraph of 3.3.4 of https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms/AlphaEvolve.pdf https://storage.googleapis.com/deepmind-media/DeepMind.com/B...