Telegram Group & Telegram Channel
AlphaProof - нейросеть Google решает задачи с IMO (международной олимпиады по математике) на уровне серебряного медалиста

Модель идеально решила 4 проблемы из 6, набрав 28 баллов из 42. Для золотой медали нужно 29 баллов. Единственная проблема - на некоторые задачи уходило больше 60 часов, тогда как у человека на все задачи в сумме 9 часов.

Подход концептуально относительно простой - зафайнтюненная Gemini переводит условие задачи в формат Lean (инструмент доказательства теорем такой). Дальше в дело вступает знакомый алгоритм AlphaZero, который научили решать формальные проблемы.

Если вы не знакомы с Lean и интересно что это такое - попробуйте natural numbers game, это прекрасное введение в Lean, которое прошёл даже Терри Тао.

Блогпост

@ai_newz



group-telegram.com/ai_newz/3056
Create:
Last Update:

AlphaProof - нейросеть Google решает задачи с IMO (международной олимпиады по математике) на уровне серебряного медалиста

Модель идеально решила 4 проблемы из 6, набрав 28 баллов из 42. Для золотой медали нужно 29 баллов. Единственная проблема - на некоторые задачи уходило больше 60 часов, тогда как у человека на все задачи в сумме 9 часов.

Подход концептуально относительно простой - зафайнтюненная Gemini переводит условие задачи в формат Lean (инструмент доказательства теорем такой). Дальше в дело вступает знакомый алгоритм AlphaZero, который научили решать формальные проблемы.

Если вы не знакомы с Lean и интересно что это такое - попробуйте natural numbers game, это прекрасное введение в Lean, которое прошёл даже Терри Тао.

Блогпост

@ai_newz

BY эйай ньюз




Share with your friend now:
group-telegram.com/ai_newz/3056

View MORE
Open in Telegram


Telegram | DID YOU KNOW?

Date: |

Telegram was founded in 2013 by two Russian brothers, Nikolai and Pavel Durov. "This time we received the coordinates of enemy vehicles marked 'V' in Kyiv region," it added. Russian President Vladimir Putin launched Russia's invasion of Ukraine in the early-morning hours of February 24, targeting several key cities with military strikes. "Russians are really disconnected from the reality of what happening to their country," Andrey said. "So Telegram has become essential for understanding what's going on to the Russian-speaking world." During the operations, Sebi officials seized various records and documents, including 34 mobile phones, six laptops, four desktops, four tablets, two hard drive disks and one pen drive from the custody of these persons.
from br


Telegram эйай ньюз
FROM American