szombat, szeptember 13, 2025

a porba rajzolt háromszögek új élete


Két érdekes hír a mesterséges intelligencia világából.

Komolyan nekifogtak újra a matematika formalizálásának és tételbizonyításának a most menő módszerekkel, ennek egyik eredménye az volt, hogy a világ matematikai olimpián egy formális bizonyítást beadó rendszer is aranyérmes lett (két másik mellett ami természetes nyelven írta a megoldást, amit viszont embernek kell ellenőrizni, hogy helyes-e). A legújabb eredmény, meg, hogy egy komolyabb tétel bizonyítását, amin két neves matematikus dolgozott másfél évet (gondolom azért nem gőzerővel) es amit feladtak, egy új rendszer 3 hét alatt befejezett (persze emberi segítséggel, ha jól értem, konkrétan leírták a bizonyítást neki "formálisabb" nyelven és ő azt átültette Lean-be). Ezek persze még kezdeti eredmények, de szerintem igen fontosak, ezek már tényleg mérföldkövek az emberi szintű mesterséges intelligencia felé.

Szóval azért kell ez az irány is, mert azt hiszem, az utóbbi időben nagyon elszaladt a ló a deep learning irányába, azaz az ilyen absztrakt vektor reprezentáció felé, de szerintem a szimbolikus reprezentációnak is helye van, előbb-utóbb a mesterséges intelligenciában is foglalkozni kell a fogalmak hullám-részecske dualitásával. Szóval bizonyos feladatokat a vektoriális reprezentációval lehet jól megoldani, de mostanra már kezd elég egyértelművé válni, hogy vannak feladatok amelyekre meg nem igazán megfelelő (persze lehet, hogy valaki dob valami nagyot, nagyon sokan dolgoznak rajta). Szerintem a jó kis formális módszereknek ezekben az esetekben azért még lehet szerepe.

Aztán meg ezen az úton végre nekifoghatunk egyszerűbb doméniumok formalizálásának is, mint mondjuk a "józan paraszti észnek". Meg aztán, azt hiszem, az egyik dolog ami visszafogja még mindig a világot, az a jó és mindenki számára hozzáférhető matematika feladat megoldás.

Valamikor ezek a rendszerek nélkülözhetetlenek lesznek abban, hogy bizonyítani tudjuk bizonyos modellek tulajdonságait és rájuk merjük bízni egy ország vezetését.

A másik hír, hogy Albániában a közbeszerzési minisztériumát AI fogja vezetni. Szerintem a kis országok ahol még lehet igazi változásokat békés úton is eszközölni lesznek a legkorábbi (és talán legnagyobb) haszonélvezői a digitális átállásnak, nagyon remélem, hogy beválik nekik ez a lépés.

Demó.

Zene

Bohemian Rhapsody flashmob.

József Attila versek

 

Nincsenek megjegyzések: