LINUX.ORG.RU
ФорумTalks

Так какие же языки программирования наиболее эффективны с точки зрения использования токенов?

 ,


0

4

Тут (martinalderson.com) наткнулся на интересный лонгрид. Имеется ввиду эффективность использования токенов при работе с ИИ агентами. Мы ведь на всех парах летим в светлое будущее, где кодит ИИ, а мы сидим под пальмой и хлебаем смузи. Так о чём это я.

Чем более эффективно исходный код токенизируется, тем лучше его понимает ИИ и лучше может его генерировать. Другими словами, для ИИ нужно больше смысла в меньшем кол-ве токенов. ИЧСХ, для лучшего понимания кода людьми нужно то же самое, а это положительно влияет на продуктивность.

Так вот, главный вывод из данного эксперимента следует не удивительный, большинство динамически типизируемых языков более эффективны по токенам, чем статически типизируемые. Но некоторые статические языки уверенно уделывают некоторые динамические. Т.е. дело не только в самой типизации, но и в конкретной имплементации. [вброс]Пламенный превед сишникам и жабаскриптерам 😛[/вброс]

Более общий вывод напрашивается интересный. Вместо бесконечных срачей на тему чей шворц длиннее какой язычок луче, у нас вырисовываются объективные, легко проверяемые критерии, какие фичи полезны для япов будущего, а какие не очень. Когда список утрясётся, останется собрать все полезные фичи в один яп, а все бесполезные выкинуть. И вуаля, вкалывают роботы кодит ИИ, а мы все идём хлебать смузи.



Последнее исправление: yvv1 (всего исправлений: 1)
Ответ на: комментарий от Obezyan

вот и поглядим.

специалистам из разных областей бывает непросто понять друг друга, поэтому я сначала решил не отвечать.

но кажется нашёл наглядный пример.

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

точно так же и в случае с формальной верификацией. правила проверки следующего «хода» в доказательствах довольно просты и укладываются, вероятно на один экран. Если агент попытается что то там мухлевать или пойти не тем путём, пруфчекер просто не позволит сделать такой «ход». поэтому получается что либо нейросеть будет доказывать так как надо, либо просто не докажет ничего. Ровно как в шахматах. поэтому у специалистов такого вопроса не возникает.

AndreyKl ★★★★★
()
Последнее исправление: AndreyKl (всего исправлений: 1)
Ответ на: комментарий от AndreyKl

специалистам из разных областей бывает непросто понять друг друга

Специалисты знают что:

  1. Проверяется не «истина» (тм), а выводимость.
  2. Ядро пруфчекера, например, Coq – это обычная программа, которая также подвержена ошибкам как и любая другая программа.
Obezyan
()
Ответ на: комментарий от Obezyan

Проверяется не «истина» (тм), а выводимость.

вообще не понял. выводимость как раз и означает что в рамках данных посылок и системы вывода, выводимое положение истинно. выводимость и истинность не синонимы только в отношении аксиом - аксиомы принимаются как истинные, но они не выводимы, на то они и аксиомы. в чём противоречие?

Ядро пруфчекера, например, Coq – это обычная программа, которая также подвержена ошибкам как и любая другая программа.

однако ядро - программа достаточно маленькая и достаточно надёжная. вы верно привели страничку багов, но как вы сами можете видеть оттуда же, непофикшенных багов немного, а риски ими представляемые - минимальны.

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

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

AndreyKl ★★★★★
()
Последнее исправление: AndreyKl (всего исправлений: 3)
Ответ на: комментарий от Obezyan

Ну это мягко говоря - не так. Они способы воспринимать контекст, запоминать, работать на его основе. Если вы предложите нейросетке новые условия, она сможет работать на их основе. Другой вопрос, что чисто физически нужно говородить это до обучение ну основе контекстов.

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

LightDiver ★★★★★
()
Ответ на: комментарий от AndreyKl

формальной верификацией

Я так понял, у вас какая-то специфическая формализованная область. Но как это будет выглядеть для обычных программ? Вряд ли оно может быть универсальным (иначе это было бы давно внедрено без всякого ИИ), как будто бы такой пруфчекер будет написать чуть ли не сложнее, чем саму программу.

MoldAndLimeHoney ★★
()
Ответ на: комментарий от LightDiver

Я дохрена инае умею. Фигня не та же.

Ты не понимаешь просто, что тостер не может программировать так, как может человек. Он умеет только воровать код у других людей и подбирать его по паттернам. Там нет рассуждения логики работы программы, нет архитектуры.

Bfgeshka ★★★★★
()
Ответ на: комментарий от Bfgeshka

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

LightDiver ★★★★★
()
Ответ на: комментарий от LightDiver

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

Буквально нет, работа производится иначе принципиально. Дело не во «внешних доп костылях», что бы это не было.

Если приближать к твоей аналогии, то будет так: либо ты проектируешь себе дом сам, либо запускаешь тетрис и ждёшь, пока тебе бот не соберёт что-то похожее на дом.

Bfgeshka ★★★★★
()
Ответ на: комментарий от LightDiver

Конечно я знаю, я этот вопрос в универе ещё начал изучать. Даже писал типичный пример нейросетей (OCR).

Нет, думать оно не может, это ненастоящие нейроны.

Bfgeshka ★★★★★
()
Ответ на: комментарий от AndreyKl

вы сами можете видеть оттуда же, непофикшенных багов немного, а риски ими представляемые - минимальны.

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

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

Я не понимаю, зачем вы спорите с логикой, но это ваше право.

Obezyan
()
Ответ на: комментарий от LightDiver

Ну это мягко говоря - не так.

Это так и мягко, и жестко. Обычное числовое сито из конца 60х начала 70х годов прошлого века, с градиентным спуском, обратным распространением ошибки и весами активаций нейронов. Т.е. то самое числовое сито. И Transformers и Mamba и даже механизм внимания - все это относится к числовым ситам.

Obezyan
()
Ответ на: комментарий от LightDiver

Технология пусть и упрощенная, но основанная на той же фигне, что и у тебя.

Вообще не так. Похоже, что у вас сейчас конфетно-букетный период очарования современныими LLM.

Это как сравнивать первые калькуляторы и современный комп и рассказывать, что калькулятор считать не умеет, потому что у него видеокарты нет.

Вы делаете именно это, сравниваете первые калькуляторы (LLM) и современный комп (биологический мозг).

Obezyan
()
Ответ на: комментарий от MoldAndLimeHoney

Я так понял, у вас какая-то специфическая формализованная область. Но как это будет выглядеть для обычных программ? Вряд ли оно может быть универсальным (иначе это было бы давно внедрено без всякого ИИ), как будто бы такой пруфчекер будет написать чуть ли не сложнее, чем саму программу.

Область обычная - практически любые программы.

Технология примерно такая: берётся программа, переводится транспиллером в rocq/lean. Потом пишутся спецификации и доказательства.

Условно, это гарантирует 100% отсутствие «обычных» багов.

«Обычных» это значит что например баг типа «padding oracle attack» ловится только с использованием спецификации криптографических примитивов, что отдельная тема.

«Условно» потому что баги компилятора и операционной системы, а так же баги железа, если эти компоненты не верифицированы (а они не верифицированы в обычной жизни) остаются естественно там где были, то есть на своём месте.

После поимки «обычных» багов и багов со специальными спецификациями (вроде криптографии), можно (если нужно) строить модели безопасности и доказывать что 1) эти модели действтиельно обеспечивают безопасность, 2) что программа соответствует построенной модели, но это уже на самом деле следующий уровень надёжности (например, это делалось при верификации Астра-Линукс)

Но обычные баги которые портят жизнь в 99 наверное процентах случаев, ловятся на 100%, т.е. все и без дополнительных сложностей.

Ну правда тут вот скандалец был в феврале ( https://symbolic.software/blog/2026-02-12-cryspen-response/ ): ребята из компании Cryspen, авторы крипто библиотеки libcrux , заявляли что у них верифицированная библиотека. Но на деле оказалось что немного преувеличивали: 1) верифицирована часть библиотеки на самом деле,а не вся; 2) у них стояли настройки в пайплайне которые в отдельных случаях отключали проверки. Соотвественно, были шансы не поймать баги.

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

Но если добросовестно, то 100% «обычных» багов ловятся.

Загвоздка в том что удовольствие довольно дорогое. Скажем год назад я бы сказал что верификация кода будет раз в 5 дороже его разработки.

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

Т.е. это применимо например к ядрам платёжных систем и т.п. критических местах.

AndreyKl ★★★★★
()
Последнее исправление: AndreyKl (всего исправлений: 3)
Ответ на: комментарий от Obezyan

Я не понимаю, зачем вы спорите с логикой, но это ваше право.

Вы правы, это может быть (хотя и маловероятно*). Но я спорю не с этим. Я спорю с тем что это что то значит в контексте беседы.

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

*Уточнение: маловероятно на мой взгляд что нейросеть пытаясь доказать найдёт и будет использовать баги чекера - это примерно как если бы нейросеть пыталась использовать баги программы для игры в шахматы. какие то шансы есть, но они впринципе не так обучаются для этого, поэтому вероятно и пытаться не будут.

По крайней мере те что есть сейчас неспециализированные (вроде опуса 4.6) тупо не могут ничего более-менее сложного доказать. а специализированные - либо доказывают, либо не доказывают. всё как обычно у людей, багов пока не нашли (и не видно чтобы пытались). доказывают, кстати очень неплохо.

AndreyKl ★★★★★
()
Последнее исправление: AndreyKl (всего исправлений: 6)
Ответ на: комментарий от Obezyan

и, мы как то тут зациклились на верификации, но в контесте беседы есть ещё один аргумент: ну будут нейросети писать тесты , а потом писать код. будем жить как жили, людей точно так же глючит (иначе багов бы не было, очевидно). ну как жить как жили.. кто то без работы останется..

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

если пару лет назад незамечать изменений было просто напросто не очень дальновидно (каюсь, сам такой), то сегодня тут уместно уже совсем другое слово.

AndreyKl ★★★★★
()
Последнее исправление: AndreyKl (всего исправлений: 2)
Ответ на: комментарий от AndreyKl

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

Да, сейчас у многих этап принятия нового через отторжение, потом будет очарование, потом осознавание, что это просто новый калькулятор.

За последние 10 лет качество кода в среднем упало на 50%. Те его стало больше, но качество ухудшилось. Все это сети впитывают через обучающие датасеты. В итоге, производительность вырастет, а качество еще больше упадет.

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

Те я согласен с тем что вы написали, но пока не вижу смысла уезжать в деревню, т.к. чем дальше тем больше мои услуги будут востребованы. И по обучению сетей, и по написанию качественного кода, и по общей экспертизе системной архитектуры.

Obezyan
()
Последнее исправление: Obezyan (всего исправлений: 1)
Ответ на: комментарий от Obezyan

что это просто новый калькулятор

единственное, что хотелось бы уточнить - по моему это станок. новый станок. калькулятор таких драмматических последствий не принёл, а станок таки да.

а так да, со всем согласен. тольк не знаю сколько из нас остануться нужны через 5-10 лет, хорошо если 10%, а если 1%?

AndreyKl ★★★★★
()
Ответ на: комментарий от AndreyKl

единственное, что хотелось бы уточнить - по моему это станок.

Да, станок с ЧПУ, ваша аналогия точнее.

Obezyan
()
Закрыто добавление комментариев для недавно зарегистрированных пользователей (со score < 50)