A rendszertervezést az ellentmondásos specifikációk nagyban megnehezíthetik, és jelentős költségekkel járhat, ha a hibákra csak a fejlesztés késői fázisában derül fény. Gyakori kihívás, hogy a követelmények csak informális vagy félformális szöveges formában állnak rendelkezésre, így az ellenőrzésük hosszadalmas és fárasztó kézi átvizsgálást igényel. A nagy nyelvmodellek (LLM) a nagy mennyiségű szöveg automatikus feldolgozására jelenthetnek megoldás, ám a korlátozott (bár napjainkban egyre növekvő) érvelési képességük a "hallucinációk" (hihető, ám hibás kimenetek) miatt az ellentmondások feltárására csak részben alkalmasak.

A feladat az úgynevezett neuro-szimbolikus következtetést vizsgálja, mely az LLM-et formális módszerekkel kombinálja. Az LLM a szöveg értelmezését és a "kreatív" munkát végzi, míg kimenetének (pl. a követelmények alapján felépített tudásgráf vagy kezdeti rendszermodell) helyességét formális módszerek segítségével ellenőrizzük. Lehetséges a másik irányú együttműködés is, ahol a formális módszer kiementét az LLM segítségével tesszük a mérnökök számára könnyebben érthetővé.

A feladat felhasználja a tanszéken fejlesztett Refinery gráfalapú formális logikai következtető keretrendszert (online demó: https://refinery.services). A témán dolgozó hallgatók olyan nemzetközi élvonalba tartozó gráfalapú formális logikai következtető algoritmus fejlesztéséhez csatlakozhatnak, amely skálázódás tekintetében vetekszik az MIT vagy a Microsoft Research kutatói által kidolgozott SMT vagy SAT megoldókra alapuló módszerekkel.

A feladatra akár több hallgató is jelentkezhet, a pontos részfeladatok és kiírás meghatározására a konzulenssel egyeztetve kerül sor.