Mistral AI wydała Leanstral 1.5, nowy otwarty model do automatycznego dowodzenia twierdzeń matematycznych w języku Lean 4. Model osiąga wynik 587 z 672 problemów na benchmarku PutnamBench i jest dostępny jako darmowy endpoint API pod nazwą leanstral-1-5, z wagami publikowanymi na licencji Apache 2.0.
Leanstral 1.5 należy do rodziny Mistral Small 4 i wykorzystuje architekturę mixture-of-experts (MoE) z 128 ekspertami, z których 4 są aktywne na token. Model ma całkowicie 119 miliardów parametrów, ale zaledwie 6,5 miliarda jest aktywowanych na raz, co pozwala na efektywne wykorzystanie mocy obliczeniowej. Kontekst sięga 256 tysięcy tokenów, a model akceptuje wejście multimodalne - tekst i obrazy.
Trening przebiegał w trzech etapach: wstępnym treningu, supervised fine-tuningu oraz reinforcement learningu z algorytmem CISPO. Innowacyjne podejście to dwuśrodowiskowe uczenie agentowe: w środowisku multi-turn model otrzymuje stwierdzenie twierdzenia i musi je udowodnić, iteracyjnie poprawiając dowód na podstawie feedbacku kompilatora Lean, aż do sukcesu lub wyczerpania budżetu kroków. Leanstral 1.5 stanowi istotny krok w automatyzacji dowodzenia twierdzeń, tradycyjnie wymagającego ludzkiej intuicji i doświadczenia matematycznego.