У меня самое дешманское открытое шасси с Али, мать Machinist X99 и три видеокарты, одна из которых стоит над другими на напечатанном креплении, и подключается к PCIe удлиннителем 20см. Отлично работает. Я бы мог подключить ещё одну, но смысла в этом не очень много.
Очень круто! Автор просто красавчик, что не бросил затею на пол пути. Теперь можно было бы сделать печатную плату. Но если автор откажется, я его всецело пойму :)
Ну вот я видел результаты тестов разного квантования, например, у Unsloth. По ним можно сделать вывод, что Q4 совсем незначительно уступает Q8. Но автор говорит, что это всё лоботомия, и кодить скрипты на питоне на Q4 категорически нельзя. Вот хотелось бы доказательств.
Это старые данные. Модель в таком виде была на HF несколько дней после публикации 3.5. Она действительно была глючной. Потом поправили, и размер её стал на 2Г больше.
На такой квантизации уже сильно падает качество. UD-Q4_K_XL - ещё норм, но если ниже, то очень заметна разница.
И по поводу скорости. 10-20 токенов на генерации терпимо, но низкая скорость на промпте - это прям грустно, особенно когда делается сжатие контекста. А на 80к это часто надо делать.
Всё ж надо пару, а лучше тройку 3090, чтобы cpu разгрузить. И контекст побольше. Но это моё ИМХО, не настаиваю.
Базовый синтез RTL, ограниченную проверку (BMC) с использованием SMT-решателя Z3. Подходит для небольших дизайнов и простых assert/assume.
Yosys+SBY - не только BMC и не только Z3. Там в полной мере поддерживается k-induction prove, и кроме Z3 там ещё десяток солверов, в т.ч. встроенный прямо в Yosys, который используется в EQY - LEC на базе Yosys.
А что касается простых assert/assume, то на них (плюс liveness) можно реализовать всё, что есть в SVA. Только текста больше получится.
Так что опенсорс не так плох как может показаться.
Отсутствие поддержки SVA - это печально, но при желании можно обойтись immediate assertions. Больше писанины, но оно работает, народ использует (в т.ч. и я).
Пока не понятно какую гипотезу необходимо доказать
Вот эту:
Это не так должно работать.
Должно работать в пайплайне из трёх агентов и RAG? Охотно верю, но хочется реальной проверки, а не просто слов. Мне вот чатгпт после разбора статьи предложил вариант пайплайна из 10 пунктов. Но это из разряда "Да, вы совершенно правы...".
Про то, что там в статье за гипотеза - это надо у Юрия спросить. Я там чёт не нашел упоминаний RAG, Каммингса и Харриса (кроме списка литературы).
Но могу из своего опыта привести пример. И использованием современных средств ИИ-разработки - спецификации, планирования, ревью на всех этапах, мультиагентной системы, функциональных тестов и формальных проверок (с помощью Yosys и SBY, кстати) - ИИ не смог написать FWFT FIFO на блочной памяти (с латентностью чтения и некоторыми дополнительными условиями). Точнее смог в конце концов, но с моей помощью.
Архитектурная задача на одном агенте с галлюцинирующей моделью не решается
Решите с несколькими. Тут-то ситуация простая - есть задача и есть неудачные попытки её решения. Если вы уверены, что её решали неправильно, покажите правильное решение (решение, а не рассуждения о том, как правильно).
У меня самое дешманское открытое шасси с Али, мать Machinist X99 и три видеокарты, одна из которых стоит над другими на напечатанном креплении, и подключается к PCIe удлиннителем 20см. Отлично работает. Я бы мог подключить ещё одну, но смысла в этом не очень много.
Очень круто! Автор просто красавчик, что не бросил затею на пол пути. Теперь можно было бы сделать печатную плату. Но если автор откажется, я его всецело пойму :)
Ну вот я видел результаты тестов разного квантования, например, у Unsloth. По ним можно сделать вывод, что Q4 совсем незначительно уступает Q8. Но автор говорит, что это всё лоботомия, и кодить скрипты на питоне на Q4 категорически нельзя. Вот хотелось бы доказательств.
На словах красиво, а есть цифры? Хочется осязаемых метрик, а не размышлений на тему. И результатов тестов тоже хочется. Какие ваши доказательства? (С)
А исходники будут?
Это старые данные. Модель в таком виде была на HF несколько дней после публикации 3.5. Она действительно была глючной. Потом поправили, и размер её стал на 2Г больше.
Сравните с VexRiscv. По моим тестам у него лучшее отношение производительности к площади.
Для использования 75-омного кабеля можно попробовать поставить терминаторы на 75 Ом (можно просто резистор в разъём воткнуть).
На такой квантизации уже сильно падает качество. UD-Q4_K_XL - ещё норм, но если ниже, то очень заметна разница.
И по поводу скорости. 10-20 токенов на генерации терпимо, но низкая скорость на промпте - это прям грустно, особенно когда делается сжатие контекста. А на 80к это часто надо делать.
Всё ж надо пару, а лучше тройку 3090, чтобы cpu разгрузить. И контекст побольше. Но это моё ИМХО, не настаиваю.
Выложили https://huggingface.co/collections/Qwen/qwen36
Какой сетап?
На днях в режиме планирования:
И создал :)
Yosys+SBY - не только BMC и не только Z3. Там в полной мере поддерживается k-induction prove, и кроме Z3 там ещё десяток солверов, в т.ч. встроенный прямо в Yosys, который используется в EQY - LEC на базе Yosys.
А что касается простых assert/assume, то на них (плюс liveness) можно реализовать всё, что есть в SVA. Только текста больше получится.
Так что опенсорс не так плох как может показаться.
Отсутствие поддержки SVA - это печально, но при желании можно обойтись immediate assertions. Больше писанины, но оно работает, народ использует (в т.ч. и я).
Я ничего не утверждаю. Это вы утверждаете, что решит. Но пока кроме утверждений ничего не видно.
Я пробовал с Клодом, GPT, GLM, Qwen и с некоторыми локальными моделями. Gemini не пробовал.
Вот эту:
Должно работать в пайплайне из трёх агентов и RAG? Охотно верю, но хочется реальной проверки, а не просто слов. Мне вот чатгпт после разбора статьи предложил вариант пайплайна из 10 пунктов. Но это из разряда "Да, вы совершенно правы...".
Про то, что там в статье за гипотеза - это надо у Юрия спросить. Я там чёт не нашел упоминаний RAG, Каммингса и Харриса (кроме списка литературы).
Но могу из своего опыта привести пример. И использованием современных средств ИИ-разработки - спецификации, планирования, ревью на всех этапах, мультиагентной системы, функциональных тестов и формальных проверок (с помощью Yosys и SBY, кстати) - ИИ не смог написать FWFT FIFO на блочной памяти (с латентностью чтения и некоторыми дополнительными условиями). Точнее смог в конце концов, но с моей помощью.
В тексте есть ссылки на статью и на задание. Не понимаю, что ещё нужно.
Решите с несколькими. Тут-то ситуация простая - есть задача и есть неудачные попытки её решения. Если вы уверены, что её решали неправильно, покажите правильное решение (решение, а не рассуждения о том, как правильно).
Покажите как. Решите задачу из статьи с помощью своего пайплайна.