Mistral AI prezentuje Leanstral 1.5: Model agenta kodu dla Lean 4 rozwiązujący 587 problemów PutnamBench

Mistral AI ogłosiło wydanie Leanstral 1.5, zaawansowanego modelu agenta kodu zaprojektowanego dla Lean 4. Nowa wersja ma na celu usprawnienie automatycznego dowodzenia twierdzeń oraz inżynierii dowodów, a jej wagi są dostępne na licencji Apache 2.0. Równocześnie uruchomiono darmowy punkt końcowy API o nazwie leanstral-1-5.

Architektura i możliwości Leanstral 1.5

Leanstral 1.5 stanowi aktualizację wcześniejszego modelu Leanstral-2603 i należy do rodziny Mistral Small 4. Jest to model agenta kodu stworzony dla Lean 4, asystenta dowodzenia, który mechanicznie weryfikuje każdy logiczny krok. Lean 4 potrafi wyrażać złożone obiekty, takie jak przestrzenie perfektoidalne, oraz właściwości fragmentów kodu Rust.

Architektura modelu opiera się na koncepcji mixture-of-experts (MoE), gdzie każdy token jest kierowany do kilku wyspecjalizowanych podsieci. Takie podejście pozwala na utrzymanie niskiego zapotrzebowania na moc obliczeniową przy jednoczesnym zachowaniu dużej całkowitej pojemności. Leanstral wykorzystuje 128 ekspertów, z czego 4 są aktywne na token. Całkowity rozmiar modelu to 119 miliardów parametrów, z czego 6,5 miliarda jest aktywowanych na token. Model obsługuje długość kontekstu do 256 tysięcy tokenów i przyjmuje dane wejściowe multimodalne (tekst i obraz), generując wyłącznie tekst.

Szkolenie Leanstral 1.5 odbywało się w trzech etapach: mid-training, nadzorowane dostrajanie (supervised fine-tuning) oraz uczenie wzmacniające z wykorzystaniem CISPO. Zachowanie agentowe modelu zostało ukształtowane w dwóch środowiskach uczenia wzmacniającego:

• W środowisku multiturn, model otrzymuje twierdzenie do udowodnienia lub obalenia. Przesyła dowód, analizuje informacje zwrotne od kompilatora Lean i udoskonala swoje próby, aż do sukcesu lub wyczerpania budżetu.
• W środowisku code agent, Leanstral działa w ramach systemu plików, edytując pliki, uruchamiając polecenia bash i korzystając z serwera języka Lean, który dostarcza w czasie rzeczywistym informacje o celach, błędach i typach. Pozwala to na uzupełnianie częściowych dowodów, budowanie pomocniczych lematów oraz utrzymywanie kontekstu dzięki kompresji.

Wyniki i zastosowania praktyczne

Zespół Mistral AI informuje, że Leanstral 1.5 osiąga 100% na zestawach walidacyjnych i testowych miniF2F. Model rozwiązał 587 z 672 problemów PutnamBench, ustanawiając nowy stan wiedzy w benchmarkach algebry FATE-H (87%) i FATE-X (34%). W teście FLTEval, pass@1 wzrósł z 21.9 do 28.9, a pass@8 z 31.9 do 43.2. FLTEval jest zbudowany na podstawie rzeczywistych pull requestów do repozytorium Wielkiego Twierdzenia Fermata. Leanstral przewyższa w nim Opus 4.6, osiągając lepsze wyniki przy siedmiokrotnie niższych kosztach, a także zwiększa przewagę nad modelami open-source, które są od trzech do dziesięciu razy większe.

Na PutnamBench, Leanstral wyprzedza Seed-Prover 1.5 o 7 problemów, kosztując około 4 dolary za problem, podczas gdy Seed-Prover w wysokim ustawieniu kosztuje około 300 dolarów lub więcej za problem. Model przewyższa również Aleph Prover, którego koszt wynosi około 54-68 dolarów za problem.

Kluczową cechą modelu jest skalowanie w czasie testowania. Zwiększenie budżetu tokenów na próbę podnosi wynik PutnamBench Pass@8. Zespół Mistral AI podaje, że model rozwiązał 44 problemy przy 50 tys. tokenów, 244 przy 200 tys., 493 przy 1 mln i 587 przy 4 mln.

Leanstral, choć trenowany głównie na matematyce, potrafi również weryfikować kod. Mistral AI udokumentował dwa studia przypadków istotne dla inżynierów. W 57 repozytoriach model zidentyfikował 47 naruszonych właściwości i 11 rzeczywistych błędów, z czego pięć nie było wcześniej zgłoszonych na GitHubie. Jeden z błędów dotyczył funkcji sign w dekodowaniu zigzag, gdzie przepełnienie wartości (value + 1) dla Std.U64.MAX powodowało awarie w trybie debugowania i cichą korupcję w trybie wydania.

Praktyczne zastosowania i dostępność

Praktyczne zastosowania Leanstral 1.5 obejmują możliwość ukończenia częściowych dowodów w repozytorium, automatyczne generowanie właściwości poprawności dla funkcji oraz testowanie kodu Rust poprzez dowodzenie lub obalanie wnioskowanych niezmienników. Najprostszym sposobem na skorzystanie z modelu jest Mistral Vibe, interfejs CLI agenta Mistral. Leanstral jest dostępny w ramach bezpłatnego planu Mistral. Aby go użyć, należy włączyć „Labs models” na koncie i utworzyć klucz API. Model można również hostować samodzielnie, instalując vLLM 0.24.0 lub nowszy i serwując wagi.

Wydanie Leanstral 1.5 przez Mistral AI stanowi znaczący krok naprzód w dziedzinie automatycznego dowodzenia twierdzeń i weryfikacji kodu. Jego zdolność do rozwiązywania złożonych problemów matematycznych i identyfikowania błędów w oprogramowaniu, przy jednoczesnym zachowaniu efektywności kosztowej, może mieć istotne implikacje dla rozwoju bezpiecznego i poprawnego oprogramowania oraz dla badań w dziedzinie sztucznej inteligencji i matematyki formalnej. Warto obserwować, jak te możliwości zostaną zaadaptowane w praktyce przez społeczność deweloperów i naukowców.

Źródło: marktechpost.com