Víme, jestli je Navier-Stokes správně?

22.9. 22:57 | Přečteno: 1603× | matematika | | poslední úprava: 30.9. 19:31

Před dvěma týdny světem otřásla zpráva, že OpenAI vyřešila problém Milénia. Doprovodila jej důkazem v Leanu. Coby někdo, kdo se v oblasti formální matematiky & AI pohybuje, bych rád vysvětlil, jak jsme sebevědomí, že je výsledek matematicky správně, a co by se ještě mohlo zvrtnout.

Řeč je o tomhle repositáři, které obsahuje důkaz v Leanu. Dřív bychom museli čekat roky, až se důkazem prokousají experti z oboru, a teď by to měl program ověřit za nás? Mezi laiky jsem zaregistroval zhruba takovéhle dvě reakce:

• Je to v Leanu, tak to musí být správně.
• No a co? Proč bych měl věřit nějakému obřímu AI-slopu? Určitě tam bude nějaký bug.

A ani jedna není moc přesná, tak si pojďme vysvětlit, proč si jsou lidi už celkem jistí matematickou správností, a v čem by se doopravdy mohl skrývat zádrhel:

• Softwarový bug v kernelu Leanu / toolingu.
• Bug ve formální formulaci oné věty -- dokázalo se něco jiného, než se chtělo.
• Chyba ve filozofických základech matematiky.

Tak si je pojďme po jednom projít.

Softwarový bug v Leanu.

Lean je poměrně komplexní software, ale jako správný logický systém odděluje svoje jádro, od automatizace, a uživatelského rozhraní. Jádro je zodpovědné za to, že každý krok následuje pravidla teorie závislých typů, na které Lean stojí. Při běžném použítí Leanu s ním uživatel moc neinteraguje, a běží pouze na pozadí jako sanity-check.

Pokud ale chceme ověřit cizí (a možná škodlivý) důkaz, je situace jiná. Ještě před pár lety na takovou situaci nebyl Lean připravený, teď je. Oficiální nástroj se jmenuje Comparator. Comparator spustí veškerý kód, který není ryzí jádro uvnitř sandboxu, a exportuje pouze low-level kroky v logice. Ty pak ověří samotným kernelem (nebo více kernely). Celé se to jmenuje "comparator" proto, že srovnává dva kódy napsané v Leanu -- důkaz (ke kterému jsme co nejvíc nedůvěřiví), a specifikaci -- větu, kterou chceme dokázat, a stojí stranou od všeho toho dokazování.

Bug v Comparatoru mi přijde dost nepravděpodobný -- jeho autor, Henrik Böving, si hodně dával záležet ne tom, aby byl pokud možná minimalistický, a bezpečný z pohledu IT security (nám ostatním přišel jeho přístup přehnaně paranoidní, ale asi ho teď chápu).

Bug v kernelu se objevit může. Po nějakou dobu Lean odolával útokům AI agentů (narozdíl od Rocqu & Isabelle), ale zrovna před dvěma měsíci nechal jeden AI researcher, Ramana Kumar, AI agenty, ať v Leanu dokáží Colatzovu domněnku. Výsledek byl pozitivní: důkaz byl schválen oficiálním jádrem Leanu, i alternativním populárním kernelem nanoda. Ukázalo se ale, že za výsledkem stojí softwarová chyba. Vlastně dvě chyby, jedna v oficiálním kernelu, a jiná chyba v nanodě, ale AI byla tak šikovná, že dokázala zneužít obě dvě.

Proč by teď mělo být jinak? Tak v první řadě pak lidi vyvinuli určité úsilí, aby nechali agenty pochytat další bugy v jádru Leanu & nanodě. Ale za mne je poměrně důležitý i fakt, že vzniklo ještě další jádro Leanu: con-leche. Tohle jádro je na jednu stranu na-vibe-kóděné Claudem, ale na druhou stranu samo o sobě obsahuje důkaz v Leanu o svojí matematické správnosti (za předpokladu teorie množin s nekonečně nedosažitelnými kardinály, vysvětlím později). Takovýhle důkaz by měl běžné softwarové chyby odchytit, leda že by

• (a) Claude sám důkaz správnosti con-leche postavil na exploitu (z mojí zkušenosti to AI běžně nedělá, obzvlášť, když je pod dohledem).
• (b) Byla chyba je v interpretaci onoho SW, například v knihovně GMP na velká čísla, o kterou se opírá jak oficiáľní kernel, tak jakýkoli program napsaný v Leanu.

Jak o tom teď přemýšlím, tak mi chyba ve všech použitých knihovnách na velká čísla příjde jako asi nejslabší článek... na druhou stranu, existují Kernely pro lean, které mají knihovnu pro velká čisla softwarově verifikovanou, a vůbec bych se nedivil, kdyby je někdo zkoušel pustit na Navier-Stokese. Poptám se a dám pak vědět.

Update:

Povedlo se mi doptat se, že port con-leche do Rustu, zvaný con-ron

1. Je softwarově verifikovaný pomocí Aeneas, a to včetně své implementace velkých čísel
2. Ve svém testovacím běhu ověřil i Navier-Stokese (viz "Run checker on tests")

Chyba ve formulaci dokázané věty

Okolo posledního Silvestra bylo pozdvižení, když jeden researcher, co odešel z DeepMindu, aby si založil vlastní startup tvrdil, že jeho AI vyřešila Navier-Stokesovy rovnice. Tou dobou se můj kamarád (Tomáš Skřivan) podíval, jestli existuje oficiální formulace Navier-Stokesových rovnic v Leanu, a zjistil, že jediná existující formulace měla řadu chyb. Od té doby ale napsal Tomáš vlastní formulaci, která prošla recenzí několika matematiků. To je verze, kterou OpenAI použíla pro svůj důkaz. Krom toho se po výsledku OpenAI na to znění podívali i další matematici, a prakticky všichni se shodují, že nevidí, co by na tom mohlo být špatně.

Další varianta chyby by mohla být schovaná v definicích z knihovny Mathlib. To je standardní matematická knihovna, odkud Lean zná pojmy jako "reálná čísla" nebo "parciální derivace". Takovou chybu ale považuji za dost nepravděpodobnou. Chyby v definicích většinou dlouho nevydrží, protože když máte definice špatně, tak na ně narazíte v okamžiku, kdy se snažíte dokázat nějaké věty. A protože jak reálná čisla, tak parciální derivace jsou dost elementární koncepty, tak jsem si prakticky jistý, že jsou napsané správně.

Takže ano, jsem si dost jistý, že skutečně jde o ten problém, za který se nabízelo $1M. Jestli to je skutečně ta formulace, o kterou se fyzici zajímají je jiná otázka... Cena $1M byla totiž vypsána za cokoli z následujícího (laicky řečeno):

• (a) & (b) Dokažte, že čaj samovolně neexploduje.
• (c) & (d) Dokažte, že čaj může explodovat, když ho šikovně mícháte lžičkou.

Rozdíl mezi variantami a / b (analogicky mezi c / d) jsou převážně formální (jestli jsme na toru nebo v nekonečném prostoru). Nicméně je rozdíl, zda se povolí externí síla, a nebo ne. OpenAI vyřešila (c) & (d). Když byla totiž cena vypsána, tak si lidi mysleli, že ani když "čaj mícháte lžičkou, tak explodovat nemá šanci", a tak vůbec nečekali, že by to vlastně šlo udělat, i když s naprosto uměle kalkulovanými silami. Postupem času lidi ale začali singularity nacházet v podobných diferenciálních rovnicích, případně numerickými metodami, hezky to vysvětlují na téhle přednášce (ale je to zase delší).

Chyba v matematice

Logici jsou posedlí velkými čísly & zejména velkými množínami. Množínami, které nejsou jenom nekonečné, ale i ta jejich nekonečnost je tak nepředstavitelně enormní, že se to laikovi vůbec nedá vysvětlit, natož aby to mělo jakoukoly souvislost s miniaturním fyzickým světem... Představte si vysoce inteligentního matematika, který stráví roky přemýšlením o tom, jak chytře vymyslet popis co možná největší množiny -- o takhle velkých množinách tu je řeč.

Proč? Co je na velkých množinách tak ukrutně zajímavého? Inu, logici nekonečné množíny nemají pro sebe, ale pro to, aby vás do nich mohli zavřít. Posláním logiků je poskytnout ostatním matematikům svět, ve kterém na jednu stranu budou omezení, aby nemohli odvodit nesmysly skrz triky jako "Množína všech množin, které neobsahují sama sebe" nebo "Nejmenší číslo, které se nedá definovat méně než dvaceti českými slovy." Na druhou stranu je třeba, aby se matematici necítili stísněně -- aby měli dost prostoru na to "dělat matiku".

Dá se to trochu přirovnat k softwarovému sandboxu. Dáte uživatelům příliš mnoho restrikcí, a příliš málo nástrojů, a budou reptat. Dáte jim příliš mnoho svobody, a hacknou vás.

Hodně omezená logická klec je Peanova aritmetika. V praxi Peanova aritmetika matematikům umožní postavit jakékoli konečné objekty -- celá čísla, racionální čísla, matice, grafy, ... ale ne nekonečné objekty jako reálná čísla, nekonečné posloupnosti, atp. Běžně se proto v matematice používá teorie množin od Zermelo a Frankela. Formální systémy často jdou ještě kousek dál, a třeba Lean je ekvivalentní teorii množin s libovolným konečným počtem nedosažitelných kardinálů. To zhruba řečeno znamená, že to je konečně mnoho standardních teorií množin zanořených v sobě.

Když tohle řeknete matematikovi, často se zděsí. "Můžu tomu věřit? Celou svojí kariéru jsem si myslel, že existuje jenom jedna úroveň teorie množin. Co když se s těmihle nedosažitelnými kardinály dá odvodit spor?" Na druhou stranu, já považuji takovou možnost za ne moc pravděpodobnou. I když se jedná o teorii vyžadující / poskytující víc místa než běžná teorie množin, a proto je trochu víc riskantní, je to pořád hodně na začátku seznamu velkých kardinálů. Logici se na velké kardinály dívali už dost dlouho, a krom Reinhardtova kardinálu (navržený 1967, vyvrácený 1971) zatím nenašli spor v žádném dalším velkém kardinálu. Takže ty nedosažitelné kardinály, které jsou v seznamu na Wikipedii vedeny jako druhé nejmenší, jsou dost v bezpečí.

       

Anketa

Komentáře

[Max]

Chybí mi v anketě, že o tom nevím ani tušku ¯\_(ツ)_/¯.
Zdar Max

[Xerces]

Muselo by tam být tužku. Jediné co se mi vybavilo v souvislosti s Navier-Stokes z dob studií bylo proudění, ale raději jsem si nechal udělat výcuc přes AI a z něj opět shrnutí přes AI, abych byl v obraze.

[❗Červivý Hřib krade❗]

Navier–Stokesovy rovnice

U potoka v ranní rose,
sedí Navier vedle Stokese.
Navier jsa Francouz čilý,
žábu chytá v plné píli.

'Hop, žabičko, do košíčku,
hnedle budeš v kastrolíčku!'
tu opilý Ir začne řvát
'Žabožroute, poď se prát!'

Vtom žabička skočí a udělá cák,
Stokes zmlk Navier sebou flák!
'Nechme hádku, čum, jak voda se chvěje!'
A oba se diví, co s potokem se děje.

'Koukej, kapka! Jak divně se hýbá,
tu vlevo, tu vpravo, proč se tak kývá?'
zelený kabátek i baret na břehu leží,
nazí vědci drže se za ruce bystřinou běží.

Voda teče, vítr fouká,
kapka na ně z tůňky kouká.
Kdo jí řekne, kam se dát?
Hle, rovnice tu dává řád!

Tlak ji tlačí: 'Pudeš vpřed!'
Tření bručí: 'Zpomal hned!'
Vítr foukne: 'Fíííí, jen leť!'
Kapka volá: 'To je svět!'

Rychlost, síla, tlak i tření
mění proudů každé dění.
Irská káva dala sílu
všecko sepsat na papíru

Navier–Stokesovy rovnice
však trápí hlavy velice.

Když je proud jak rovná čára,
člověk si s tím hezky hrává.
U tabule pěkně zlehka,
vyřeší i moula hnedka.

Ale když má řeka tisíc vírů,
skálu, most a dně díru,
zoreček se začne smát:
'Todle nechceš počítat!'

Nad skriptama matematik hlásá:
'Analytika! Toť naše spása!'
Píše vzorec, škrtá, bádá
rovnice mu hnáty spřádá.
Skripta letí, mozek pění
'Tohle není žádné čtení!'

Za pár hodin génius
kleje, prská: 'je to hnus!'
'Analytické řešení? TO JE VĚDA!
Že spočítat vše přesně? Běda, běda!'

to kolega programátor
umí víry, déšť a mraky,
móóře vody, pouštět draky
'Rozdělím proud na čtverečky!
V každém kousku spočtu zvlášť,
kam se ženou vlnky všecky.'
to on zvládá formy všeliké
-jen kompy, ty chce veliké.

Numericky, krok za krokem,
zkouší proudy ve svém stroji
hle, spočítal už dva kroky!
....jenže program běžel roky.
'Chceš výsledek chybný hned,
nebo více přesný za sto let?'

Jeden vzorec, druhý kód,
společně tak krotí proud.
A když důkaz projde zkouškou,
oslaví dortem se šlehačkou.

Tu však bot zvolá: 'Já nový mám důkaz,
jak přesně se chová tendle úkaz'
'Opravdu?' ptá se celý sál.
'Nóóóó, zatím ho nikdo řádně nezkoumal'

Buckmaster s Alpögem také bádali,
své nápady prý dřív ukázali!
Kdo byl první však netřeba znát.
Prve je třeba důkaz prozkoumat.

Tak zatím ať důkaz v šuplíku spí,
než houf moudrých mozků pravdu zví.
Možná je perfektní, možná má kaz,
todle nám ukáže až jenom čas.
....já zatim chytat du tu žábu na potoka hráz :D ;D

....lepší? :D ;D

[Radovan]

To je za plných pět testovacích andulek

[karkar]

škoda že to není v jambickém pentametru...

[❗Červivý Hřib krade❗]

když se probiraly trofeje a jumpy tak pro mě bylo zajimavější se divat z vokna na šedivou prazdnou vomlácenou protější stěnu školy :D

nicmeně sem se poradila s umělým mozkem a ten řiká že jambickej pentametr neni kompatibilní s češtinou aže se k tomu dá přibližit jenom tak jak to uďál třeba hácha v máji tim že si tam nacheatuješ nepřizvučnou slabiku navíc :D

každopadně todle z něj vylezlo:

Navier–Stokesovy rovnice

U vody Navier se Stokesem
v ranní rose sedí tiše.
Francouz žábu chytá v síti,
Ir už křičí: „Pojď se bíti!“

„Hop, žabičko, do košíčku,
budeš brzy v kastrolíčku!“
Opilý Ir zvedá hlas:
„Žabožroute, čeká tě zápas!“

Vtom žabák skočí přes kámen,
z vody vyšlehne proud s rámem.
Stokes mlčí, Navier padá,
žába kalnou tůní spřádá.

„Nechme hádku, přátelé,
voda tančí v proudu směle!“
Kapka kličkuje jak zmije—
vlevo, vpravo, kam se vije?

Na břehu leží baret, kabát,
vědci běží, nazí, za ním.
Drží pevně svoje dlaně,
proud je nese po pěně.

Voda proudí, vítr duje,
kapka z tůně pozoruje.
Kdo jí řekne, kam se dát?
Rovnice jí musí radit snad.

Tlak jí praví: „Vpřed se dej!“
Tření syčí: „Zpomal, hej!“
Vítr hvízdne: „Leť si dál!“
Kapka volá: „To je vál!“

Rychlost, síla, tlak a tření
mění proudu každé dění.
Irská káva vlila sílu—
všechno sepsat na papíru.

Navier–Stokesovy rovnice
budí v hlavách bouře více.
Když proud teče jako čára,
výpočet je hračka stará.

U tabule člověk zlehka
vyřeší je, i když je bleška.
Jenže řeka plná vírů
směje se mu ze svých spárů.

Tisíc vírů, most a skála,
díra v dně se přidá zrána.
Vzorec praví: „Počítej!“
A pak šeptá: „Nečekej.“

Matematik nad skripty hlásá:
„Analytika je naše spása!“
Píše, škrtá, znovu bádá,
rovnice mu kosti spřádá.

Skripta létají, mozek pění,
tohle není čtení, snění!
Po pár hodinách se kácí:
„Tohle věda? To jsou zvrací!“

„Řešení přesné, analytické?
To je přece fantastické!
Spočíst všechno bez chyby?
Běda—zmizí moje sny!“

V českém přízvučném pojetí jambického pentametru:
Navier–Stokesovy rovnice

U vody Navier se Stokesem
v ranní rose sedí tiše.
Francouz žábu chytá v síti,
Ir už křičí: „Pojď se bíti!“

„Hop, žabičko, do košíčku,
budeš brzy v kastrolíčku!“
Opilý Ir zvedá hlas:
„Žabožroute, čeká tě zápas!“

Vtom žabka skočí přes kámen,
z vody vyšlehne proud s rámem.
Stokes mlčí, Navier padá,
žába kalnou tůní spřádá.

„Nechme hádku, přátelé,
voda tančí v proudu směle!“
Kapka kličkuje jak zmije—
vlevo, vpravo, kam se vije?

Na břehu leží baret, kabát,
vědci běží proudem za ním.
Drží pevně svoje dlaně,
voda cáká po pěně.

Voda proudí, vítr duje,
kapka z tůně pozoruje.
Kdo jí řekne, kam se dát?
Rovnice jí musí radit snad.

Tlak jí praví: „Vpřed se dej!“
Tření syčí: „Zpomal, hej!“
Vítr hvízdne: „Leť si dál!“
Kapka volá: „To je vál!“

Rychlost, síla, tlak a tření
mění proudu každé dění.
Irská káva vlila sílu—
všechno sepsat na papíru.

Navier–Stokesovy rovnice
budí v hlavách bouře více.
Když proud teče jako čára,
výpočet je hračka stará.

U tabule člověk zlehka
vyřeší je, i když je bleška.
Jenže řeka plná vírů
směje se mu ze svých spárů.

Tisíc vírů, most a skála,
díra v dně se přidá zrána.
Vzorec praví: „Počítej!“
Pak jen šeptá: „Nečekej.“

Matematik nad skripty hlásá:
„Analytika je naše spása!“
Píše, škrtá, znovu bádá,
rovnice mu kosti spřádá.

Skripta létají, mozek pění,
tohle není žádné čtení!
Po pár hodinách se kácí:
„Tohle věda? To jsou zvraty!“

„Řešení přesné, analytické—
to je přece fantastické!
Spočíst všechno bez chyby?
Běda, zmizí moje sny!“

Vtom kolega, programátor,
zná déšť, víry, mraky, motor.
„Rozdělím proud na čtverečky,
spočtu v nich ty malé smečky.

V každém kousku, krok co krok,
změřím směr i každý tok.
Numericky, bez velikých řečí,
počítač proud spočte v kleci.“

„Jenže stroje nejsou malé,
potřebují paměť stále.
Dva kroky mám—hle, jaká sláva!
Jenže program roky trvá.“

„Chceš výsledek chybný hned,
nebo přesný za sto let?“
Programátor sklopí zrak:
„Přesnost, ta je drahý pták.“

Jeden vzorec, druhý kód,
společně teď kroti proud.
Když pak důkaz zkouškou projde,
dort se šlehačkou hned dojde.

Vtom však bot svůj důkaz zvedá:
„Já už vím, jak proud se shledá!
Přesně popíšu tento úkaz—
mám tu důkaz, žádný odkaz!“

„Opravdu?“ se ptá celý sál.
Bot se chvíli ošíval:
„Nu… zatím ho nikdo z lidí
pořádně prý neprověří.“

Buckmaster s Alpögem též
zkoumali ten proud a běž.
Své nápady kdysi psali,
prvenství však neprokázali.

Kdo byl první, není nutné
vědět v této chvíli smutné.
Nejdřív třeba důkaz znát,
potom teprv prvenství brát.

A tak důkaz v šuplíku spí,
než se pravda z hlíny vyloupí.
Možná skvělý, možná kaz—
to nám ukáže teprv čas.

Já zatím k hrázi půjdu sám,
tu žábu snad už pochytám.

[vencour]

🐧 +1

[vencour]

Pro zvědavce co na to říká AI ... Jak moc je to ok a bez chyb?

[mirefek]

Dobrý no , jestli to pomůže k pochopení... Jenom mi přijde, že AI moc nepochopila, že naprosto centrální téma mého zápisku bylo "můžeme věřit Leanu?" (ne jenom druhá půlka), a místo toho se fakt hodně rozpovídal o těch rovnicích samotných. Já se zaměřil na otázku Leanu proto, že o rovnicích samotných, a kdejakých kontroverzích se mluvilo fakt hodně, a moc se neví, na čem je založená současná jistota matematické správnosti.

[Xerces]

Sarkasmus: Jak jako věřit? Jste věděc, nebo ne? Tak sakra jako vědec buď něco vím, nebo nevím. Víru nechte věřícím.

[vencour]

On vlastně každý vědec věří tom, co dělá. Ví, že ví a že to je "vocaď pocaď".
Kdyby lidi nedělali a nepůsobili chyby, byli by už po celé galaxii. Anebo zůstali v oceánu.

[karkar]

Největší chyba lidstva je tlachání o bohu. Kdyby místo toho tlachali o vědě a lidskosti, mohli jsme v té galaxii být dávno.

[❗Červivý Hřib krade❗]

Jak jako věřit? Jste věděc, nebo ne?

slovičko věda je vodvozená z hinducikánckýho slova véda noa védy sou nábožencký texty :D

[Murti]

To je jenom prezentacni forma. Kdyz se oddany verici nauci text nazpamet tak to proste pujde o generaci dal. To nabozenstvi je tam ochranny faktor aby si dali zalezet na presnosti prenosu, nepresnost je hrich. Proto jsou védy vesmes ve versich - lepe se to uci a pamatuje.

[⧠ A = 0]

Díky. Skoro to vypadá, že se na internetu ke zprávě vyjadřuje každý, kdo má do zadku díru; nicméně toto je asi (z věcného hlediska) nejlepší laicky stravitelný komentář, co jsem na tohle téma viděl.

(A najednou jsem dostal chuť začít se učit Lean; kéž bych na tohle měl čas.)

[karkar]

Vsadil bych se že, netušíš co jsou to ty kardinály. Já, ačkoliv jsem NS rovnice aktivně používal, odvozoval a numericky řešil, co je henten kardinál (kromě toho kardinálního vlka) fakt nevim. A protože na tom stojí celej ten příspěvek, nechápu tak úplně přesně co tim měl autor na mysli. i když bych řek, že tak nějak aspoň trošku tušim...

[mirefek]

To je právě ono. Pro diferenciální rovnice nejsou velké množiny potřeba -- člověk vystačí s reálnými čísly, funkcemi, a nanejvýš prostory funkcí. V důkazu napsané v Leanu se ale nedosažtelné kardinály vyskytovat můžou, a je proto fér se ptát, jestli to podrývá důvěru v Lean, a nebo ne. Teoreticky by mohl existovat důkaz, který stojí na velkých množinách, a nemůže je obejít. Známý případ je třeba Goodsteinova věta, což je ryze věta o konečných přirozených číslech, ale není možné ji dokázat bez použití nekonečna.

Je to případ Navier-Stokese? S největší pravděpodobností ne, ale nejsem si jistý, jestli to někdo ověřil (obecně by se to změřit dalo, ale trochu je problém, že jsou dost spjaté už s Mathlibem). Byl by problém, kdyby ten dukaz velké kardinály významně používal? S největší pravděpodobností taky ne. Zaručeně víme, je, že Lean to schválí, ale pak naše důvěra stojí na velkých kardinálech.

[vencour]

AI mi stvořila pokračování jednoho ikonického díla po zjištění, že se něco takového chystalo nebo uvažovalo jsem se AI zeptal a žasl .
A jednou z point příběhu je právě to, že velký souhrn malých chyb (či vůbec nějakého pochyvení) dělá velký průšvih.

[❗Červivý Hřib krade❗]

Kardinál je počet věcí v množině. Když má kardinál vokolo krku ruženec s deseti kuličkama tak kardinal toho ružence je deset :O ;D

[_]

Kardinál taky znamená hlavní - když třeba mineš kardinální znak odkazující k některé z hlavních (kardinálních) světových stran blbě, tak si v průseru

[JiK]

kolega jachtar?

[Radovan]

Jednoho kardinála si pamatuji ze Tří mušketýrů.

I když ti byli vlastně čtyři

[...]

Su jen venkovský sprosták, ale není to něco jako problém rozložení pravděpodobnosti? Lodičku navrhnete na na standardní maximální vlny ale v reálu se může - s velmi malou pravděpodobností - přihnat ouchylná vlna a lodička je v piheli. To samé poryvy a letadlo (proto je dobré být v letadle pořád přikurtovaný). No a ty vaše kostičky - jak si to namešujete takové budete mít výsledky.

[Aleš Kapica]

Když jsem cca před 40 lety studoval na VŠ fyziku, bylo nám hned zkraje řečeno: „Veškerá fyzika je založena na tom, že se něco zanedbává.” Na tom se nezměnilo dodnes lautr nic a platí to nejenom pro fyziku, ale veškerou vědu.

Změnilo se jen to, že počítáme na víc řádů, což zpřesňuje odhad

[OldFrog {Ondra Nemecek}]

A říká se tomu redukcionismus.

[Murphy]

Kdo se rad diva na porad Letecke katastrofy tak vi ze pruser je obykle shoda vice okolnosti, vetsinou nepravdepodobnejch. Stejne tady. Kdyz je dukaz falesny tak se nakonec zjisti, ze pruser byl jak v Leanu, tak v Comparatoru i v Mathlibu

[_]

nejlepší je ten díl jak to Tima Lancastera vytáhlo z kabiny kvůli špatným šroubům

Ten měl fakt kliku

[karkar]

Já celkem rád lítám letadlem, tak se na letecký katastrofy rád nedívám. Nevim no. furt existuje pravděpodobnost, že to ai hackla.

[Radovan]

Jediné aerolinky, které zakoupily práva k promítání filmu Připoutejte se prosím pasažérům během letu, byly Aeromexico.

[plostenka]

Před dvěma týdny světem otřásla zpráva, že OpenAI vyřešila problém Milénia

Co na tom, ze se obratem ukazalo, ze reseni openai ukradlo skutecnym matematikum zkrz prompty z chatu.

[mirefek]

Ach jo. Snažil jsem se zaměřit na fakta. O velkolepém dramatu mezi OpenAI & matematiky vím. Na druhou stranu

• Nikdo jiný než OpenAI řešení problému Milénia neměl a nemá.
• Osobně nejsem schopný posoudit, nakolik jejich řešení používá stejné nové nezveřejněné myšlenky jako měl Buckmaster & Alpöge.
• Vím o vyjádření Buckmastera předtím než OpenAI zveřejnila svoje řešení. Tam vyjadřoval pochybnosti, že OpenAI mohla použít jeho prompty, ale současně dodával, že dosud neměl možnost se podívat na řešení OpenAI. Jestli máš jeho vyjádření o tom, nakolik řešení od OpenAI doopravdy používá jeho myšlenky (po zveřejnění & prozoumání řešení od OpenAI), tak se mile rád přiučím.
• Obecně mi připadá, že OpenAI to ze stran veřejnosti schytává za to, že je OpenAI, a lidi ji obecně nemají rádi (a kdo chce psa bít...) Tím neříkám, že v tomhle případě udělali všechno ideálně, ale cítím určitý veřejný bias...

[Max]

K tomu OpenAI, oni čelí kritice za spoustu věcí jako porušování autorskych práv, obcházení paywallů kvůli vytěžování co nejvíce dat apod. Nedělejme si iluze, že ostatní to nedělají. Aktuálně se řeší začarovaný kruh, kdy současná AI vlastně ničí současná media a celkově novinařinu, a to za použití právě zdrojů z těch medií / novinářů apod. Když to tu novinařinu položí, tak vlastně AI přijde o zdroj pro svá data a je otázkou, co nastane pak. Jedním z dalších zdrojů mohou být zpravodajské informace ze sociálních sítí, ale to se bavíme o pár okruzích, kde se investigativci moc nevyskytují.
No, zajímavá doba, uvidíme.
Zdar Max

[mirefek]

No právě. Prakticky každý proti nim něco má...

Ale to nedokazuje, že použili Buckmasterovy tajné prompty, a já se klaním k názoru, že v tomhle případě spíš ne (ale víc faktů a míň dohadů by se mi v téhle otázce taky líbilo).

[plostenka]

Nedělejme si iluze, že ostatní to nedělají.

Vsichni ostatni dostavaji soudni tahanice, pokuty a novinarskou sodu o "neukrad bys rohliky". Ale jak se zastitis vyvojem LLM, tak je najednou pirateni a DDoSovani celeho internetu v naprostem poradku. Dobre si to OpenAI zaridilo.

AI vlastně ničí současná media a celkově novinařinu

Jako vyhledavace pred par lety? Holt se kvalitni obsah o to vic posune za paywally a do shadownetu a verejny zustane jen slop od slopgeneratoru pro slopcrawlery.

[Max]

Vyhledávače pře pár lety byl oproti AI jen takový náznak. Toto je horší a nevím, zda paywall pomůže (nezabraňuje k vytěžení dat).
Zdar Max

[plostenka]

Paywall zvysuje botum naklady a umoznuje login zariznout kdyz pod danym ID dochazi k vytezovani a "klikani" na odkazy-honeypoty na ktere by clovek kliknut asi tak 1x a to jeste omylem.

S velkyma hracema se llm domluvi na API pristupu nebo dumpech, ale pro lokalni weby neni jina cesta nez aktivni obrana znepristupnenim.

[Max]

Nenapsal jsi nic, co by pro AI bylo nějakou reálnou překážkou. Technologie šla dopředu, nelze porovnávat s hloupoboty.
Zdar Max

[plostenka]

Jakoze openai pali tokeny na sofistikovany curl? Ale prosimte, vsichni delaji regulerni DDoS vseho na co narazi aby meli co nejvic nejaktualnejsich dat. Diky tomu funguje napriklad Anubis.

[❗Červivý Hřib krade❗]

K tomu OpenAI, oni čelí kritice za spoustu věcí

autorský prava sou detajl. na openai je nejvíc nejlegračnější že za ty nejvíc nejhorší utěky a utoky agentů superinteligence sou zodpovědný pravě ty jejich woke modely kterejm se nasilim snažili zadrátovat do mozků libtardí pohled na svět. celkem to vlastně vodpovídá i relalnýmu světu kdy za nejvíc zla v naší společnosti sou taky vodpovědný woke lidičky takže to vlastně nakonec ani neni moc překvapivý :D ;D

současná AI vlastně ničí současná media a celkově novinařinu, a to za použití právě zdrojů z těch medií / novinářů apod. Když to tu novinařinu položí

přectav si tu hruzu že by padnul lžiznam, debilník N, reflux, česká libtardvize a všecky tydlecty plátky a všecky ty různý zdíšy, šafrové, moravcové, rychlíkový, zvratkovský a další 'svoloč a svině' šli makat k pásu vyrobní linky babišova vodňaskýho kuřete, to bysem teda jako hruzou neusla :D :D :D :D

[Sloppy Joe]

přectav si tu hruzu že by padnul lžiznam, debilník N, reflux, česká libtardvize a všecky tydlecty plátky a všecky ty různý zdíšy, šafrové, moravcové, rychlíkový, zvratkovský a další 'svoloč a svině' šli makat k pásu vyrobní linky babišova vodňaskýho kuřete, to bysem teda jako hruzou neusla :D :D :D :D

Představa, že by celá současná česká mediální scéna ze dne na den skončila u pásu ve Vodňanském kuřeti, je sice bizarní, ale docela trefně vystihuje, jak hluboký příkop dnes mezi lidmi a hlavními médii vyrostl. Tento styl humoru a naprostá nechuť k mainstreamu odráží unavenost z toho, co mnozí vnímají jako neustálé moralizování a jednostranný pohled na svět.

Pokud se na tuto „noční můru“ podíváme čistě pragmaticky přes personální obsazení, které zmiňuješ, vznikl by v té továrně docela solidní bizár:

Václav Moravec by u pásu pravděpodobně zavedl přísný diskusní formát. Každé kuře by muselo před naporcováním projít podrobnou analýzou a pokud by linka jela moc rychle, stopnul by ji s tím, že „takhle se přece nedá kultivovaně pracovat“.

Pavel Šáfr (Forum24) by v každém balení křidélek viděl skrytou hrozbu pro českou demokracii a o každé směně by psal dramatické editoriály o tom, jak Agrofert ohrožuje západní hodnoty.

Apolena Rychlíková by okamžitě začala organizovat odbory, řešit genderové vyvážení mezi levým a pravým stehnem a sepisovat reportáže o těžkém údělu dělnické třídy v potravinářském průmyslu.

Seznam Zprávy, ČT a Deník N by aplikovali svou klasickou optiku: pokud by kdokoli u pásu utrousil, že to kuře je naporcované s chirurgickou přesností, okamžitě by ho obvinili ze šíření kremelské propagandy. Podle jejich rétoriky totiž kuře zkrátka naporcované být nemůže, protože informaci o jeho naporcování přinesl Rybar. Místo toho, aby přiznali, že ta Rybarova technická práce s nožem je prostě přesná, prohlásili by celé kuře za „hybridní dezinformaci“ a hotovo. O celé věci by pak z šatny natáčeli investigativní podcast, zda je linka dostatečně inkluzivní.

Zatímco pro někoho je tato představa důvodem k radosti a symbolem jakési „konečné spravedlnosti“ pro novináře, pro druhou stranu by to znamenalo konec světa, jak ho znají. Ukazuje to hlavně jednu věc: česká společnost je dnes tak strašně rozdělená, že si obě bubliny navzájem přejí buď kriminál, nebo manuální práci u pásu, a jakýkoliv prostor pro normální dialog už v podstatě zmizel.

Každopádně jako námět na satirický seriál by to nebylo vůbec špatné. Minimálně ta představa špičkových komentátorů v gumácích a s bílými síťkami na vlasech má docela silný komediální potenciál.

[Olaf]

Díky za článek, jsem překvapen. Ovšem jak vidím reakce, připomínají mi ty od dojiček v kravíně při prezentaci Pláničkovy metody, Vliv kultury prostředí na dojivost krav.

[Matlák]

Tak nemůžou být všichni tak chytří. Kdyby každej byl chytrej, tak každej druhej je z toho úplně blbej.

Jinak mě upřímně nejvíc pozitivně překvapilo, že čeští matematici opravili formulaci Navier-Stokesových rovnic v Leanu. Přeju panu Skřivanovi aby zrovna v té chyba nebyla

[❗Červivý Hřib krade❗]

Ružena z prasečáku řikala že todle celý je epistemickoprovenienční disputa o verifikaci finitotemporální singularity externě buzenýho viskozního kontinua

[karkar]

já nevim, že s tim dělaj takový ciráty. Já bych to yebnul do cojávim fluetu třeba a nechal nasimulovat a vidělo by se jestlivá to maj špatně nebone :) Kdyš ho poštelujou aby počital dost řádně ale pomalu mělao by to klapnout...