Newsletter Subscribe
Enter your email address below and subscribe to our newsletter
[forminator_form id="25163"]

qz+1garymarcus.substackcacm.acm+1OpenAI ilmoitti 1. elokuuta, että sen julkaisematon Astra-malliperhe tuotti ratkaisuja 10 pitkään avoinna olleeseen ongelmaan matematiikassa ja teoreettisessa tietojenkäsittelytieteessä, julkaisten 249-sivuisen käsikirjoituksen ja täysin varmennetut Lean 4 -todistussertifikaatit GitHubissa. Tulokset kattavat aloja, kuten korkeampiulotteinen geometria, koodausteoria, ryhmäteoria, kvanttikompleksisuus ja äärimmäisyyskombinatoriikka, ja yritys raportoi kokonaislaskentakustannusten olevan noin 2 000 dollaria GPT-5.6 Sol API -hinnoilla.ndtv+2
OpenAI:n blogikirjoituksen mukaan Astra tuotti edistysaskelia pallojen pakkausrajoissa, virheenkorjauskoodeissa ja ensimmäisen eksplisiittisen ei-sofisen ryhmän rakentamisessa, mikä on ollut avoin kysymys vuodesta 1999 lähtien. Malli todisti myös kvanttirinnakkaistoistoteoreeman yleisille kahden pelaajan kietoutuneille peleille ja tuotti tuloksia Ehrhartin tilavuuskonjektuurista ja Connesin jäykkyyskonjektuurista. Kolme muuta Paul Erdősin luettelon ongelmaa ratkaistiin myös, kertoo Quartz.qz+2
OpenAI totesi, että sen tekoäly tuotti keskeiset matemaattiset argumentit, kun taas tutkijat formalisoivat jokaisen todistuksen Lean-todistusavustajalla. GitHub-arkiston "sorry"-laskuri, joka on merkki varmistamattomista vaiheista, on nollassa, mikä tarkoittaa, että jokainen looginen askel kaikissa kymmenessä todistuksessa on koneellisesti tarkistettu.qz
Muodollisesta varmennuksesta huolimatta kriitikot ovat kyseenalaistaneet, edustavatko tulokset todellista harppausta tekoälyn kyvyissä. Tunnettu tekoälytutkija Gary Marcus kirjoitti, että Anthropicin matemaatikko Levent Alpöge pystyi replikoimaan osittain puolet OpenAI:n tuloksista 24 tunnissa käyttämällä Fablea, jo julkisesti saatavilla olevaa mallia. Marcus väitti, että tämä herättää epäilyksiä siitä, onko Astra itse läpimurto vai piileekö edistys siinä, että tunnistetaan, mitkä ongelmat soveltuvat haku- ja varmennustekniikoille.garymarcus.substack
"OpenAI ei raportoi, mitä ongelmia he yrittivät ja joissa he epäonnistuivat. He ovat antaneet meille osoittajan ilman nimittäjää, mikä on aina huolestuttava merkki", Marcus kirjoitti. Hän huomautti myös, ettei OpenAI ole vielä päättänyt, nimetäänkö Astra GPT-6:ksi vai GPT-5.7:ksi, mikä viittaa siihen, että sisäisesti harppausta saatetaan pitää inkrementaalisena.garymarcus.substack
ACM:n viestintäblogi julkaisi 4. elokuuta analyysin, jossa Astraa kuvailtiin "hämmästyttäväksi, mutta pahasti liioitelluksi". Samaan aikaan Leidenin julistus matematiikan tekoälystä, jonka sadat matemaatikot allekirjoittivat kesäkuussa 2026, on nostanut esiin laajempia huolia epäluotettavista tekoälyn tuottamista todistuksista ja attribuutiosta.analyticsinsight+1
OpenAI ei ole ilmoittanut Astran julkaisupäivää, ja mallin on läpäistävä liittovaltion tekoälyturvallisuustarkastus ennen kuin se saavuttaa käyttäjät. Yritys tunnusti keskustelun todeten, että sillä on "syvä kunnioitus ja ymmärrys niitä kohtaan, jotka ovat huolissaan sen vaikutuksista", ja se aikoo julkaista metodologiansa. OpenAI lanseerasi myös äskettäin ChatGPT for Academic Researchers -palvelun, joka tarjoaa 100 000 tutkijalle ilmaisen pääsyn uusimpiin malleihinsa.analyticsinsight+1
Matemaatikko Terence Tao teki Marcuksen viittaamassa 26. heinäkuuta pitämässään luennossa eron yksittäisten avointen ongelmien ratkaisemisen, jossa tekoäly näyttää vahvalta, ja matemaattisen teorian rakentamisen välillä, missä tekoälyn kyvyistä ei ole vielä näyttöä.garymarcus.substack