Z przyjemnością informujemy, że jeden z naszych pracowników naukowych, mgr inż. Łukasz Janiec z Katedry Cybernetyki i Robotyki został laureatem w konkursie Dell Technologies "AI na Twoim biurku. To proste!".

Konkurs cieszył się dużym zainteresowaniem. 
Grono ekspertów w osobach: prof. Włodzisław Duch (Uniwersytet Mikołaja Kopernika), dr Maciej Kawecki (znany popularyzator nauki i polskich naukowców w kraju i za granicą, This is The World oraz This is IT) oraz Sebastian Kondracki (jeden z twórców Bielik AI) wybrało 15 projektów z ponad 600 zgłoszeń do nagrodzenia nowoczesną lokalną stacją AI Dell Pro Max z GB10. 

Finaliści uzyskali możliwość spotkania w siedzibie Dell Technologies w Łodzi z ekspertami i dyrektorem polskiego oddziału Dell Dariuszem Piotrkowskim. W programie przewidziano także wizyty i warsztaty w fabryce na miejscu.
Każdy z uczestników miał okazję zaprezentować i skonsultować swoje projekty i plany użycia stacji.

Projekt autorstwa Pana Łukasza Jańca zakłada wykorzystanie możliwości tej stacji w ramach przedsięwzięcia „Trustworthy Robotics by Design: Automatyzacja formalnej weryfikacji algorytmów robotyki z użyciem LLM i Lean 4”, powiązanego z tematyką  jego badań  i pracą nad  rozprawą doktorską.

- W ramach tego projektu zamierzam wykorzystać lokalne modele LLM do wspomagania automatycznej weryfikacji formalnej algorytmów robotyki oraz leżącej u ich podstaw matematyki przy użyciu Lean 4, czyli języka programowania i asystenta dowodowego, w którym można formalizować i sprawdzać dowody matematyczne. Prace będą opierać się na narzędziach takich jak LeanDojo, LeanProgress oraz nowatorskim podejściu zwanym „Formal-Verification-in-the-Loop” w nadrzędnej warstwie systemu sterowania - mówi o swoich planach mgr inż. Łukasz Janiec - Tego rodzaju prace są szczególnie ważne w przypadku systemów robotyki o krytycznym znaczeniu dla bezpieczeństwa: robotów chirurgicznych, systemów cyber-fizycznych działających w czasie rzeczywistym, takich jak drony obronne, oraz systemów w fabrykach z wieloma robotami, gdzie nawet krótkie zakleszczenia mogą spowodować milionowe straty produkcyjne.

Naukowiec, zainspirowany znakomitym wykładem „Mathematical discovery in the age of AI” autorstwa dra Bartosza Naskręckiego, ma nadzieję przyczynić się do  budowy solidnych i zweryfikowanych matematycznych oraz algorytmicznych fundamentów dla robotyki, które będą wspierać godne zaufania systemy sztucznej inteligencji.

Mgr inż. Łukasz Janiec zajmuje się zagadnieniami koordynacji i automatyczną syntezą formalnie poprawnego sterowania w systemach wielu robotów. Ważną częścią jego badań jest analiza i unikanie zakleszczeń w systemach zdarzeniowych typu RAS, predykcja konforemna dla zapewnienia odporności działania w warunkach niepewności i formalna weryfikacja poprawności sterowania (Lean4 + LLM)