Az AI automatizálja a matematikai bizonyítások generálását általános célú modellekkel
Az elmúlt néhány évben a nagyméretű AI modellek ügyesek lettek a kódolásban, és elkezdtek más hasznos tudományágakba is általánosodni, különösen a matematika és a tudomány területén. Mint az AI fejlesztés legtöbb aspektusában, itt is a rendszerek egyre nagyobb általánosítása és egyszerűsítése volt a történet, ahogy elmozdulunk a magasan specializált matematikai modellektől az általános célú foundation modellek kihasználása felé, és megfelelő eszközöket biztosítunk számukra, hogy előhívjuk képességeiket egy adott területen. Ennek legújabb példája a Numina-Lean-Agent, egy AI rendszer, amely standard, általános foundation modelleket használ matematikai érvelésre. Ezzel a szoftverrel matematikusok egy csapata megoldotta a Putnam 2025 matematikai verseny összes feladatát – felülmúlva a sokkal több matematikára specifikus dolgot használó szabadalmaztatott rendszerek teljesítményét – és felhasználták eredeti matematikai kutatások elvégzésére is, együttműködve vele a Brascamp-Lieb tétel formalizálásában.
Mi a Numina-Lean-Agent? A szoftvert a Chinese Academy of Sciences, University of Liverpool, Xi’an Jiaotong-Liverpool University, Tongji University, University of Cambridge, Project Numina, Imperial College London és a University of Edinburgh kutatóiból álló csapat építette. A szoftver „egy formális matematikai érvelő, amely egy általános kódoló ügynökön alapul”. Néhány kulcsfontosságú komponense van:
Matematika felfedezése együtt: A Putnam demonstráció mellett a szerzők a szoftvert aktív partnerként is használták néhány matematikai munkában, különösen a Brascamp Lieb formalizálásában (nem fogom színlelni, hogy el tudom magyarázni, mit jelent ez). „Kevesebb mint két hétnyi szórványos együttműködés alatt a két emberi szakértő és az ügynök több mint 8000 sor Lean kód formalizálását fejezte be. E folyamat során az ügynök önállóan körülbelül 70 új definíciót, lemmát és tételt vezetett be, illusztrálva ezzel azon képességét, hogy aktívan bővítse a formális könyvtárat, és részt vegyen nagyszabású, tartós formalizálási erőfeszítésekben” – írják a szerzők.
- Lean-LSP-MCP: Szoftver, amely lehetővé teszi az AI ügynökök számára, hogy interakcióba lépjenek a Lean tételbizonyítóval. „Képessé teszi a modelleket a Lean projektek mélyreható megértésére, elemzésére és manipulálására”, és eszközöket biztosít a modelleknek a szemantikai tudatosság és interakció, a kódvégrehajtás és stratégiafeltárás, valamint a tételek lekérése terén.
- LeanDex: Kapcsolódó tételek és definíciók szemantikai lekérése – alapvetően egy keresőeszköz a tételekhez.
- Informal Prover: Egy rendszer, amely Gemini modelleket használ informális megoldások generálására.
- A legérdekesebb eszköz mind közül: Discussion Partner: Egy eszköz, amely „felhatalmazza a Claude Code-ot arra, hogy segítséget kérjen a Lean formalizálás során: amikor akadályokba ütközik – például bizonyítási szűk keresztmetszetek, stratégiaválasztási dilemmák vagy az átmeneti lemmák kétértelműségei –, az elsődleges modell proaktívan kezdeményezhet megbeszéléseket más LLM-ekkel”.
Miért fontos?
Miért fontos ez – képességi többlet és AI ökológiák: A Numina-Lean-Agent szépen bemutat két fontos dolgot a kortárs AI-ról: 1) az AI rendszerek sokkal többre képesek, mint gondolnák az emberek, és néhány speciális keretrendszer és eszköz létrehozása gyakran drámaian jobb képességeket csal ki rendszereinkből (itt a matematika, de sok területen bebizonyosodott), és 2) az AI ökológia nagy egészében sok különálló frontier modellből áll, és úgy tűnik, hogy ezeknek a modelleknek az egymással való interakciója gazdagsághoz vezethet, hasonlóan ahhoz, ahogy különböző típusú emberek konzultálása egyetlen problémáról jobb választ eredményezhet, mint csak egy személlyel beszélni. ---