Leanstral 1.5: Революция в формальной верификации кода и математики
Leanstral 1.5: Proof abundance for all
Мы представляем Leanstral 1.5, бесплатную модель с лицензией Apache-2.0, которая демонстрирует рекордные результаты на PutnamBench и FATE-H. Благодаря обучению с подкреплением, она не только решает сложные математические задачи, но и находит скрытые баги в реальных репозиториях, делая формальную верификацию доступной и эффективной.
Формальная верификация может быть не только эффективной, но и практичной для реального использования, обнаруживая ошибки, которые традиционные методы часто пропускают.
- InsideOutSanta
Многие критикуют Mistral за неспособность конкурировать с крупными моделями, и это справедливо. Но я думаю, что это игнорирует то, что Mistral на самом деле делает: они делают конкретные возможности доступными в малых моделях высокого качества.
Я часто занимаюсь OCR, анализом файлов и подобными задачами. Для этого я использую Mistral. Я закинул 100$ на свой аккаунт, и этого хватило на целый год без каких-либо опасений по поводу количества запросов, потому что стоимость ничтожна. Это ценно, даже если это не конкурирует с Opus 4.8.
- boulos
Это отличная работа, но пример с поиском бага мне показался странным:
> Один из таких багов был в функции sign для zizag-декодирования библиотеки datrs/varinteger. При вводе Std.U64.MAX выражение (value + 1) переполнялось, вызывая краши в режиме отладки и тихую порчу данных в релизном режиме — это пограничный случай, который тестирование и фаззинг обычно пропускают.
В каком смысле этот пограничный случай можно считать тем, что «тестирование [...] обычно пропускает»? Конечно, плохие тесты его пропустят или даже не подумают о нем, но я считаю, что (а) внимательные люди и (б) ML-системы для написания кода на самом деле очень хорошо справляются с мыслью «ой, мне нужно протестировать экстремальные значения». Особенно для вещей, которые парсят пользовательский ввод.
Мне интересно, нашли ли они другие баги, которые были более интересными, но их было слишком сложно быстро объяснить.
- andai
Половина статьи посвящена сравнению с несколькими передовыми LLM. Но все они вышли полгода назад. «Наша новая модель лучше, чем все эти китайские модели трех поколений назад» — это мне кажется довольно смешным.
- Groxx
> Один из таких багов был в функции sign для zizag-декодирования библиотеки datrs/varinteger. При вводе Std.U64.MAX выражение (value + 1) переполнялось, вызывая краши в режиме отладки и тихую порчу данных в релизном режиме — это пограничный случай, который тестирование и фаззинг обычно пропускают.
Эта библиотека: https://github.com/datrs/varinteger
Кажется, это вполне верно, так как идентичная проблема была создана в этом репозитории за неделю до публикации этой новости: https://github.com/datrs/varinteger/issues/8 (это сотрудник Leanstral? У них почти нет информации и очень редкая активность. Или, может быть, Leanstral просто подхватил эту проблему?)
Это крошечная, удивительно плохо протестированная, давно не тронутая (8 лет) библиотека: https://github.com/datrs/varinteger/blob/master/tests/test.r... у которой около 1000 загрузок в день: https://crates.io/crates/varinteger [1], что кажется довольно низким показателем.
Честно говоря, я бы не стал считать это таким ошеломляющим успехом, чтобы приводить его в качестве единственного примера. Хотя автоматическое обнаружение, безусловно, полезно. Или это значимое достижение для этой узкой области? Я не играл с LLM для написания доказательств, но учитывая нехватку обучающих данных, я не был бы удивлен, если бы они были немного сырыми по сравнению с общим программированием.
1: https://crates.io/crates/varinteger указывает на https://github.com/mafintosh/varinteger-rs, который перенаправляет на https://github.com/datrs/varinteger, так что, несмотря на то, что на первый взгляд они выглядят по-разному, похоже, это одна и та же библиотека.
- bjt12345
Мне кажется немного абсурдным критиковать Mistral, из всех компаний, за отставание от Frontier-моделей.
Во-первых, кто не отстал? Grok... Meta....? Многие крупные компании борются.
Во-вторых, Mistral пытается решить другую проблему.
В-третьих, Mistral следует поздравить за то, что они так долго остаются в гонке.