TGTGInsighttelegram intelligenceLIVE / telegram public index
← Python Заметки
Назад кон каналите

TGINSIGHT SIMILAR POSTS

Најди сличен содржај

Изворен канал @pythonotes · Post #32 · 7 фев.

Погледај објаваПогледај оригинал

Скорее всего уже слышали, что складывать строки через + это плохая практика. Падение производительности, и всё такое. Без лишних слов, давайте измерять: from timeit import timeit def t1(): # складываем 10 строк через + из переменной t = 'text' for _ in range(1000): s = t + t + t + t + t + t + t + t + t def t2(): # склеиваем список строк через метод join arr = ['text'] * 10 for _ in range(1000): s = ''.join(arr) def t3(): # складываем через + но не из переменной а непосредственно инлайн объекты for _ in range(1000): s = 'text' + 'text' + 'text' + ... # всего 10 раз Теперь каждую строку склейки запустим по 10М раз >>> timeit(t1, number=10000) 0.21951690399964718 >>> timeit(t2, number=10000) 1.4978306379998685 >>> timeit(t3, number=10000) 0.2213820789993406 Хм, а нам говорили что через "+" это плохо и медленно ))) 😁 Тут стоит учитывать, что речь идёт о склейке множества длинных строк. Давайте изменим условия: def t4(): t = 'text'*100 for _ in range(1000): s = t + t + t + t + t + t + t + t + t def t5(): arr = ['text'*100] * 10 for _ in range(1000): s = ''.join(arr) def t6(): for _ in range(1000): s = 'text'*100 + 'text'*100 + ... # всего 10 раз >>> timeit(t4, number=10000) 12.795130728000004 >>> timeit(t5, number=10000) 2.642637542999182 >>> timeit(t6, number=10000) 0.2184546610005782 Вот, уже другой разговор, сразу видна разница, в среднем в 6 раз. Но погодите, почему последний тест t6() по скорости такой же как и t3()? Ведь строки теперь в 100 раз длиннее! Это вопросы оптимизации кода, какие простые изменения ускоряют или замедляют выполнение программы. Мы столкнулись с примером обхода обращения к переменной. Например, именно так работает директива #define в С++, во время компиляции подставляя значение переменной вместо ссылки на неё. В Python это тоже работает, но часто ли вы сможете встретить такой способ работы со строками? К сожалению, способ почти только теоретический. В целом, тесты показали то, что мы хотели. Делаем выводы самостоятельно. Полный листинг 🌍 #tricks

Hashtags

#define#tricks
Резултати

Пронајдени 1 слични објави

Пребарај: #ttrl

当前筛选 #ttrl清除筛选
Machinelearning

@ai_machinelearning_big_data · Post #8037 · 12.07.2025 г., 13:04

Најди сличноПогледај

🌟 Теперь поговорим подобнее про Kimina-Prover-72B: Это модель, которая не просто доказывает теоремы, а учится на своих ошибках. Kimina-Prover-72B создана на базе Qwen2.5-72B, которая бьет рекорды в формальной математике на Lean 4 и ее облегченные версии 8 и 1,7 миллиарда параметров. Numina - это некоммерческая научная коллаборация, ориентированная на развитие ИИ в области математики. Ее миссия: создание и публикация обширных баз данных математических задач, разработку open-source ИИ-решателя для их обработки и инструментов для поддержки совместной работы людей и ИИ в фундаментальных науках. На популярном бенчмарке miniF2F Kimina-Prover-72B достигла внушительной точности в 92.2%, оставив позади Deepseek-Prover-V2 671B. 🟡Ключевая фишка Kimina-Prover - агентный фреймворк для поиска доказательств Test-Time Reinforcement Learning. Вместо того чтобы пытаться решить сложную задачу в лоб, система научилась декомпозировать ее. Она самостоятельно генерирует, комбинирует и применяет промежуточные утверждения, или леммы, выстраивая из них длинные логические цепочки. По сути, это рекурсивный поиск: для доказательства основной теоремы модель может сначала доказать несколько вспомогательных лемм. 🟡Механика доказательств. Система отслеживает «рейтинг полезности» каждой леммы и отбраковывает те, что ведут в тупик. Вторым эшелоном идет механизм проверки на вменяемость. Прежде чем использовать новую лемму, модель пытается доказать ее отрицание. Если это удается, значит, лемма противоречива и ее сразу выбрасывают. Такая комбинация гарантирует логическую строгость и надежность всего доказательства. 🟡Kimina-Prover умеет учиться на ошибках. В отличие от других систем, которые в случае неудачи просто начинают заново, Kimina-Prover умеет читать сообщения об ошибках от компилятора Lean и предлагать исправления. Для этого ее специально дообучали на датасете из комбинаций «неверное доказательство – фидбэк – верное доказательство». Чтобы обучение шло стабильно, использовали стратегию Batched Failure Replay: все неудачные попытки с одной итерации собираются и используются как обучающий батч для следующей. И это оказалось куда эффективнее, чем бездумный перебор вариантов при том же бюджете вычислений. 📌Лицензирование: MIT License. 🟡Статья 🟡Набор моделей 🟡Demo 🖥GitHub @ai_machinelearning_big_data #AI#ML#LLM#TTRL#Reasoning#KiminaProver

Hashtags

#ai#ml#llm#ttrl#reasoning#kiminaprover