Leanstral: фонд с открытым исходным кодом для надежного кодирования вибрации

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

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

Представляем Леанстрал

Мы выпускаем Leanstral, первый агент с открытым исходным кодом, разработанный для Lean 4. Lean4 — это помощник по доказательству, способный выражать сложные математические объекты, такие как перфектоидные пространства и характеристики программного обеспечения, такие как свойства фрагментов Rust. В отличие от существующих систем проверки, которые действуют как оболочки для больших универсальных моделей или фокусируются на отдельных математических задачах, Leanstral спроектирован так, чтобы быть высокоэффективным (с активными параметрами 6B) и обученным для работы в реалистичных формальных хранилищах.

• Открыто и доступно: мы выпускаем весы Leanstral под лицензией Apache 2.0, в режиме агента в Mistral Vibe и через бесплатную конечную точку API. Мы также выпустим технический отчет с подробным описанием нашего подхода к обучению и новый пакет оценки FLTEval, чтобы вывести оценки за рамки математики соревнований.

• Эффективность и мощь: мы используем очень разреженную архитектуру для Leanstral и оптимизируем ее для задач проверочного проектирования. Используя параллельный вывод с Lean в качестве идеального средства проверки, Leanstral является одновременно производительным и экономически эффективным по сравнению с существующими конкурентами с закрытым исходным кодом.

• Возможность обновления через MCP: Leanstral поддерживает произвольные MCP через Vibe и был специально обучен для достижения максимальной производительности с часто используемым Lean-lsp-mcp.

Оценка

Чтобы отразить полезность в реалистичных сценариях разработки доказательств, мы оцениваем Leanstral на предмет выполнения всех формальных доказательств и правильного определения новых математических концепций в каждом запросе на проект FLT, а не на отдельные математические проблемы. Мы сравниваем Leanstral с ведущими агентами кодирования (Claude Opus 4.6, Sonnet 4.6, Haiku 4.5) и моделями с открытым исходным кодом (Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B).

Модели Leanstral и OSS

Leanstral-120B-A6B демонстрирует значительное преимущество в эффективности по сравнению со своими гораздо более крупными аналогами с открытым исходным кодом. В то время как такие модели, как GLM5-744B-A40B и Kimi-K2.5-1T-32B, с трудом масштабируются, их баллы FLTEval достигают примерно 16,6 и 20,1 соответственно, Leanstral превосходит их обоих всего за один проход.

Даже Qwen3.5-397B-A17B, сильнейшему показанному участнику OSS, требуется 4 прохода, чтобы набрать 25,4 балла. Напротив, Leanstral достигает более высокого балла 26,3 при вдвое меньших инвестициях (pass@2) и продолжает линейно масштабироваться, достигая 29,3 при том же уровне затрат.

Леанстрал против семьи Клода

Leanstral служит ценной альтернативой пакету Claude, предлагая конкурентоспособную производительность за небольшую часть цены: Leanstral pass@2 достигает 26,3 балла, опередив Sonnet на 2,6 балла, при этом стоимость эксплуатации составляет всего 36 долларов США по сравнению с 549 долларами Sonnet. На pass@16 Leanstral набирает 31,9 балла, уверенно опережая Sonnet на 8 очков. Хотя Claude Opus 4.6 остается лидером по качеству, его стоимость составляет 1650 долларов США, что в 92 раза выше, чем стоимость Leanstral.

В нашем сравнительном тестировании мы использовали Mistral Vibe в качестве основы без каких-либо модификаций специально для оценки.

Тематические исследования

Отвечаем на сообщения stackexchange об изменениях в последней версии Lean

Когда критические изменения попадают в новую версию Lean, миграция кода может стать огромной головной болью. Мы кормили Леанстралом реальный вопрос из обмена стеками Proof Assistants о скрипте, который загадочным образом перестал компилироваться в Lean 4.29.0-rc6 (с которым мы не обучались ввиду его новизны). Виной всему была перепрошивка(rw) тактика, которая внезапно не смогла сопоставить шаблоны, включающие простой псевдоним типа, первоначально записанный как def T2 := List Bool.

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

Предложенное исправление было простым: просто поменяйте местами def для abbrev. Потому что abbrev создает прозрачный псевдоним, который сразу же по определению равен исходному типу, rw тактика снова могла бы идеально соответствовать шаблону (L2 n).length в доказательстве. Leanstral выполняет работу и прекрасно объясняет пользователю ее суть.

Рассуждения о программах

Мы скопировали определения в Rocq из https://www.cs.princeton.edu/courses/archive/fall10/cos441/sf/Imp.html и попросил Leanstral перейти на Lean. Это удалось сделать успешно, даже внедрив собственную систему обозначений. Пример фрагмента:

inductive ceval : com → state → state → Prop where
 | E_Skip (st : state) : ceval .CSkip st st
 | E_Ass (st : state) (a1 : aexp) (n : Nat) (l : ident) (h : aeval a1 st = n) :
     ceval (.CAss l a1) st (update st l n)
 | E_Seq (c1 c2 : com) (st st' st'' : state) (h1 : ceval c1 st st') (h2 : ceval c2 st' st'') :
     ceval (.CSeq c1 c2) st st''
 | E_IfTrue (st st' : state) (b1 : bexp) (c1 c2 : com) (h : beval b1 st = true) (h1 : ceval c1 st st') :
     ceval (.CIf b1 c1 c2) st st'
 | E_IfFalse (st st' : state) (b1 : bexp) (c1 c2 : com) (h : beval b1 st = false) (h1 : ceval c2 st st') :
     ceval (.CIf b1 c1 c2) st st'
 | E_WhileEnd (b1 : bexp) (st : state) (c1 : com) (h : beval b1 st = false) :
     ceval (.CWhile b1 c1) st st
 | E_WhileLoop (st st' st'' : state) (b1 : bexp) (c1 : com) (h1 : beval b1 st = true) (h2 : ceval c1 st st') (h3 : ceval (.CWhile b1 c1) st' st'') :
     ceval (.CWhile b1 c1) st st''


-- Notation for command evaluation
notation:50 c " / " st " ⇒ " st' => ceval c st st'

Его также можно перевести на Lean, а затем доказать некоторые свойства программ на этом языке, просто воспользовавшись утверждением Рока (без доказательства):

-- Example command: adds 2 to variable X
def plus2 : com := .CAss "X" (.APlus (.AId "X") (.ANum 2))


-- Theorem: The plus2 command correctly adds 2 to variable X
-- Intuition: If X has value n in the initial state, after executing plus2,
-- X will have value n+2 in the final state
-- This specifies the behavior of the plus2 command
theorem plus2_spec (st : state) (n : Nat) (st' : state) (h1 : st "X" = n) (h2 : plus2 / st ⇒ st') :
 st' "X" = n + 2 := by
 -- plus2 is defined as .CAss "X" (.APlus (.AId "X") (.ANum 2))
 -- Use equation compiler to unfold it
 change ceval (.CAss "X" (.APlus (.AId "X") (.ANum 2))) st st' at h2
 cases h2 with
 | E_Ass _ _ n l h =>
   have : aeval (.APlus (.AId "X") (.ANum 2)) st = n := h
   simp only [aeval] at this
   rw [update]
   simp [← this, h1]

Требуйте доказательств. Попробуйте Леанстрал сегодня.

Леанстрал сегодня доступен каждому.

• Нулевая настройка в Мистраль Вайб: Мы интегрировали Leanstral непосредственно в Mistral Vibe для немедленного кодирования и проверки вибрации без каких-либо настроек. Использовать /leanstall начать.

• API Labs: доступ к модели через нашу бесплатную/почти бесплатную конечную точку API. labs-leanstral-2603. Мы сохраняем эту конечную точку доступной в течение ограниченного периода времени, чтобы собирать реалистичные данные обратной связи и наблюдаемости, чтобы стимулировать следующее поколение проверенных моделей кода.

• Владейте весами: загрузите лицензионную модель Apache 2.0 и запустите ее на своем компьютере.

Документация – Зарегистрируйтесь в Mistral Vibe