нейроинтерфейс
Jul. 26th, 2024 04:26 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
sab123Из зивана приехало:
ИИ научили решать задачки международной математической олимпиады, и он их нарешал на уровне серебряного медалиста.
<<
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
AlphaProof is a system that trains itself to prove mathematical statements in the formal language Lean. It couples a pre-trained language model with the AlphaZero reinforcement learning algorithm, which previously taught itself how to master the games of chess, shogi and Go.
Formal languages offer the critical advantage that proofs involving mathematical reasoning can be formally verified for correctness. Their use in machine learning has, however, previously been constrained by the very limited amount of human-written data available.
In contrast, natural language based approaches can hallucinate plausible but incorrect intermediate reasoning steps and solutions, despite having access to orders of magnitudes more data. We established a bridge between these two complementary spheres by fine-tuning a Gemini model to automatically translate natural language problem statements into formal statements, creating a large library of formal problems of varying difficulty.
When presented with a problem, AlphaProof generates solution candidates and then proves or disproves them by searching over possible proof steps in Lean. Each proof that was found and verified is used to reinforce AlphaProof’s language model, enhancing its ability to solve subsequent, more challenging problems.
...
I tried this year’s problems while I was at the International #Math Olympiad myself. It took me hours. I imagine that when people saw Sputnik overhead in 1957, they might have had the same feeling that I do now.
I have been anticipating this level of #AI coming, but thought it was still years away. My interest is not in making AI better, but in what we need to do to help all the people. That’s below.
But first, context: IMO problems are specifically selected to be non-standard. For the previous 10 years, I served as the national coach of the USA International Math Olympiad team (https://www.quantamagazine.org/po-shen-loh-led-the-u-s...). During the IMO itself, the national coaches meet to select the problems that will appear on the exam paper.
One of the most important tasks of that group is to avoid problems that have similarity to problems that have appeared anywhere before. During those meetings, national coaches would often dig up an old obscure math competition, on which a similar problem had appeared, and show it to the group, after which the proposed problem would be struck down.
So, this AI breakthrough is totally different from #GPT being able to do standardized tests through pattern-matching. It strikes at the heart of discovery. It's very common for students to hit a wall the first time they try IMO-style problems, because they are accustomed to learning from example, remembering, and executing similar steps.
Take a look at the 6 problems for yourself, and you’ll see that they are way beyond any curricular standards: https://www.imo-official.org/year_info.aspx?year=2024. And even though the AI took more than the normal time limit, it’s only a matter of time before the software and hardware speed up, so the sheer fact that it was able to solve the problems at all is a major advance. The hard part of solving these problems isn’t calculation. It’s inventing a solution pathway. Most people would get 0 points even if they had a year to think.
>>
Это наконец-то реализация комбинированного интеллекта. Идея по сути довольно простая: вот, скажем, считать до 100 - для человека довольно сложная задача, дети ей учатся годами. А компьютер может это делать очень легко и эффективно. Поэтому пытаться научить компьютерный ИИ арифметике - глупо и неэффективно. От этого происходят не только тормоза, но и косяки в арифметике ("галлюцинации"). Вместо того надо сращивать ИИ и родную реализацию арифметики в компьютере, по сути мозг со встроенным нейроинтерфейсом к калькулятору. То же самое относится к многим другим областям - грамматики, логические доказательства, и прочее.
Мне уже лет 10 как непонятно, почему так не сращивают. Я тогда увидел пример, который пытается научить ИИ находить соответствие количества открывающих и закрывающих скобок, с попыткой разобрать, что там получилось в индивидуальных нейронах - типа, этот реагирует на открывание, этот на открывание, а тут считается баланс, но кривовато. И подумал, что было бы очень логично отдать подсчет в отдельную арифметическую логику, к которой обращаться из нейронной сети.
И вот наконец-то на практике сростили.
ИИ научили решать задачки международной математической олимпиады, и он их нарешал на уровне серебряного медалиста.
<<
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
AlphaProof is a system that trains itself to prove mathematical statements in the formal language Lean. It couples a pre-trained language model with the AlphaZero reinforcement learning algorithm, which previously taught itself how to master the games of chess, shogi and Go.
Formal languages offer the critical advantage that proofs involving mathematical reasoning can be formally verified for correctness. Their use in machine learning has, however, previously been constrained by the very limited amount of human-written data available.
In contrast, natural language based approaches can hallucinate plausible but incorrect intermediate reasoning steps and solutions, despite having access to orders of magnitudes more data. We established a bridge between these two complementary spheres by fine-tuning a Gemini model to automatically translate natural language problem statements into formal statements, creating a large library of formal problems of varying difficulty.
When presented with a problem, AlphaProof generates solution candidates and then proves or disproves them by searching over possible proof steps in Lean. Each proof that was found and verified is used to reinforce AlphaProof’s language model, enhancing its ability to solve subsequent, more challenging problems.
...
I tried this year’s problems while I was at the International #Math Olympiad myself. It took me hours. I imagine that when people saw Sputnik overhead in 1957, they might have had the same feeling that I do now.
I have been anticipating this level of #AI coming, but thought it was still years away. My interest is not in making AI better, but in what we need to do to help all the people. That’s below.
But first, context: IMO problems are specifically selected to be non-standard. For the previous 10 years, I served as the national coach of the USA International Math Olympiad team (https://www.quantamagazine.org/po-shen-loh-led-the-u-s...). During the IMO itself, the national coaches meet to select the problems that will appear on the exam paper.
One of the most important tasks of that group is to avoid problems that have similarity to problems that have appeared anywhere before. During those meetings, national coaches would often dig up an old obscure math competition, on which a similar problem had appeared, and show it to the group, after which the proposed problem would be struck down.
So, this AI breakthrough is totally different from #GPT being able to do standardized tests through pattern-matching. It strikes at the heart of discovery. It's very common for students to hit a wall the first time they try IMO-style problems, because they are accustomed to learning from example, remembering, and executing similar steps.
Take a look at the 6 problems for yourself, and you’ll see that they are way beyond any curricular standards: https://www.imo-official.org/year_info.aspx?year=2024. And even though the AI took more than the normal time limit, it’s only a matter of time before the software and hardware speed up, so the sheer fact that it was able to solve the problems at all is a major advance. The hard part of solving these problems isn’t calculation. It’s inventing a solution pathway. Most people would get 0 points even if they had a year to think.
>>
Это наконец-то реализация комбинированного интеллекта. Идея по сути довольно простая: вот, скажем, считать до 100 - для человека довольно сложная задача, дети ей учатся годами. А компьютер может это делать очень легко и эффективно. Поэтому пытаться научить компьютерный ИИ арифметике - глупо и неэффективно. От этого происходят не только тормоза, но и косяки в арифметике ("галлюцинации"). Вместо того надо сращивать ИИ и родную реализацию арифметики в компьютере, по сути мозг со встроенным нейроинтерфейсом к калькулятору. То же самое относится к многим другим областям - грамматики, логические доказательства, и прочее.
Мне уже лет 10 как непонятно, почему так не сращивают. Я тогда увидел пример, который пытается научить ИИ находить соответствие количества открывающих и закрывающих скобок, с попыткой разобрать, что там получилось в индивидуальных нейронах - типа, этот реагирует на открывание, этот на открывание, а тут считается баланс, но кривовато. И подумал, что было бы очень логично отдать подсчет в отдельную арифметическую логику, к которой обращаться из нейронной сети.
И вот наконец-то на практике сростили.
no subject
Date: 2024-07-27 11:29 am (UTC)И что полезного теперь эта срощенная ИИ-система может делать?
В товары/деньги это как-то конвертируется?
no subject
Date: 2024-07-28 08:49 pm (UTC)no subject
Date: 2024-07-28 11:13 pm (UTC)Обычно, математические теоремы плохо конвертируются в продающиеся товары.
no subject
Date: 2024-07-29 01:37 am (UTC)Другой жизненный пример - юридические аргументы. Проверка цитат и логических выводов на правильность позволит автоматически писать толковые юридические аргументы. То есть получатся автоматические юристы.
no subject
Date: 2024-07-29 02:28 am (UTC)Когда, по-твоему, AI сумеет писать правильные программы?
> Другой жизненный пример - юридические аргументы. Проверка цитат и логических выводов на правильность позволит автоматически писать толковые юридические аргументы. То есть получатся автоматические юристы.
Когда, по-твоему, появятся автоматические юристы?
Для полноценных программистов и юристов - нужна способность проверять на ошибки и на достижение результата.
Математические доказательства правильности - проверкой на ошибки не являются.
no subject
Date: 2024-07-29 09:45 pm (UTC)no subject
Date: 2024-07-30 02:11 am (UTC)Каким образом "доказательства правильности являются проверкой на ошибки"?
Разве в этих доказательствах правильности происходит проверка на соответствие с реальным миром?
> галлюцинированное уже сейчас юристы копипастят в свои документы.
Так ведь юристы и копипастят. Проверяя на ошибки.
Если бы можно было полагаться на "доказательства правильности" для проверки на ошибки, то юристов бы уже исключили из процесса.
no subject
Date: 2024-07-30 05:01 pm (UTC)По определению.
> Разве в этих доказательствах правильности происходит проверка на соответствие с реальным миром?
И программирование и юриспрудениця происходят в формальной логической среде.
> Так ведь юристы и копипастят. Проверяя на ошибки.
Нет, когда напрямую копипастят, то не проверяя. Оно им потом иногда вылазит.
no subject
Date: 2024-07-30 05:14 pm (UTC)> По определению.
Нет, не являются.
Доказательства проверяют соответствие теоретической модели теоретическим аксиомам.
Тестирование на практике теоретические доказательства не делают.
>> Разве в этих доказательствах правильности происходит проверка на соответствие с реальным миром?
> И программирование и юриспрудениця происходят в формальной логической среде.
Лишь _частично_ в формальной среде.
И программирование и юриспруденция опираются на практические наблюдения за реальным миром.
>> Так ведь юристы и копипастят. Проверяя на ошибки.
> Нет, когда напрямую копипастят, то не проверяя.
Откуда ты взял, что юристы не проверяют то, что они копипастят?
Если бы юристы не проверяли, то ошибки бы шли сплошным потоком.
> Оно им потом иногда вылазит.
Иногда вылазит, потому что юристы не все ошибки находят.