Вышла новая модель Leanstral 1.5
Заявлена новая открытая (Apache 2.0) модель Leanstral 1.5 (https://huggingface.co/mistralai/Leanstral-1.5-119B-A6B) с 119B всего и 6B активных параметров.
На практике верификация свойств кода позволила доказать временную сложность AVL-деревьев. Кроме того, автоматическое нахождение ошибок выявило 5 ранее неизвестных багов в открытых репозиториях.
Сначала было промежуточное обучение, затем SFT и RL с CISPO в двух средах, где многошагово доказывались теоремы и выполнялась агентская работа с файловой системой и Lean LSP.
В результате полностью пройден miniF2F (100%), решено 587 из 672 на PutnamBench, получен статус нового SOTA с 87% на FATE‑H и 34% на FATE‑X, а цена около $4 за задачу в разы дешевле аналогов.
