Hilbert: így épít formális matematikai bizonyításokat az Apple rendszere
Az Apple bemutatta a Hilbert nevű ügynöki keretrendszert, amely informális matematikai érvelést kapcsol össze a Lean 4 formális bizonyítás-ellenőrzésével. A rendszer a sikertelenül megoldott feladatokat részproblémákra bontja, majd a verifikátor visszajelzése alapján javítja a bizonyításokat.
- A Hilbert informális érvelést és Lean 4-es formális bizonyítást kapcsol össze.
- A rendszer négy komponenst használ, köztük bizonyításgeneráló modellt és verifikátort.
- A miniF2F benchmarkon 99,2 százalékos eredményt ért el.
- A PutnamBench 660 feladatából 462-t oldott meg, ez 70,0 százalék.
- A tanulmányt elfogadták a NeurIPS 2025 MATH-AI workshopjára.
A természetes nyelvű gondolkodás és a formális ellenőrzés összekapcsolása
Az Apple kutatói szerint a nagy nyelvi modellek jelentős matematikai érvelési képességeket mutatnak, megoldásaik azonban gyakran olyan hibákat tartalmaznak, amelyek automatikusan nem ellenőrizhetők. A formális tételbizonyító rendszerek, köztük a Lean 4, ezzel szemben teljes pontosságú automatikus ellenőrzést tesznek lehetővé.
Ez a különbség egyben korlátot is jelent. Az Apple leírása szerint a jelenlegi, bizonyításokra specializált nyelvi modellek lényegesen kevesebb feladatot oldanak meg, mint az általános célú modellek természetes nyelven. A Hilbert ezt a különbséget próbálja csökkenteni az informális érvelés és a formális verifikáció együttes használatával.
Négy komponens dolgozik együtt
A Hilbert négy fő összetevőt hangol össze. Az egyik egy informális nyelvi modell, amely matematikai érvelésben erős. Ezt egy Lean 4-es taktikákra optimalizált, specializált bizonyításgeneráló modell egészíti ki. A rendszerhez tartozik továbbá egy formális verifikátor és egy szemantikus tételkereső.
Ha a bizonyításgeneráló modell nem tud megoldani egy feladatot, a Hilbert rekurzív felbontást alkalmaz. A problémát részfeladatokra, vagyis részgólokra bontja, amelyeket a bizonyításgeneráló vagy az érvelő modell oldhat meg. A formális verifikátor visszajelzései alapján a rendszer szükség esetén módosítja a hibás bizonyításokat.
99,2 százalék a miniF2F teszten
Az Apple közlése szerint a Hilbert a kulcsfontosságú teszteken jelentősen felülmúlta a korábbi megközelítéseket. A miniF2F benchmarkon 99,2 százalékos eredményt ért el, ami 6,6 százalékponttal jobb a legjobb nyilvánosan elérhető módszernél.
A rendszer a PutnamBench teszten is a közlés szerint a legjobb ismert eredményt hozta. A 660 feladatból 462-t oldott meg, ami 70,0 százalékos teljesítmény. Ez meghaladta a SeedProver 50,4 százalékos eredményét, és 422 százalékos javulást jelentett a legjobb nyilvánosan elérhető alapvonalhoz képest.
Kutatási eredmény, nem felhasználói termékbejelentés
A Hilbertről szóló tanulmányt 2025 októberében publikálták, és elfogadták a NeurIPS 2025 MATH-AI workshopjára. A szerzők között Sumanth Varambally, Thomas Voice, Yanchao Sun, Zhifeng Chen, Rose Yu és Ke Ye szerepel. Rose Yu a UC San Diegóhoz kötődik, Sumanth Varambally munkája pedig az Apple-nél készült.
A közölt eredmények alapján a Hilbert azt mutatja meg, hogyan lehet az informális matematikai gondolkodás szélesebb problémamegoldó képességét a Lean 4 ellenőrizhetőségével kombinálni. A hír közvetlenül egy kutatási keretrendszerről szól, amely formális bizonyítások generálását vizsgálja.
