Import AI ৪৭৮: সামঞ্জস্যের জন্য গণিত; ProgramBench; এবং Mirendil দেখায় RSI কী অর্থ বহন করে

এটি ফিডে পাওয়া অংশবিশেষ। এটি সংক্ষিপ্ত বা প্রকাশকের মূল ভাষায় হতে পারে।

Welcome to Import AI, a newsletter about AI research. Import AI runs on arXiv, cappuccinos, and feedback from readers. If you’d like to support this, please subscribe.Subscribe nowHow math could help alignment:…What the “industrialization of mathematics” means for safety…AI safety startup Resolution (formerly known as Sequent, Import AI 461) has published work on how it has automatically formalized some mathematical statements related to statistical learning theory. Specifically, the team has autoformalized the resolution of singularities, which they believe “lays the groundwork for further automated research into the relationship between loss landscape geometry and generalization.”How they did it: I’ll skip over the math and concentrate on how they did it, which gives us some broader lessons for how people are using AI systems to push on the frontier of knowledge. A Resolution researcher “started by working with agents to develop two plans: a high-level, human-interpretable version and a detailed (112-page) plan divided into atomic steps that closely followed the existing literature,” they write. The researcher “then deputized an orchestrator agent to carry out the plan, spinning up agents to do pen-and-paper math, write Lean, and handle support functions like checking that things were staying on track… the execution phase required little scaffolding beyond the initial plan and some agent skills distilled from earlier internal autoformalization efforts.”$135k for math formalization: The work took about a week, taking “on the order of 100B input tokens (90% cache reads) and about 300 million output tokens (totaling an estimated $135,000 in token spend), and produced about 600k lines of Lean.” Now that they’ve done this, they’ve been able to accelerate some other aspects of their research: “We have already seen both benefits from autoformalization in using this library to extend parts of singular learning theory. Formalizing resolution of singularities lets us aut