ИИ OpenAI набрал 12/12 на Олимпиаде по программированию. Официальные чемпионы — команда СПбГУ

[M_AJ]

Получается теперь придется как в шахматах, следит за тем, чтобы не проносили телефоны с доступом к ChatGPT

[411]

del

[ValeriyPus]

(del)

[JediPhilosopher]

Ну что, все, ICPC можно закрывать?

Жалко родной ИТМО чет уже который год ничего не занимает высокого (сейчас глянул - аж с 17 года не выигрывали). Ведь в свое время именно эта олимпиада ему помогла сильно распиариться и раскрутиться.

[funca]

Ну хоть в традиционных олимпийских дисциплинах, в роде метания копья или там прыжков с трамплина, у компьютеров не видно даже близко ни каких успехов. У человечества ещё не все потеряно.

[jamiederinzi]

В метании копья машины превзошли людей уже примерно так в древнем Риме. В прыжках в воду... Ну, дайте роботам ещё пару лет.

[ssj100]

была бы задача и это сделали бы? помните в 2014 году что говорили про компьютер и Го? и через 4 года полный разгром

[Dmitry_Dor]

Ну хоть в традиционных олимпийских дисциплинах,... У человечества ещё не все потеряно.

¯\_(ツ)_/¯

[Wesha]

Марафон не пробежит.

[ogogoggogog]

Какое убожество (если не рендер), ну пенсионеров уже обогнали. И то не любых, некоторые даже в 60 колесо крутят и на руках ходят. Вы посмотрите что кожмешки атлеты умеют хотябы уровня КМС

[Robastik]

В большинстве регионов среднестатистические мужчины не доживают до пенсии.

[ogogoggogog]

кармасери и тут нагадили. а робот среднестатистический через 5 лет ломается, и чо? Чем тут восхищаться-то в видосике?

[axion-1]

Скорее в гимнастике или в марафоне. Там где требуется либо идеальная координация движений, либо большой запас хода.

[Wesha]

И водонепроницаемость.

[pulsatrix]

И плавучесть.

[axion-1]

Всё-таки это на олимпиадных задачах, они не самые сложные. В задачах где нужен долгий ресёрч, множество экспериментов и подбор параметров (типа тех что на Kaggle, например), люди пока что лидируют. Но боюсь такими темпами "угадыватель следующего слова" и там скоро сможет побеждать.

[ihost]

Отделы маркетинга и пиара у компаний-разработчиков нейрогенераторов работают действительно сильно, в отличие от самих галлюцинирующих нейрогенераторов - надо же отбивать тонны вложенных инвестиций

Недавно хайповали на IMO, теперь пытаются рекламироваться на ICPC - в случае с IMO даже поленились забить готовые ответы в свои нейромодельки https://www.reddit.com/r/LocalLLaMA/comments/1m1dzqj/imo_2025_llm_mathematical_reasoning_evaluation/ , интересно как здесь будет

А по существу уже давно понятно, что llm это симулятор светской беседы, а путь к настоящему AI/AGI лежит в области автоматизированных формальных доказательств, с постепенным увеличением слоя абстракции, и выполнения доказательств во все более сложных вселенных формальных моделей

Недавно как раз попадалась научная статейка авторов из Китая, где IMO 2025 решали как раз через автоматизированные формальные доказательства на Lean, и плюсом еще сделали библиотечку для геометрических доказательств

[Wesha]

автоматизированные формальные доказательства

— А чем докажешь?
— Мамай клянус!

[jamayka]

Ну как раз в той статейке ведь и говорится о том, что llm использовалась как минимум для порождения идей для новых построений, а уже дальше из этих построений выводились все возможные факты и с помощью формальных доказательств выбирались нужные. Подозреваю, что перевод естественного языка в постановке задачи в формальный тоже делался с помощью llm. Короче я клоню к тому, что llm - это не просто "симулятор светской беседы", это симулятор всякого. Нужно просто научиться его эффективно использовать в комплексе с другими инструментами и методиками, а не ждать от него чуда.

[ihost]

Вы же об этой статье говорите https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver/SeedProver_0801_2.pdf ?

IMO 2025 During the IMO 2025 contest, all problems were translated into formal statements by human experts

Также pdf-ки с итоговыми красивыми человеко-читаемыми доказательствами (из папки SeedProver/IMO2025) были сделаны экспертами по мотивам Lean-доказательства (о чем сказано в readme)

Да, как Вы верно заметили, llm использовался для генерации идей новых лемм, но скорее всего обычный random сработал бы не хуже для случайного блуждания в пространстве формальных лемм

[jamayka]

Есть ощущение, что рандом сработал бы много хуже. llm хорошо умеет генерить правдоподобный контент (далеко не обязательно правдивый), что очень неплохо сужает пространство для блуждания. Поправьте, если это не так.

[411]

А где сами задачи глянуть?

[ihost]

https://worldfinals.icpc.global/problems/2025/finals/problems/problemset.pdf

[d_ilyich]

Прошу прощения, что не совсем в тему. Вопрос к тем, у кого оформлена подписка на чей-нибудь ИИ: платная версия действительно более "умная"? На каком-то сервисе я видел заявление, что, мол, в бесплатном режиме бот не очень, а вот за деньги -- прям гений будет.

Спрашиваю потому, что ни один из опробованных мной бесплатных AI-ботов не смог эффективно решить задачку с leetcode 3552. Grid Teleportation Traversal. Под эффективным решением в данном случае я понимаю любое, которое было бы принято литкодом. Лучше всех проявил себя QWEN-Coder.

[newalex123]

Не знаю насчет гениальности, но конкретно эту задачу GPT-5 Thinking в режиме Heavy thinking решил с первой попытки(Accepted 608 / 608 testcases passed) за 5 минут 18 секунд

[d_ilyich]

Это в платной версии такой режим?

[newalex123]

Да. Вообще я не в курсе, доступен ли GPT-5 Thinking для бесплатных пользователей, но если и да - скорее всего ресурсы, выделяемые ему, сильно ограничены. Долгодумающие режимы только в платной версии.