cdetrio
Joined 11 years ago
Joined 11 years ago
The idea behind the challenge to provide a few lines of human-written/checked scaffolding that defines an "API surface". The API surface is resistant to junk/slop filling out the sorry's. This is supposed to reduce the number of lines that humans have to read to only a handful, while the full valid AI-generated proof is tens of thousands of lines. The challenge was just solved a couple weeks, here's the discussion about it: https://leanprover.zulipchat.com/#narrow/channel/583336-Auto...
My reading of that part in the technical report (models "could be using their own tools behind the model’s API, which is a blackbox"), is that there's no way to prevent it.
But from fchollet's comment here, using tools and harnesses is encouraged, as long as they are generic and not arc-agi specific. In that case, the models should be benchmarked by prompting through claude code and codex, rather than the through API (as from the api we only expect raw LLM output, and no tool use).
It's curious how different people come to very different conclusions about the usefulness of LLMs.
I haven't thoroughly read all of Levin's papers, so I'm not sure to what extent they specifically address the issue of whether textbook models of morphogen gradients can or cannot account for these experiments. I'd guess that it is difficult to say conclusively. You might have to use one of the software packages for simulating multi-cellular development, regulatory logic, and morphogen gradients/diffusion, if you wanted to argue either "the textbook model can generate this behavior" or that the textbook model cannot.
The simulations/models that I'm familiar with are quite basic, relative to actual biology, e.g. models of drosophila eve stripes are based on a few dozen genes or less. But iiuc, our understanding of larval development and patterning of C Elegans is far behind that of drosophila (the fly embryo starts as a syncytium, unlike worms and vertebrates, which makes fly segmentation easier to follow). I haven't read about Xenopus (the frogs that Levin studies), but I'd guess that we are very far from being able to simulate all the way from embryo to facial development in the normal case, let alone the abnormal picasso and "eye on tail" tadpoles.
"Here, we propose a new analogy, inspired by recent work in machine learning and neuroscience: that the genome encodes a generative model of the organism. In this scheme, by analogy with variational autoencoders, the genome does not encode either organismal form or developmental processes directly, but comprises a compressed space of latent variables."
1. https://arxiv.org/abs/2407.15908 2. discussion with the authors https://www.youtube.com/watch?v=6QaMnUBkmz4
1. https://www.leaprate.com/news/oanda-suspends-weekend-trading...