Чтобы вместо разгребания багрепортов на свой собственный быстрый рендер текста заниматься сотней эмуляторов терминала?
Ну AI впихивать время нашли, могли бы более полезным заняться. Emacs, Vim, Kakoune, Xi умеют и tty и gui фронтенд без проблем, а эти видите ли не могут. Кроме того, в статье как раз и демонстрируется, что привязка к определённому рендереру может в будущем аукнуться.
Да и сколько нужно этих редакторов в терминале чтобы хватило?
Проблема в том, что тюнинг редактора под себя требует времени. Под "временем" я понимаю годы. Это развитие своих хоткеев, плагинов, изучение и введение в эксплуатацию чужих плагинов. Держать и развивать под себя 2 редактора, 1 для консоли, один для DE - слишком дорогое удовольствие.
Наверное лучшее решение в современном мире - практически натив в песочнице. Кстати из Rust компилировать не обязательно, есть ещё куча языков, умеющих в WASM.
По такой логике нативные плагины вообще не должны существовать, а то вдруг сегфолтнется, ужас какой. Редактор - не панель управления ядерным реактором, так что я считаю, что гипотетическая возможность вылета такого некритичного приложения, как текстовый редактор, при использовании сторонних плагинов - более чем умеренная плата за более простую архитектуру и улучшенную производительность бинарных плагинов.
Был бы заявкой на лучший редактор в мире, если бы поддерживал работу в терминале - которая в Zed невозможна тк он гвоздями прибит к Vulkan (под Linux) и рендерингу в графической среде.
Т.е. я правильно понимаю, что в качестве меры борьбы с вытеснением её профессии 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" всё же означает что задача была именно что придумана на ходу.
Ну AI впихивать время нашли, могли бы более полезным заняться. Emacs, Vim, Kakoune, Xi умеют и tty и gui фронтенд без проблем, а эти видите ли не могут. Кроме того, в статье как раз и демонстрируется, что привязка к определённому рендереру может в будущем аукнуться.
Проблема в том, что тюнинг редактора под себя требует времени. Под "временем" я понимаю годы. Это развитие своих хоткеев, плагинов, изучение и введение в эксплуатацию чужих плагинов. Держать и развивать под себя 2 редактора, 1 для консоли, один для DE - слишком дорогое удовольствие.
По такой логике нативные плагины вообще не должны существовать, а то вдруг сегфолтнется, ужас какой. Редактор - не панель управления ядерным реактором, так что я считаю, что гипотетическая возможность вылета такого некритичного приложения, как текстовый редактор, при использовании сторонних плагинов - более чем умеренная плата за более простую архитектуру и улучшенную производительность бинарных плагинов.
Я имею в виду не способность вызывать терминал, а способность работать внутри терминала.
Был бы заявкой на лучший редактор в мире, если бы поддерживал работу в терминале - которая в Zed невозможна тк он гвоздями прибит к Vulkan (под Linux) и рендерингу в графической среде.
Также очень странный подход к архитектуре плагинов, которые надо обязательно компилировать из Rust в WASM тк разработчики панически боялись, что чужой плагин может крашнуть редактор https://zed.dev/blog/language-extensions-part-1#challenges-with-packaging-parsers
Т.е. я правильно понимаю, что в качестве меры борьбы с вытеснением её профессии 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" всё же означает что задача была именно что придумана на ходу.