cdetrio
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...
There's an interesting wrinkle though. The formal definitions and statements need to be correct, i.e. need to faithfully translate the human-readable (informal) definitions and statements. A few months ago, Kevin Buzzard created an auto-formalization challenge: https://gist.github.com/kbuzzard/778bc714030b3e974ab5f403878...
It's a handful of human-written lines, a skeleton that defines an "API surface". If you use AI to generate the rest of the code, the API surface (along with the Lean compiler) acts to guarantee that the whole generated solution (tens of thousands of lines) will be correct.
The discussion thread about the challenge, which was solved a couple weeks ago, is here: https://leanprover.zulipchat.com/#narrow/channel/583336-Auto...
Without the human-written or human-audited skeleton, you might get AI-generated slop Lean code that compiles, but contains nonsensical definitions/statements and thus vacuous proofs. Though from what I gather, recent models are much improved in their capability to generate correct statements and definitions and proofs, for both formal math and informal math.
A discussion thread about a different auto-formalization effort without human-written API surface, with some correct output and some slop: 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...
I gave a talk about it back in June. Slides: https://docs.google.com/presentation/d/1n75Mo09HmyruV5S7q0cH... video: https://youtu.be/2eISBAbT3GM?t=1h22m3s
1. https://news.ycombinator.com/item?id=15308771 Super-Accurate GPS Chips Coming to Smartphones in 2018 (ieee.org)
> We vary N from 1 to 24 hours and examine the p-values. [.....] there are a number of periods where the p-values are significantly below 0.05 and we reject the null hypothesis for those periods.
Is it p-hacking to vary N and find low p-values? If its not p-hacking, but a valid analysis with predictive power, then wouldn't it make a good trading strategy to watch the tether wallet and buy btc whenever new issuance happens?
Skidmore got involved last spring when he heard Catherine Austin Fitts, former assistant secretary of Housing and Urban Development, refer to a report which indicated the Army had $6.5 trillion in unsupported adjustments, or spending, in fiscal 2015. Given the Army’s $122 billion budget, that meant unsupported adjustments were 54 times spending authorized by Congress.
> As I think about acts of integrity and grace, I realise that there is nothing in my knowledge to compare with Frege’s dedication to truth. His entire life’s work was on the verge of completion, much of his work had been ignored to the benefit of men infinitely less capable, his second volume was about to be published, and upon finding that his fundamental assumption was in error, he responded with intellectual pleasure clearly submerging any feelings of personal disappointment. It was almost superhuman and a telling indication of that of which men are capable if their dedication is to creative work and knowledge instead of cruder efforts to dominate and be known. [2]
And how rare it is to see such "exceptionally honest" academic dialogue as Frege's:
> Frege starts his analysis by this exceptionally honest comment : "Hardly anything more unfortunate can befall a scientific writer than to have one of the foundations of his edifice shaken after the work is finished. This was the position I was placed in by a letter of Mr Bertrand Russell, just when the printing of this volume was nearing its completion" [3]
Voevodsky too, upon finding himself in the same position as Frege, reacted with a super-human level of integrity and intellectual honesty:
> In 1998, the American mathematician Carlos Simpson published a paper indicating there might be a mistake in Voevodsky and Kapranov’s 1990 result. For years Voevodsky sifted through the details without making much progress. He remained convinced the result was right. Then, in the autumn of 2013, as the leaves changed color and summer gave way to autumn, he made a breakthrough. Of sorts. He confirmed the error. The important result was no longer quite so important.
> “It is plainly wrong. The main theorem is incorrect,” he says. “It’s not that there is some gap in the proof. It’s that the main theorem is plainly wrong.” The mistake, he explains, was in failing to question the obvious. “We had proved that an assertion was indeed true in all of the difficult cases, but it turned out to be false in the simple case. We never bothered to check.” In confirming the error, he added an addendum to the original citation in his official publications list—“Warning: The main theorem of this paper was shown by Carlos Simpson to be false.” [1]
It is all the more remarkable that he spent years of working through painstaking details to prove to himself that he was wrong. And rather than quietly issuing a retraction, he shouted it from the rooftops, leading a heroic charge to get mathematicians to stop hand-waving with English-language proofs, and start writing code. [4]
> And I now do my mathematics with a proof assistant. I have a lot of wishes in terms of getting this proof assistant to work better, but at least I don’t have to go home and worry about having made a mistake in my work. I know that if I did something, I did it, and I don’t have to come back to it nor do I have to worry about my arguments being too complicated or about how to convince others that my arguments are correct. I can just trust the computer. There are many people in computer science who are contributing to our program, but most mathematicians still don’t believe that it is a good idea. And I think that is very wrong.[5]
1. https://nautil.us/issue/24/error/in-mathematics-mistakes-are...
2. https://plato.stanford.edu/entries/russell-paradox/
3. https://en.wikipedia.org/wiki/Russell%27s_paradox#cite_note-...
4. https://www.quantamagazine.org/univalent-foundations-redefin...
5. https://www.ias.edu/sites/default/files/pdfs/publications/le...