Т.е. я правильно понимаю, что в качестве меры борьбы с вытеснением её профессии AGI она ушла в профессию, которую гипотетический AGI уничтожит ещё раньше? :)))
Я вообще к вам хотел попробоваться, но честно говоря бывшие тренеры по боксу в качестве core инженеров C++ меня очень смущают.
Как это вообще возможно?? Для поддержки ядра текстового редактора надо знать миллион вещей, всякие CRDT/gapbuffers/строковые кэши, обычно многопоточку, теорию по парсерам, C++ собственно на хорошем уровне, ядра пары других текстовых движков шапочно. Мейнтейнеры подобных движков, известные мне, все с бэкграундом в CS и при этом достаточно упоротые чтобы продолжать специализироваться в C++ со временем. А у вас так легко, взял из бокса вкатился, пилит constexpr <auto> template MyLineStorage::fetch в кор команде... Кстати его ответ "Как пришёл в IT" освещает что угодно, но только не как он пришёл в IT.
Это не так. В VST верифицируемая программа пишется на си
Гм, не совсем. Несколькими страницами ниже:
Verifiable C is a program logic (higher-order impredicative concurrent separation logic) for C programs with these restrictions:
• No casting between integers and pointers. • No goto statements. • No bitfields in structs. • No struct-copying assignments, struct parameters, or struct returns. • Only structured switch statements (no Duff’s device). • No varargs functions, except limited undocumented support for calling printf and fprintf.
The Verifiable C program logic operates on the CompCert Clight language. CompCert’s clightgen tool (described in the next chapter) translates C into C light, so that you can use VST to apply the program logic to the program. Clight (and clightgen) does support some of the features listed above (such as goto, bitfields, struct-copying), but programs with those features cannot be proved in Verifiable C.
"Пишется на ограниченном диалекте C" != "пишется на си".
Чем Lean и Coq не подходят?
Про Lean не в курсе, но Coq (закрою глаза на то, что это ЯП, а не система символьного вывода) является реализацией исчисления конструкций и следовательно подвержен всем ограничениям исчисления конструкций, например в Coq является выводимым парадокс Карри:
Parameter Y : Prop.
Axiom curry_axiom : forall P : Prop,
Y <-> (Y -> P).
Theorem curry_paradox : forall P : Prop, P.
Proof.
intros P.
destruct (curry_axiom P) as [H1 H2].
(* H1 : Y -> (Y -> P)
H2 : (Y -> P) -> Y *)
set (f := fun z : Y => H1 z z).
(* f z = H1 z z : P, so f : Y -> P *)
pose (y := H2 f).
(* y : Y *)
exact (H1 y y).
Qed.
Нет таких символьных систем, в которых можно непротиворечиво вывести всю математику. Во-первых никто толком не договорился об аксиоматике (поэтому собственно и возможен мой пример выше), во-вторых есть теоремы Гёделя о неполноте.
И для математики, и для программирования существуют инструменты проверяющие корректность
Для программ и доказательств, записанных на формально верифицируемом языке. Что на сегодняшний день равняется 2.5 академическим ЯП в области программирования и примерно 0 универсальных формальных систем в области чистой математики.
Операционная система, не получив от программы сигнала о завершении через системный вызов exit, принудительно ее уничтожает
Новое слово в системном программировании... FYI если в программе нет вызова exit и т.д., то проц просто продолжает выполнять опкоды, расположенные за программой в памяти. Как правило это заканчивается тем, что он выполняет что-то в non executable области, и как следствие segfault. Но всякое бывает, может случайно и сискол exit выполниться. Никакого "принудительного уничтожения" таких программ в Linux нет, их поведение просто не определено.
В целом как-то многовато пафоса для, видимо, набора типа "высокоуровневых" макросов для опкодов x86-64?
критиковал не столько решения openai, сколько язык записи доказательств у openai =) Само по себе решение #1 от openai, как оказалось, верное - перепроверил после всех разъяснений.
У Google значительно лучше, как минимум понятнее. В решении #1 тоже не нашёл ошибок.
Круто... Теперь хотелось бы увидеть не столько решения, сколько цепочки рассуждений модели. Как она выбирает, на чём основывать доказательство, по каким ложным путям ходит в процессе. И на чём записываются эти цепочки рассуждений, явно же внутри там какой-то аля prolog / rocq.
Моя картина мира пошатнулась если честно :( Я раньше думал, что такие трюки невозможны без AGI (т.е. в данном случае формализованной модели арифметики, наивной теории множеств, планиметрии и т.д. где-то внутри LLM).
Для справки: я phd по математике, занимаюсь (занимался) символьным выводом. Спасибо за "не подкреплено знаниями по теме вопроса".
Язык этот я вижу первый раз, видимо что-то олимпиадное. Профессиональный язык в математике это нечто, пересыпанное кванторами и логическими связками, вот например - символика там мб весьма специфической и непонятной, но как минимум там фразы с логичной структурой, а не обрубки.
Не знаю, что там за общеизвестные обозначения, но Z с двумя индексами может обозначать всё, что угодно. Общеизвестное обозначение для данного множества из задачи это ℕ⊗ℕ или ℕ² или ℤ⁺⊗ℤ⁺ или даже {(x, y) | (x∈ℤ y∈ℤ x>0 y>0}. Не зная что там за объект, я вынужден докапываться даже до самых базовых объектов в условии, например для графов (не для наборов точек) "покрытие" может означать 2 вещи - покрытие рёбер и покрытие вершин. И мне странно, что дано условие задачи, в котором не устранена малейшая двусмысленность, при том что это можно сделать в половину строки хоть на этом псевдоязыке хоть в обычной математической нотации. В этот раз вы вроде интерпретировали верно, в иных условиях может не повезти.
Ссылку на решения что характерно не привели, разумеется ссылка на тг канал важнее. https://github.com/aw31/openai-imo-2025-proofs Посмотрел решение первой задачи, имхо это какой-то бред.
ИИ выдаёт решение на каком-то трудно читаемом языке, похожем на тот, что используется человеком в математических доказательствах, но состоящем из излишне коротких фраз, иногда грамматически некорректных, с сильной нехваткой логических связок между ними. Читать и валидировать это невозможно, например неясно где знак равенства означает "введём определение" (то что в нормальной нотации обозначается := или ≝), а где утверждение равенства. Могли бы помочь текстовые комменты, но ИИ не утруждает себя их написанием, равно как и написанием кванторов в определениях, что делает невозможным понимание определений. Чтобы не быть голословным:
### PROBLEM 1 SUBMISSION ###
\[
P_n:=\{(a,b)\in \mathbf Z_{>0}^2: a+b\le n+1\}, \quad n\ge 3.
\]
Need families of n lines covering P_n. "Sunny": direction not in {horizontal, vertical, slope -1}.
Need possible numbers of sunny lines in an n-line covering.
--------------------------------------------------------------------------
### 1. Basic configs, notation.
For n: triangle in plane: T_n = {x>=1,y>=1,x+y<=n+1}, vertices (1,1),(1,n),(n,1). P_n = integer points in it.
Three sides lines: H_n: y=1 bottom, V_n: x=1 left, D_n: x+y=n+1 hyp. Exactly forbidden directions.
(...)
Что значит "covering"? Что такое slope -1? Что такое Z и что означают индексы в ней? Что такое hyp. - hypotenuse, hypothesis, автор токены экономит???? Что такое "forbidden directions", мы же вроде на формальном языке пытаемся говорить?
Я не понимаю как кто-то реально может заявлять о своей способности провалидировать это решение.
Очень оторванный от реальности подход. Проблем у него миллион, навскидку хотя бы такие:
– Чтобы этот подход работал, нужен coding standard, регламентирующий АБСОЛЮТНО ВСЁ. Межблочные интервалы. Выравнивание знаков равенства в блоке похожих выражений var1 = value1. Шаг в сторону и летит любое кастомное форматирование кода. Вот например несколько способов записать массив чисел, пользуясь одним и тем же кодстайлом:
( 1 2 3
4 5 6 )
( 1 2
3 4
5 6 )
( 1 2 3 4 5 6 )
После roundtrip в AST и обратно будем выводить всё в 1 строку, да? Не всё кастомное форматирование является, как вы выражаетесь, "самовыражением". В некоторых случаях человек записал числа прямоугольником 2x3 потому что это способ наглядно представить данные, например там числа логически идут парами. В другом случае он вылез за разрешённую кодстайлом ширину текста 100 символов потому что иначе не влезает длинное объявление объекта. В третьем случае поставил 3 пустых строки, а не как по стандарту 1, вокруг какого-то блока, потому что там кластеры блоков кода. Исключения, исключения... Никогда и нигде в реальном проекте вы не встретите большого куска кода, способного без изменений пережить десериализацию в AST и сериализацию обратно.
– Чтобы этот подход работал, надо к каждому репозиторию с кодом иметь корректно парсящую его систему, которая может весить в разы больше скромного набора plaintext строк.
– Первый же реальный проект, в который вы притащите ваш редактор, начнётся с того, что там будет сторонний код, использующий собственный кодстайл (или не использующий вовсе), править который под "ваш" кодстайл и подключать ваш парсер никто не будет. Как взаимодействовать с таким кодом?
Так у вас в способе #2 MyHeap каждый раз выделяет блок только с бОльшим адресом?? А что если память кончится? А как возвращать ему память (free()) и переиспользовать её?
В общем виде этот компонент называется "аллокатор памяти" и реализовать его правильно - это грёбаная ядерная физика. В 90% случаев лучше всего взять сторонний а не делать самому.
Яннп если честно. Чем этот набор баззвордов, определяющих эту вашу парадигму "Голубого океана", отличается от типового списка ценностей типовой компании, который точно так же про customer trust, лояльность к брэнду итд? Что такого уникального во вкусвилле? Ну сеть продуктовых магазинов верхнего ценового сегмента. Иногда там могу закупиться, иногда в пятёрочке или перекрёстке. Ужас какой, я брэнду не лоялен.
Зачем? Alacritty есть в terminfo в современных дистрибутивах. TERM=alacritty / alacritty-direct. Установка TERM в xterm-256color в Alacritty чревата неработой настроек цветовой схемы Alacritty и возможно каких-то Esc-последовательностей, специфичных для Alacritty.
Numpy и в частности numpy.matmul предельно оптимизированы (вычисление numpy.matmul выполняет BLAS емнип), а все реализации matmul, используемые в данном тесте, достаточно наивны (просто проходится 3 вложенных цикла и делается умножение a_ik * b_kj, далее всё отдаётся на откуп компилятору).
На таких сравнительно небольших размерах матриц (1500x1500) эти 39 миллисекунд на python можно ускорить ещё в 2 раза, если отключить многопоточность :)
# перед импортом numpy!!!
import os
os.environ['OPENBLAS_NUM_THREADS'] = '1'
os.environ['NUMEXPR_NUM_THREADS'] = '1'
os.environ['MKL_NUM_THREADS'] = '1'
os.environ['OMP_NUM_THREADS'] = '1'
Вас не смущает, что Rust Java и Fortran в matmul обогнали C на порядок?)) Явно всё векторизовалось, как минимум в Rust: https://godbolt.org/z/6cvj9Y65r, а в C-LCC нет.
Вряд ли задача вида "open question in number theory—a good Ph.D.-level problem" - это посчитать набор чисел. Практически наверняка это задача на доказательство.
Также "came up with a problem" всё же означает что задача была именно что придумана на ходу.
Over the next 10 minutes, Ono watched in stunned silence as the bot unfurled a solution in real time, showing its reasoning process along the way. The bot spent the first two minutes finding and mastering the related literature in the field. Then it wrote on the screen that it wanted to try solving a simpler “toy” version of the question first in order to learn. A few minutes later, it wrote that it was finally prepared to solve the more difficult problem. Five minutes after that, o4-mini presented a correct but sassy solution.
Я конечно хреновый математик, но лично я валидировать решение небанальной математической задачи не смогу если его передо мной будут разворачивать в режиме реального времени. В спокойной обстановке, без лишних людей вокруг, с пачкой бумаги и карандашом, - и то минут 30 может влёгкую уйти только чтобы въехать, в чём состоит решение и правильными ли объектами оперирует автор (+дьявол может быть в неявных допущениях), и от часа и больше на попытки составления контрпримеров и т.д.
Что они там за 10 минут умудрились осознать и провалидировать я понятия не имею, но очень сомневаюсь, что то, чем они занимались эти 10 минут, являлось анализом решения по существу.
Upd: виноват поторопился - бывают наборы векторов равной длины, дающие сумму 0 и не образующие правильный многоугольник. Причём наботы как с чётным, так и с нечётным кол-вом элементов.
С чётным кол-вом: вектора из центра прямоугольника в его углы С нечётным кол-вом: все положения часовых стрелок кроме 3,4,8,9,12. (равносторонний треугольник 2 6 10 + крест 1 5 7 11).
Суровые у вас девятиклассники... Имхо достаточно просто доказать лемму, что если сумма векторов равной длины, равна нулю, то концы этих векторов, исходящих из 1 точки, образуют правильный многоугольник. Далее противоречие с простотой p.
Т.е. я правильно понимаю, что в качестве меры борьбы с вытеснением её профессии AGI она ушла в профессию, которую гипотетический AGI уничтожит ещё раньше? :)))
Я вообще к вам хотел попробоваться, но честно говоря бывшие тренеры по боксу в качестве core инженеров C++ меня очень смущают.
Как это вообще возможно?? Для поддержки ядра текстового редактора надо знать миллион вещей, всякие CRDT/gapbuffers/строковые кэши, обычно многопоточку, теорию по парсерам, C++ собственно на хорошем уровне, ядра пары других текстовых движков шапочно. Мейнтейнеры подобных движков, известные мне, все с бэкграундом в CS и при этом достаточно упоротые чтобы продолжать специализироваться в C++ со временем. А у вас так легко, взял из бокса вкатился, пилит
constexpr <auto> template MyLineStorage::fetchв кор команде... Кстати его ответ "Как пришёл в IT" освещает что угодно, но только не как он пришёл в IT."У вас нет контейнера для запуска гадости или вы не можете его создать за 5 минут, вы нам не подходите, прощайте".
Гм, не совсем. Несколькими страницами ниже:
"Пишется на ограниченном диалекте C" != "пишется на си".
Про Lean не в курсе, но Coq (закрою глаза на то, что это ЯП, а не система символьного вывода) является реализацией исчисления конструкций и следовательно подвержен всем ограничениям исчисления конструкций, например в Coq является выводимым парадокс Карри:
Нет таких символьных систем, в которых можно непротиворечиво вывести всю математику. Во-первых никто толком не договорился об аксиоматике (поэтому собственно и возможен мой пример выше), во-вторых есть теоремы Гёделя о неполноте.
Для программ и доказательств, записанных на формально верифицируемом языке. Что на сегодняшний день равняется 2.5 академическим ЯП в области программирования и примерно 0 универсальных формальных систем в области чистой математики.
Новое слово в системном программировании... FYI если в программе нет вызова exit и т.д., то проц просто продолжает выполнять опкоды, расположенные за программой в памяти. Как правило это заканчивается тем, что он выполняет что-то в non executable области, и как следствие segfault. Но всякое бывает, может случайно и сискол exit выполниться. Никакого "принудительного уничтожения" таких программ в Linux нет, их поведение просто не определено.
В целом как-то многовато пафоса для, видимо, набора типа "высокоуровневых" макросов для опкодов x86-64?
критиковал не столько решения openai, сколько язык записи доказательств у openai =) Само по себе решение #1 от openai, как оказалось, верное - перепроверил после всех разъяснений.
У Google значительно лучше, как минимум понятнее. В решении #1 тоже не нашёл ошибок.
Круто... Теперь хотелось бы увидеть не столько решения, сколько цепочки рассуждений модели. Как она выбирает, на чём основывать доказательство, по каким ложным путям ходит в процессе. И на чём записываются эти цепочки рассуждений, явно же внутри там какой-то аля prolog / rocq.
Моя картина мира пошатнулась если честно :( Я раньше думал, что такие трюки невозможны без AGI (т.е. в данном случае формализованной модели арифметики, наивной теории множеств, планиметрии и т.д. где-то внутри LLM).
Для справки: я phd по математике, занимаюсь (занимался) символьным выводом.
Спасибо за "не подкреплено знаниями по теме вопроса".
Язык этот я вижу первый раз, видимо что-то олимпиадное. Профессиональный язык в математике это нечто, пересыпанное кванторами и логическими связками, вот например - символика там мб весьма специфической и непонятной, но как минимум там фразы с логичной структурой, а не обрубки.
Не знаю, что там за общеизвестные обозначения, но Z с двумя индексами может обозначать всё, что угодно. Общеизвестное обозначение для данного множества из задачи это ℕ⊗ℕ или ℕ² или ℤ⁺⊗ℤ⁺ или даже {(x, y) | (x∈ℤ y∈ℤ x>0 y>0}. Не зная что там за объект, я вынужден докапываться даже до самых базовых объектов в условии, например для графов (не для наборов точек) "покрытие" может означать 2 вещи - покрытие рёбер и покрытие вершин. И мне странно, что дано условие задачи, в котором не устранена малейшая двусмысленность, при том что это можно сделать в половину строки хоть на этом псевдоязыке хоть в обычной математической нотации. В этот раз вы вроде интерпретировали верно, в иных условиях может не повезти.
Ссылку на решения что характерно не привели, разумеется ссылка на тг канал важнее.
https://github.com/aw31/openai-imo-2025-proofs
Посмотрел решение первой задачи, имхо это какой-то бред.
ИИ выдаёт решение на каком-то трудно читаемом языке, похожем на тот, что используется человеком в математических доказательствах, но состоящем из излишне коротких фраз, иногда грамматически некорректных, с сильной нехваткой логических связок между ними. Читать и валидировать это невозможно, например неясно где знак равенства означает "введём определение" (то что в нормальной нотации обозначается := или ≝), а где утверждение равенства. Могли бы помочь текстовые комменты, но ИИ не утруждает себя их написанием, равно как и написанием кванторов в определениях, что делает невозможным понимание определений. Чтобы не быть голословным:
Что значит "covering"? Что такое slope -1? Что такое Z и что означают индексы в ней? Что такое hyp. - hypotenuse, hypothesis, автор токены экономит???? Что такое "forbidden directions", мы же вроде на формальном языке пытаемся говорить?
Я не понимаю как кто-то реально может заявлять о своей способности провалидировать это решение.
Очень оторванный от реальности подход. Проблем у него миллион, навскидку хотя бы такие:
– Чтобы этот подход работал, нужен coding standard, регламентирующий АБСОЛЮТНО ВСЁ. Межблочные интервалы. Выравнивание знаков равенства в блоке похожих выражений var1 = value1. Шаг в сторону и летит любое кастомное форматирование кода. Вот например несколько способов записать массив чисел, пользуясь одним и тем же кодстайлом:
После roundtrip в AST и обратно будем выводить всё в 1 строку, да? Не всё кастомное форматирование является, как вы выражаетесь, "самовыражением". В некоторых случаях человек записал числа прямоугольником 2x3 потому что это способ наглядно представить данные, например там числа логически идут парами. В другом случае он вылез за разрешённую кодстайлом ширину текста 100 символов потому что иначе не влезает длинное объявление объекта. В третьем случае поставил 3 пустых строки, а не как по стандарту 1, вокруг какого-то блока, потому что там кластеры блоков кода. Исключения, исключения... Никогда и нигде в реальном проекте вы не встретите большого куска кода, способного без изменений пережить десериализацию в AST и сериализацию обратно.
– Чтобы этот подход работал, надо к каждому репозиторию с кодом иметь корректно парсящую его систему, которая может весить в разы больше скромного набора plaintext строк.
– Первый же реальный проект, в который вы притащите ваш редактор, начнётся с того, что там будет сторонний код, использующий собственный кодстайл (или не использующий вовсе), править который под "ваш" кодстайл и подключать ваш парсер никто не будет. Как взаимодействовать с таким кодом?
Так у вас в способе #2 MyHeap каждый раз выделяет блок только с бОльшим адресом?? А что если память кончится? А как возвращать ему память (free()) и переиспользовать её?
В общем виде этот компонент называется "аллокатор памяти" и реализовать его правильно - это грёбаная ядерная физика. В 90% случаев лучше всего взять сторонний а не делать самому.
Яннп если честно. Чем этот набор баззвордов, определяющих эту вашу парадигму "Голубого океана", отличается от типового списка ценностей типовой компании, который точно так же про customer trust, лояльность к брэнду итд? Что такого уникального во вкусвилле? Ну сеть продуктовых магазинов верхнего ценового сегмента. Иногда там могу закупиться, иногда в пятёрочке или перекрёстке. Ужас какой, я брэнду не лоялен.
Зачем? Alacritty есть в terminfo в современных дистрибутивах. TERM=alacritty / alacritty-direct. Установка TERM в xterm-256color в Alacritty чревата неработой настроек цветовой схемы Alacritty и возможно каких-то Esc-последовательностей, специфичных для Alacritty.
Numpy и в частности numpy.matmul предельно оптимизированы (вычисление numpy.matmul выполняет BLAS емнип), а все реализации matmul, используемые в данном тесте, достаточно наивны (просто проходится 3 вложенных цикла и делается умножение a_ik * b_kj, далее всё отдаётся на откуп компилятору).
На таких сравнительно небольших размерах матриц (1500x1500) эти 39 миллисекунд на python можно ускорить ещё в 2 раза, если отключить многопоточность :)
Вас не смущает, что Rust Java и Fortran в matmul обогнали C на порядок?))
Явно всё векторизовалось, как минимум в Rust: https://godbolt.org/z/6cvj9Y65r, а в C-LCC нет.
Вряд ли задача вида "open question in number theory—a good Ph.D.-level problem" - это посчитать набор чисел. Практически наверняка это задача на доказательство.
Также "came up with a problem" всё же означает что задача была именно что придумана на ходу.
Я конечно хреновый математик, но лично я валидировать решение небанальной математической задачи не смогу если его передо мной будут разворачивать в режиме реального времени. В спокойной обстановке, без лишних людей вокруг, с пачкой бумаги и карандашом, - и то минут 30 может влёгкую уйти только чтобы въехать, в чём состоит решение и правильными ли объектами оперирует автор (+дьявол может быть в неявных допущениях), и от часа и больше на попытки составления контрпримеров и т.д.
Что они там за 10 минут умудрились осознать и провалидировать я понятия не имею, но очень сомневаюсь, что то, чем они занимались эти 10 минут, являлось анализом решения по существу.
Upd: виноват поторопился - бывают наборы векторов равной длины, дающие сумму 0 и не образующие правильный многоугольник. Причём наботы как с чётным, так и с нечётным кол-вом элементов.
С чётным кол-вом: вектора из центра прямоугольника в его углы
С нечётным кол-вом: все положения часовых стрелок кроме 3,4,8,9,12. (равносторонний треугольник 2 6 10 + крест 1 5 7 11).
Суровые у вас девятиклассники... Имхо достаточно просто доказать лемму, что если сумма векторов равной длины, равна нулю, то концы этих векторов, исходящих из 1 точки, образуют правильный многоугольник. Далее противоречие с простотой p.