1. Algebarska semantika za logike interpretabilnosti
Teo Šestak, 13. listopada 2025.
Sažetak
Logika interpretabilnosti IL proširuje logiku dokazivosti GL. Osnovna semantika za IL je Veltmanova semantika. Poznato je da je logika IL potpuna u odnosu na Veltmanovu semantiku, ali isto se ne može reći za njezina proširenja, od kojih su neka dokazano nepotpuna.
U ovom izlaganju definirat ćemo novu klasu Booleovih algebri koje se mogu koristiti za modeliranje logika interpretabilnosti. Ove algebre na prirodan način proširuju modalne algebre i mogu se smatrati generalizacijama Veltmanovih okvira. Dodatno, svako konzistentno proširenje IL adekvatno je i potpuno obzirom na ovu semantiku.
2. Aritmetizacija analize
Zvonimir Šikić, 20. listopada 2025.
Sažetak
Danas su u analizi preostali samo prirodni brojevi ili sustavi prirodnih brojeva… Matematika je aritmetizirana. (Poincaré, 1900.)
U potrazi za sigurnim temeljem matematike, matematičari su se okrenuli prirodnim brojevima. Iz njih i njihovih skupova izgradili su realne i kompleksne brojeve, funkcije i geometrijske objekte. Pitanja o njima preveli su u pitanja o ℕ i 𝒫(ℕ). To je projekt aritmetizacije koji je Kronecker odbacio kao „mistiku.“
Hilbert je predložio program aksiomatskog opravdanja te „mistike“ tako da se analiza razvije u okviru aksiomatskog sustava realnih brojeva te da se konzistentnost tog sustava dokaže konstruktivnim metodama koje bi Kronecker prihvatio (to je bio Hilbertov drugi problem).
Gödel je 1931. dokazao da je tako formulirano pitanje konzistentnosti formalnog aksiomatskog sustava analize ekvivalentno odgovarajućem pitanju u formalnom aksiomatskom sustavu aritmetike, npr. PA, ali je također dokazao da se na to pitanje u PA ne može odgovoriti (ni konzistentnost samog sustava PA nije dokaziva u PA).
Zato nije pretjerano reći da su moderna logika i izračunljivost proizašle iz zabrinutosti matematičara 19. stoljeća za temelje analize.
Drugi su matematičari, paralelno, slijedili Kroneckera u izgradnji analize konstruktivnim metodama. Jedan od slavnijih bio je Herman Weyl koji je 1918. izgradio analizu u sustavu s aksiomom aritmetičke komprehenzije. Danas bismo rekli u sustavu ACA₀. Taj je sustav dovoljno jak da dokaže sve temeljne teoreme analize. On je i PA konzervativan pa ga to kvalificira kao istinsku aritmetizaciju analize.
No nije da aritmetička komprehenzija samo dokazuje ove teoreme. Ona je zapravo ekvivalentno nekima od njih i te se ekvivalencije mogu dokazati u RCA₀ (sustavu izračunljive analize). Time se bavi reverse mathematics u kojoj su se iskristalizirali sustavi RCA₀, WKL₀, ACA₀, ATR₀ i Π₁¹CA₀. Oni su poznati kao “velika petorka” i generiraju gotovo sve teoreme standardne matematike.
Teoremi najjačih sustava ATR₀ i Π₁¹CA₀ imaju ,,skupovni štih” (kakav npr. ima Cantor-Bendixsonov teorem koji tvrdi da je neprebrojiv zatvoreni skup uvijek unija prebrojivog i savršenog skupa). Takvi teoremi su na marginama “uobičajene” analize pa bi analitičari mogli biti zadovoljni teorijama RCA₀ ⊂ WKL₀ ⊂ ACA₀. Ipak, neki važni dijelovi kombinatorike premašuju ACA₀.
3. Math Online Judge: web platforma za rješavanje matematičkih zadataka u formalnim jezicima
Ivica Kičić, 24. studenoga 2025.
Sažetak
U posljednjih desetak godina formalna verifikacija, potpomognuta sustavima poput Lean-a i Rocq-a, sve se češće koristi u matematičkom istraživanju — od provjere dokaza do automatiziranog dokazivanja teorema. Iako ti sustavi imaju znatan potencijal, njihovo je usvajanje otežano tehničkom složenošću i nedostatkom pristupačnih okruženja koja bi olakšala prve korake u radu s takvim alatima.
Usporedno s time, u informatičkom obrazovanju široko su prihvaćene tzv. „Online Judge“ platforme — web sustavi koji nude opsežne zbirke zadataka i omogućuju automatsku provjeru ispravnosti rješenja. Njihov natjecateljski karakter i neposredna povratna informacija pokazali su se vrlo učinkovitim u poticanju učenja programiranja.
Ovaj seminar predstavlja ideju i rani prototip takve platforme, prilagođene rješavanju matematičkih zadataka u formalnim jezicima. Sustav bi omogućio automatsku evaluaciju rješenja te strukturirano napredovanje kroz razine složenosti, stvarajući time okruženje koje potiče učenje i eksperimentiranje s formalnim metodama.
Cilj seminara je otvoriti raspravu o tome u kojoj bi mjeri ovakav sustav mogao doprinijeti edukaciji o formalnim jezicima te koliko bi mogao pomoći u popularizaciji formalne verifikacije i njenog uvođenja u širu matematičku praksu.
4. Prikaz teksta buduće monografije “Logika i vjerojatnost”
Zvonimir Šikić, 15. prosinca 2025.
Sažetak
Prikazujemo tekst buduće knjige Logika i vjerojatnost (403. str. plus reference).
Logika uključuje standardnu propozicijsku i predikatsku logiku, ali i Aristotelovu silogistiku i njeno Vennovo poopćenje (iz povijesnih razloga). Također je nestandardno uključena i bulovska logika (čiju odlučivost dokazujemo Herbrandovom metodom) te njoj ekvivalentna monadska logika.
Glavno sredstvo kojim analiziramo predikatsku (poliadsku) logiku su Bethova semantička stabla za koja trivijalno dokazujemo da su pozitivni test za implikaciju (što je zapravo dokaz potpunosti i kompaktnosti te logike i ekvivalentnosti njenih aksiomatskih, prirodnih i sekventnih formulacija). Trivijalno slijedi postojanje nestandardnih modela aritmetike 1. reda (dokazujemo i kategoričnost aritmetike 2. reda) kao i Skolemov „paradoks“ koji diskutiramo u svezi s redukcijom matematike na teoriju skupova. Nestandardno je i poglavlje posvećeno definicijama.
Obrađujemo i modalnu logiku (standardne sustave K, T, S4 i S5, deontičke sustave D i D+ te sustav aritmetičke dokazivosti GL) kako sintaktički tako i semantički (pomoću Kripkeovih okvira i modela). Bavimo se i modalnom kvantifikacijom. Kao nestandardni dodatak nudimo Gödelov ontološki dokaz i njegovu kritiku.
Gödel/Tarski/Rosser teoreme o nepotpunost obrađujemo (također nestandardno) na tri razine. Prva koja je svakom lako pratljiva odnosi se na („lingvističke“) teorije koje govore o vlastitom jeziku. Druga se odnosi na aritmetičke teorije općenito i nešto je apstraktnija, ali jasno pokazuje zašto je aritmetika nepotpuna. Treća se odnosi na aritmetiku 1. reda i tehnički je najzahtjevnija zbog raznih (zapravo nebitnih) ograničenja aritmetike 1. reda.
Obrađujemo i teoriju izračunljivosti (preko Smullyanovih formalnih sustave i Smullyan-izbrojivosti) te u tom kontekstu dokazujemo pojačane verzije teorema o nepotpunosti.
Na kraju logičkog dijela dokazujemo teorem o nedokazivosti konzistentnosti i diskutiramo njegove popularne primjene na pitanje „je li čovjek stroj“. Dokazujemo da bismo, što se Gödelovih teorema tiče, mogli biti strojevi. Ali ako jesmo onda nismo sposobni za potpunu spoznaju tih strojeva, odnosno za potpunu spoznaju samih sebe.
Vjerojatnost počinjemo standardni prikazom klasične vjerojatnosti s mnogo nestandardnih primjera. (Bacio sam 5 kuna i 1 kunu. Ne vidite rezultat ali vas istinito informiram da je 5 kuna dalo glavu. Kolika je vjerojatnost da je 1 kuna dala glavu? Nije nužno 1/2!) Tu se bavimo i problemom determinizma. (Bacanje kovanice je deterministički pokus, jer za zadani v i ω ishod možemo izračunati i eksperimentalno potvrditi. Zašto je onda bacanja kovanice slučajni pokus?)
Slijedi prikaz frekvencijskog pristupa vjerojatnosti (vjerojatnost = granična frekvencija) i mnogih problema koji potkopavaju taj pristup. Posebno se bavimo Bernoullijevim pogrešnim izvodom vjerojatnosti iz frekvencija (njegov tzv. zlatni teorem).
Prikazujemo i najstariji pristup vjerojatnosti kao plauzibilnosti s obzirom na raspoložive informacije. To je najopćenitiji i najprimjenljiviji pojam vjerojatnosti, koji su frekvencionisti odbacili „jer nije jasno zašto bi taj pojam zadovoljavao standardne aksiome vjerojatnosti.“ No, Cox je dokazao da ih plauzibilnost zadovoljava i taj prigovor ne stoji već skoro sto godina.
Konačno se vraćamo logici pokazujući da je vjerojatnost proširena logika. Definiramo probabilističke modele kao proširenja logičkih (verističkih) modela i u odnosu na njih definiramo probabilističku implikaciju (npr. probabilistički modus ponens izgleda ovako: 𝑃𝑟(𝐴)=𝑝 & 𝑃𝑟(𝐵|𝐴)=𝑞 ⟹ 𝑃𝑟(𝐵)∈[𝑝𝑞,1−𝑝𝑞]). To je zapravo bila Booleova logika.
Dokazujemo da u logičkom kontekstu zakon velikih brojeva zapravo ne zahtijeva neprebrojiv vjerojatnosni prostor (na kojem je relevantni skup nizova zanemariv).
Sljedeća dva poglavlja bave se pitanjem što je slučajnost. Na izgled različiti odgovori koji se pozivaju na nepredvidivost (Mises, Ville, Kolmogorov), tipičnost (Martin-Löf) i nekompresibilnost (Kolmogorov, Chaitin) daju ekvivalentne rezultate. To Martin-Löf Chaitinovu tezu da oni dobro definiraju slučajnost čini plauzibilnom.
U kontekstu nekompresibilnosti dokazujemo i Gödel-Chaitinov teorem o nepotpunosti (postoji 𝑚 takav da se ni za jedan konačni niz 𝑠 ne može formalno dokazati da on ima složenost veću od 𝑚).
Zadnje poglavlje bavi se odnosom vjerojatnosti, (znanstvene) indukcije i kauzalnosti. Pokazujemo da nema probabilističke metode koja uzroke može odrediti iz podataka. Zato podatke moramo tumačiti i na temelju neformalnih uzročno-posljedičnih pretpostavki (tj. treba li ili ne treba kontrolirati neku varijablu ne možemo riješiti bez kauzalnih pretpostavki). No, postoje i formalne metode koje to rješavaju algoritamski i koje su u zadnjih 30-tak godina, dovele do prave „𝑘𝑎𝑢𝑧𝑎𝑙𝑛𝑒 𝑟𝑒𝑣𝑜𝑙𝑢𝑐𝑖𝑗𝑒“. Prikazujemo i njihovu osnovnu ideju.
5. Prikaz teksta buduće monografije “Logika i vjerojatnost” (2)
Zvonimir Šikić, 22. prosinca 2025.
Sažetak
Nastavak prikaza teksta buduće knjige Logika i vjerojatnost (403. str. plus reference).
Vjerojatnost počinjemo standardni prikazom klasične vjerojatnosti s mnogo nestandardnih primjera. (Bacio sam 5 kuna i 1 kunu. Ne vidite rezultat ali vas istinito informiram da je 5 kuna dalo glavu. Kolika je vjerojatnost da je 1 kuna dala glavu? Nije nužno 1/2!) Tu se bavimo i problemom determinizma. (Bacanje kovanice je deterministički pokus, jer za zadani v i ω ishod možemo izračunati i eksperimentalno potvrditi. Zašto je onda bacanja kovanice slučajni pokus?)
Slijedi prikaz frekvencijskog pristupa vjerojatnosti (vjerojatnost = granična frekvencija) i mnogih problema koji potkopavaju taj pristup. Posebno se bavimo Bernoullijevim pogrešnim izvodom vjerojatnosti iz frekvencija (njegov tzv. zlatni teorem).
Prikazujemo i najstariji pristup vjerojatnosti kao plauzibilnosti s obzirom na raspoložive informacije. To je najopćenitiji i najprimjenljiviji pojam vjerojatnosti, koji su frekvencionisti odbacili „jer nije jasno zašto bi taj pojam zadovoljavao standardne aksiome vjerojatnosti.“ No, Cox je dokazao da ih plauzibilnost zadovoljava i taj prigovor ne stoji već skoro sto godina.
Konačno se vraćamo logici pokazujući da je vjerojatnost proširena logika. Definiramo probabilističke modele kao proširenja logičkih (verističkih) modela i u odnosu na njih definiramo probabilističku implikaciju (npr. probabilistički modus ponens izgleda ovako: 𝑃𝑟(𝐴)=𝑝 & 𝑃𝑟(𝐵|𝐴)=𝑞 ⟹ 𝑃𝑟(𝐵)∈[𝑝𝑞,1−𝑝𝑞]). To je zapravo bila Booleova logika.
Dokazujemo da u logičkom kontekstu zakon velikih brojeva zapravo ne zahtijeva neprebrojiv vjerojatnosni prostor (na kojem je relevantni skup nizova zanemariv).
Sljedeća dva poglavlja bave se pitanjem što je slučajnost. Na izgled različiti odgovori koji se pozivaju na nepredvidivost (Mises, Ville, Kolmogorov), tipičnost (Martin-Löf) i nekompresibilnost (Kolmogorov, Chaitin) daju ekvivalentne rezultate. To Martin-Löf Chaitinovu tezu da oni dobro definiraju slučajnost čini plauzibilnom.
U kontekstu nekompresibilnosti dokazujemo i Gödel-Chaitinov teorem o nepotpunosti (postoji 𝑚 takav da se ni za jedan konačni niz 𝑠 ne može formalno dokazati da on ima složenost veću od 𝑚).
Zadnje poglavlje bavi se odnosom vjerojatnosti, (znanstvene) indukcije i kauzalnosti. Pokazujemo da nema probabilističke metode koja uzroke može odrediti iz podataka. Zato podatke moramo tumačiti i na temelju neformalnih uzročno-posljedičnih pretpostavki (tj. treba li ili ne treba kontrolirati neku varijablu ne možemo riješiti bez kauzalnih pretpostavki). No, postoje i formalne metode koje to rješavaju algoritamski i koje su u zadnjih 30-tak godina, dovele do prave „𝑘𝑎𝑢𝑧𝑎𝑙𝑛𝑒 𝑟𝑒𝑣𝑜𝑙𝑢𝑐𝑖𝑗𝑒“. Prikazujemo i njihovu osnovnu ideju.
6. Formalna verifikacija zaštite integriteta SEV-SNP tehnologije
Sophie Weber, 9. veljače 2026.
Sažetak
Pojam formalne verifikacije obuhvaća modeliranje nekog sustava iz stvarnog svijeta jezikom simboličke logike te verifikaciju svojstava tog modela. Uvest ćemo pojam prepisivanja multiskupa (multiset rewriting) kao metodu formalne verifikacije te alat za automatsko dokazivanje Tamarin.
Definirat ćemo pojam pouzdane okoline za izvršavanje (trusted execution environment) i opisati AMD-ovu tehnologiju SEV-SNP kao jedan primjer ovakve okoline. Ovakva okolina koristi se u kontekstu izvršavanja programa na udaljenom računalu (npr. AWS, Azure, Google Colab i sl.) kada želimo osigurati tajnost i integritet podataka koje čuvamo i obrađujemo na udaljenom računalu.
Proći ćemo kroz modele (Paradžik et al., 2025. i Weber, 2025.) koji u Tamarinu modeliraju SEV-SNP platformu te provjeravaju sigurnosna svojstva vezana za SEV-SNP. Paradžik et al. (2025.) pronalazi 4 potencijalna napada vezana uz autentičnost podataka i sigurnost SEV-SNP platforme. Weber (2025.) dokazuje sva očekivana svojstva vezana za integritet memorije na platformi.
7. Memorijski učinkovito treniranje velikih modela: LORA
Goran Ivanković, 16. veljače 2026.
Sažetak
U posljednje vrijeme često slušamo o napretku umjetne inteligencije koja uključuje chatbotove i generativne modele. Većinu tog napretka dugujemo velikom broju parametara modela. Za pokretanje takvih modela potrebne su skupine vrlo jakih računala, dostupnih samo velikim kompanijama. Mnoge firme, a pogotovo one koje se zalažu za open-source, okreću se treniranju manjih i efikasnijih modela koje napokon može pokrenuti krajnji korisnik uz prosječnu grafičku karticu. S nedavnim napretkom u područjima optimizacije i kvantizacije, čak i fino podešavanje modela u vlastite i specijalizirane svrhe postaje sve jednostavnije.
U ovom seminaru opisat ćemo jednu metodu koja to omogućuje – LORA (Low-Rank Adaptation). Metoda je zanimljiva zbog načina na koji smanjuje broj parametara koji se treniraju, zbog čega potrebna memorija na grafičkoj kartici ostaje unutar dohvata prosječnog korisnika.
8. Opći okviri i algebarska semantika za logike interpretabilnosti
Teo Šestak, 23. veljače 2026.
Sažetak
Logike interpretabilnosti su familija logika koje proširuju modalnu logiku dokazivosti GL. Cilj logika interpretabilnosti je formalizirati pojam relativne interpretabilnosti među aritmetičkim teorijama. Osnovna logika interpretabilnosti je sistem IL, od kojega se dodavanjem shema aksioma dobivaju razna proširenja. Standardna relacijska semantika za logike interpretabilnosti, Veltmanova semantika, nema neka svojstva koja bismo željeli. Primjerice, sistem IL je potpun, no nije jako potpun obzirom na klasu svih Veltmanovih okvira. Također, neka proširenja sistema IL su nepotpuna obzirom na klasu okvira koju definiraju.
U ovom radu, bavimo se općim okvirima i algebarskom semantikom za logike interpretabilnosti. Prvo definiramo opće okvire za logike interpretabilnosti, po uzoru na opće okvire za modalne logike. Dokazujemo, ponovno po uzoru na modalne logike, teoreme jake potpunosti za IL i za proširenja. Takvi opći okviri, kao poseban slučaj, obuhvaćaju Veltmanove okvire. Nakon toga definiramo algebarsku semantiku tako da Booleovim algebrama pridružimo operator(e), koji odgovaraju modalnim operatorima u jeziku logika interpretabilnosti. Zatim dokazujemo teorem potpunosti proširenja sistema IL obzirom na odgovarajuću klasu algebri. Konačno, pokazat ćemo kako možemo općem okviru pridružiti algebru i, obrnuto, algebri opći okvir, tako da se čuva valjanost formula.
Ovaj seminar ujedno je i javna obrana teme doktorske disertacije.
9. Lokalizirano moralno planiranje korištenjem linearne temporalne logike
Matej Mihelčić, 9. ožujka 2026.
Sažetak
Na seminaru ćemo opisati problem CONFLICT na primjeru etičkog planiranja baziranog na logici, korištenjem linearne temporalne logike. Navedeni problem je bitan u robotici jer omogućuje pronalazak etički-zadovoljivog egzaktnog plana. Generalno je problem CONFLICT PSPACE-potpun problem, međutim uz definirane pretpostavke lokalnosti na propozicije i akcije, zadano indeksiranje propozicija i uvjet da akcije ovise o ograničenom broju susjednih akcija u predefiniranom intervalu, uz konstantan broj globalnih propozicija, pokazujemo da problem možemo riješiti u polinomnom vremenu. Empirijski pokazujemo da navedeni pristup uz pretpostavke lokalnosti ima znatne primjene u robotici, te omogućuje brz i točan pronalazak etički-zadovoljivog egzaktnog plana.
Ovo je zajednički rad s Adrianom Satjom-Kurdijom.