Links for 2023-04-17
Formal Mathematics Statement Curriculum Learning
We show that at same compute budget, expert iteration, by which we mean proof search interleaved with learning, dramatically outperforms proof search only. We also observe that when applied to a collection of formal statements of sufficiently varied difficulty, expert iteration is capable of finding and solving a curriculum of increasingly difficult problems, without the need for associated ground-truth proofs.
...we confirm here that our models acquire advanced capabilities to leverage these high-level tactics by providing exogenous arguments which are not present in the current tactic state. The generation of these exogenous arguments through language modeling seems to require a non-trivial amount of mathematical intuition...We have also observed a number of proofs that require multiple non-trivial reasoning steps through the use of lower-level tactics...
...we also observe that proofs generated by our models have a distinctive style compared to proofs formalized by humans. This stems in part from the model’s capability to leverage high-level tactics in a way that is challenging for humans...
Paper [Feb 2022]: https://arxiv.org/abs/2202.01344
Here is a reminder that it is now possible to take a bunch of static 2D photos of a place and have a neural network turn them into a high-resolution 3D environment. This means that any place (and object) that has been photographed from a few directions can now be turned into a virtual 3D environment. Want to design a photorealistic video game environment? Just take a bunch of photos and have the neural network do the rest. https://jonbarron.info/zipnerf/
4 Autonomous AI Agents you need to know https://towardsdatascience.com/4-autonomous-ai-agents-you-need-to-know-d612a643fa92
Combining Data and Theory for Derivable Scientific Discovery with AI-Descartes: “We develop a method to enable principled derivations of models of natural phenomena from axiomatic knowledge and experimental data by combining logical reasoning with symbolic regression.” https://www.nature.com/articles/s41467-023-37236-y
“New paper comparing GPT-3.5 & GPT-4 performance on college physics problems. It shows that in just a few months, AI has made a leap from the 39th to the 96th percentile of human level performance. Now imagine where it will be in 10 years.” — @carlbfrey https://arxiv.org/abs/2303.1701
How A.I. and DNA Are Unlocking the Mysteries of Global Supply Chains [The New York Times] https://archive.is/jZMRe
This AI Clock Uses ChatGPT to Generate Tiny Poems That Tell the Time https://www.theverge.com/23669343/ai-clock-chatgpt-poems-rhymes-diy-project
The latest Y Combinator class is full of AI startups. [Business Insider] https://archive.is/rX6Sp
Scientists at Stanford University have developed a retinal prosthesis with five times the resolution of the most advanced prosthetics currently used in clinical studies. https://scopeblog.stanford.edu/2022/12/02/a-big-jump-in-prosthetic-vision/
A New History of Greek Mathematics: “I have read only about 30 pp. so far, but this is clearly one of the best science books I have read, ever. It is clear, always to the point, conceptual, connects advances in math to the broader history, explains the math, and full of interesting detail.” https://marginalrevolution.com/marginalrevolution/2023/04/a-new-history-of-greek-mathematics.html
Probabilistic Numerics: Computation as Machine Learning — “This book aims to give an overview of the emerging new area of Probabilistic Numerics, particularly influenced by contemporary machine learning...Our principal goals will be to study uses and roles for uncertainty in numerical computation, and to employ such uncertainty in making optimal decisions about computation.” https://www.probabilistic-numerics.org/assets/ProbabilisticNumerics.pdf#page=3
Polio Lab Leak Caught with Wastewater Sampling https://www.lesswrong.com/posts/nhb3CpnnpnLxWBn5x/polio-lab-leak-caught-with-wastewater-samplin
10 reasons why lists of 10 reasons might be a winning strategy https://www.lesswrong.com/posts/8gbfvGhSnEJ9hHGew/10-reasons-why-lists-of-10-reasons-might-be-a-winning
Development of a novel epigenetic clock resistant to changes in immune cell composition: “…we investigate how cell composition impacts existing epigenetic clocks, we build a * new clock * that predicts age evenly across cell types, and we show this new clock has interesting properties.” https://www.biorxiv.org/content/10.1101/2023.03.01.530561v1
GPT-4 » Open-Source when it comes to bugfinding: https://twitter.com/ID_AA_Carmack/status/1647286964696276992