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