О, попытка давить авторитетом целых тысяч математиков. Сразу видно оппонент об этом всё знает. Жаль, только по контексту “эмипирическое наблюдение людей разрабатывавших софт” не догадался, что речь не о Колмогоровской сложности
В нём фундаментальности столько же, сколько в народных мудростях. Эмпирическое наблюдение людей разрабатывавших софт 50 лет назад это не “фундаментальный закон инженерии программного обеспечения”
Конструктивная математика даёт алгоритм разложения числа любой разрядности на простые числа за конечное время, безотносительно того, насколько “разумным” оно кажется конкретному исследователю. А неконструктивная математика вообще не даёт никаких алгоритмов.
С практической точки зрения программа работающая за 1e100 лет и незавершающаяся программа одинаково бесполезны.
Слышал об этом, но не встречал интересных ресурсов о практическом применении. Буду рад, если поделитесь ссылкой.
Ещё, в соседнем lean4, вроде как, много чего интересного формализуют и верифицируют (в том числе, с помощью ИИ), но в его экосистему я не очень погружён
Что же до “сложности кодирования” посредством индуктивных конструкций - это не более чем вопрос обучения и привычек (а также конкретного языка кодирования).
В CIC, поскольку это логическая теория, нельзя писать незавершимые функции. Одно только это делает программирование гораздо сложнее, потому нужно бороться termination checker-ом при записи привычных алгоритмов. Вот пример из агды, где для определения обычной функции деления приходится доказывать фундированность натуральных чисел.
Противопоставление позитивизма, прагматизма, материализма, эмпириокритицизма, инструментализма и тому подобных «-измов» друг другу — всё это больше напоминает детсадовские войны за внимание воспитательницы. Наиболее же обобщённым критерием «научности» является именно полезность знаний, возможность их применения во благо всего человечества.
В первом предложении вы критикуете противопоставления философских течений, во втором утверждаете, что прагматизм самое правильное.
Но какова практическая польза от самого факта, что эти котики «могут существовать»? Верно, никакой. А конструктивное доказательство обязано было бы предоставить такого страшного котика, вывести его из условия задачи.
Если доводить тезис о практической пользе до логического завершения, то конструктивная математика тоже будет антинаучной. Она утверждает, что любое число можно разложить на простые, но не существует алгоритма, который разложил бы любое 16384-битное число за разумное время. Получается, истинная математика должна быть ультрафинитной. Более того, у разных людей граница между настоящей и выдуманной математикой проходит по-разному. Кто-то может считать только на cpu старенького ноутбука, а у кого-то есть доступ к вычислительному кластеру, и практически решаемые задачи у них, очевидно, разные.
У тех, кто «не хочет задумываться», просто не остаётся выбора, как довериться авторитетным мнениям.
Когнитивные ресурсы тоже конечны и тоже стоят денег. Если какую-то задачу можно решить с помощью ООП, следуя догмам дяди Боба, то нет смысла нанимать светил науки, чтобы они ту же задачу решали на какой-нибудь агде, или диалекте ML с сепарационной логикой поверх него
Обеспечить стабильность, выразительность, качество кода помогает прежде всего полиморфное типизированное лямбда-исчисление. Эта дисциплина формализует рассуждения о корректности алгоритмов и предоставляет наиболее минималистичные фундаментальные абстракции для программирования.
Исчисление индуктивных конструкций ещё более выразительно и даёт ещё больше инструментов для рассуждений о корректности, но писать на нём практический код невероятно сложно.
LLM может применять языки формальной верификации, но только брутфорсом, т.е. бессмысленным перебором, в серии экспериментов.
Не соответствует наблюдаемым данным. ЛЛМки на самом деле довольно неплохо доказывают различные теоремы. Особенно, если генерировать доказательство не за один раз, а поэтапно, с фитбеком от прувера
Любые профессии, в основе которых математика и логика, надежно защищены от того, что сейчас называют "ИИ". С одной стороны, принципиально непреодолима граница между, грубо говоря, таблицей умножения, в которой нет галлюцинаций, и любой вероятностной "нейросетью", в которой галлюцинации есть. Никакие мультиагенты тут не помогут.
Проблема корректности давно решена другими средствами: системами проверки доказательств типа lean4 и rocq. А алгоритмическая проверяемость вывода в логике первого порядка (та логика, которой пользуется подавляющее большинство математиков) это вообще результат столетней давности
Это ж просто особенность датасета на котором дообучали модель. Дообучать можно и по-другому, так, чтобы модель пользователю перечила, если тот несёт бред. Причём, уже даже бенчмарки меряющие это начали появляться
И он будет вынужден ее решать методами, которые вам не понравятся (детект блокировщиков, DRM и прочее)
Флаг им в руки. Ютуб монополист пока не начал монетизироваться. Когда начнёт, то куча пользователей откроют для себя альтернативы от rumble до каких-нибудь поделок поверх ipfs
Все посчитано и изучено, рекламу по ТВ смотрят, она работает, иначе она не стоила бы столько.
Но даже если засчитывается, в итоге это сыграет негативно - все больше людей будут переходить на блокировщик, эффективность её сильно упадет, цена показа тоже, автор контента получит меньше.
Это проблема гугла, не пользователей.
С телевизором такое не выйдет, люди все равно не станут массово выключать его или все разом ходить в туалет.
Мой опыт просмотра фильмов/матчей по ТВ говорит, что будут. Отойти взять еды, воды попить или в туалет сходить, пока показ не продолжился, это, кажется, довольно стандартная история.
В случае Ютуба, цена товара - это просмотр рекламы, либо оплата подписки премиум. Все остальное нарушает основной принцип торговли, и называется либо воровство, либо грабеж.
Грабёж это когда не запускаешь рекламный скрипт на своём компе, всё верно. Выключать ТВ или отходить в туалет, когда включается реклама, можно, или тоже воровство/грабёж?
А вы ввели меня в заблуждение, говоря, что для RSA требуется простое число.
Я не вводил вас в заблуждение. Для работы RSA требуется простое число, иначе сложность разложения (а вместе с ней и криптостойкость) падает. Вы просто в очередной раз подгоняете реальность, где используется вероятностный генератор, под ваши представления, где всё, что используется гарантировано работает.
Насколько я понял, это ослабление сформулировано именно по алгоритму Миллера-Рабина. То есть не алгоритм подогнан под требования, а требования под то, что может выдать алгоритм.
Первые реализации RSA использовали тест Соловея-Штрассена, который слабее Миллера-Рабина. По вашей логике, видимо, тоже требования под алгоритм подогнали. Зачем только потом переезжать на тест посильнее остаётся загадкой: всё ведь и со старым гарантировано работало.
Отлично! Вам осталось только осознать, что это и есть пример ослабления требования от "работает всегда" до "работает практически всегда" и можем расходиться
Уже есть лет 30 как: xmpp
О, попытка давить авторитетом целых тысяч математиков. Сразу видно оппонент об этом всё знает. Жаль, только по контексту “эмипирическое наблюдение людей разрабатывавших софт” не догадался, что речь не о Колмогоровской сложности
В нём фундаментальности столько же, сколько в народных мудростях. Эмпирическое наблюдение людей разрабатывавших софт 50 лет назад это не “фундаментальный закон инженерии программного обеспечения”
Это какие?
С практической точки зрения программа работающая за 1e100 лет и незавершающаяся программа одинаково бесполезны.
Верифицированный компилятор си
Логика Хоара построенная поверх него
Фреймворк для верификации конкуррентных алгоритмов, пример верификации в этом фреймворке
Ещё, в соседнем lean4, вроде как, много чего интересного формализуют и верифицируют (в том числе, с помощью ИИ), но в его экосистему я не очень погружён
В CIC, поскольку это логическая теория, нельзя писать незавершимые функции. Одно только это делает программирование гораздо сложнее, потому нужно бороться termination checker-ом при записи привычных алгоритмов. Вот пример из агды, где для определения обычной функции деления приходится доказывать фундированность натуральных чисел.
В первом предложении вы критикуете противопоставления философских течений, во втором утверждаете, что прагматизм самое правильное.
Если доводить тезис о практической пользе до логического завершения, то конструктивная математика тоже будет антинаучной. Она утверждает, что любое число можно разложить на простые, но не существует алгоритма, который разложил бы любое 16384-битное число за разумное время. Получается, истинная математика должна быть ультрафинитной. Более того, у разных людей граница между настоящей и выдуманной математикой проходит по-разному. Кто-то может считать только на cpu старенького ноутбука, а у кого-то есть доступ к вычислительному кластеру, и практически решаемые задачи у них, очевидно, разные.
Когнитивные ресурсы тоже конечны и тоже стоят денег. Если какую-то задачу можно решить с помощью ООП, следуя догмам дяди Боба, то нет смысла нанимать светил науки, чтобы они ту же задачу решали на какой-нибудь агде, или диалекте ML с сепарационной логикой поверх него
Исчисление индуктивных конструкций ещё более выразительно и даёт ещё больше инструментов для рассуждений о корректности, но писать на нём практический код невероятно сложно.
Эта оптимизация давным-давно вшита в компиляторы
Не соответствует наблюдаемым данным. ЛЛМки на самом деле довольно неплохо доказывают различные теоремы. Особенно, если генерировать доказательство не за один раз, а поэтапно, с фитбеком от прувера
Думают, экспериментируют, понемногу выстраивают понимание языка и в конце-концов решают поставленную проблему
Проблема корректности давно решена другими средствами: системами проверки доказательств типа lean4 и rocq. А алгоритмическая проверяемость вывода в логике первого порядка (та логика, которой пользуется подавляющее большинство математиков) это вообще результат столетней давности
Ну мы же в предположении, что пользователь
шизне может сам отделить когда ИИ бредит, а когда нетА ютуб уже поборол блокировщики рекламы?
Это ж просто особенность датасета на котором дообучали модель. Дообучать можно и по-другому, так, чтобы модель пользователю перечила, если тот несёт бред. Причём, уже даже бенчмарки меряющие это начали появляться
Флаг им в руки. Ютуб монополист пока не начал монетизироваться. Когда начнёт, то куча пользователей откроют для себя альтернативы от rumble до каких-нибудь поделок поверх ipfs
Эта же логика применима к рекламе в интернете
Это проблема гугла, не пользователей.
Мой опыт просмотра фильмов/матчей по ТВ говорит, что будут. Отойти взять еды, воды попить или в туалет сходить, пока показ не продолжился, это, кажется, довольно стандартная история.
Так, а отличие от блокировщиков тут в чём? AdNauseam вот даже по ссылкам проходит, чтобы всё точно засчиталось
Грабёж это когда не запускаешь рекламный скрипт на своём компе, всё верно. Выключать ТВ или отходить в туалет, когда включается реклама, можно, или тоже воровство/грабёж?
https://ru.wikipedia.org/wiki/Ирония
Я не вводил вас в заблуждение. Для работы RSA требуется простое число, иначе сложность разложения (а вместе с ней и криптостойкость) падает. Вы просто в очередной раз подгоняете реальность, где используется вероятностный генератор, под ваши представления, где всё, что используется гарантировано работает.
Первые реализации RSA использовали тест Соловея-Штрассена, который слабее Миллера-Рабина. По вашей логике, видимо, тоже требования под алгоритм подогнали. Зачем только потом переезжать на тест посильнее остаётся загадкой: всё ведь и со старым гарантировано работало.
Отлично! Вам осталось только осознать, что это и есть пример ослабления требования от "работает всегда" до "работает практически всегда" и можем расходиться