Sampung pagsulong sa matematika at teoretikal na computer science

Nais naming bigyan ang mga siyentipiko at matematiko ng mga kasangkapang nagpapabilis sa pagtuklas. Kaya kamakailan ay inanunsyo namin ang ChatGPT for Academic Researchers⁠, isang inisyatibang nagbibigay sa 100,000 siyentipiko at matematiko ng libreng access sa aming pinakamahusay na mga modelo ng ChatGPT. Patuloy rin naming sinusuri ang aming mga modelo gamit ang mga bukas na suliranin sa pananaliksik habang binubuo ang mga ito.

Noong Mayo, ibinahagi namin ang isang kontra-halimbawang binuo ng AI⁠ para sa haka-hakang unit-distance ni Erdős, na natuklasan habang sinusuri ang isang hindi pa inilalabas na modelo. Nakapagbigay-inspirasyon na ang gawaing ito sa mga bagong pagsulong sa matematika at teoretikal na computer science¹. Ngayon, ibinabahagi namin ang sampung piling resulta, na bawat isa ay lumulutas o nagbibigay ng malaking pagsulong sa isang matagal nang bukas na suliranin. Saklaw ng mga suliraning ito ang high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, mga alhebrang Operator, quantum complexity, lattice cryptography, at extremal combinatorics. Mahalaga ang lahat ng suliraning ito sa kani-kanilang komunidad sa matematika, at ilan sa mga ito ay may malawak na kabuluhan sa buong larangan.

Naghaharap kami ng mga bagong resulta para sa mga sumusunod na suliranin. Nakamit ang mga resulta gamit ang panloob na bersyon ng Astra, ang susunod naming pangunahing modelo. Sa mga rate ng Sol API, humigit-kumulang $2,000 ang halaga ng kabuuang token na kinailangan upang makahanap ng mga solusyon sa mga suliraning ito. Pagkatapos, inihanda ng mga tao ang mga argumentong ito bilang mga manuskrito sa tulong ng parehong modelo. Pagkaraan, ginawang pormal ng modelo ang bawat argumento sa isang sertipiko sa Lean⁠(magbubukas sa bagong window). Inilalabas din namin para sa bawat solusyon ang salaysay ng modelo tungkol sa proseso ng pag-iisip nito.

1. Pag-iimpake ng mga sphere sa matataas na dimensiyon. Mga bagong upper bound sa density ng sphere packing hanggang sa threshold na Cohn–Elkies.
2. Mga binary at spherical code: Mga bound na pinahusay nang eksponensiyal para sa pinakamalaking sukat ng mga binary code sa anumang itinakdang minimum na distansiya, na may katumbas na mga resulta para sa mga high-dimensional spherical code.
3. Mga non-sofic group. Isang konstruksiyong nagpapatunay sa pag-iral ng mga non-sofic group at tumutugon sa isang pangunahing bukas na tanong sa group theory.
4. Haka-haka ni Connes tungkol sa rigidity. Pagpapabulaan sa matagal nang haka-haka na ang ilang grupo ay natatanging natutukoy ng kani-kanilang mga alhebrang von Neumann.
5. Complexity ng arithmetic circuit. Mga bagong lower bound para sa pagkukuwenta ng permanent gamit ang mga arithmetic circuit at formula, kabilang ang lower bound na may order na n⁴/log n para sa arithmetic formula.
6. Quantum parallel repetition. Isang exponential parallel repetition theorem para sa mga pangkalahatang larong quantum na may dalawang manlalaro, na nagpapalawak sa isang saligang prinsipyo mula sa classical complexity theory.
7. Suliranin sa pinakamalapit na vector. Polynomial-factor hardness ng approximation para sa suliranin sa pinakamalapit na vector, isang saligang tanong tungkol sa lattice na may kaugnayan sa post-quantum cryptography.
8. Haka-haka ni Ehrhart tungkol sa volume. Pagtukoy, sa bawat dimensiyon, sa pinakamalaking posibleng volume ng isang convex body na ang centroid lamang ang interior lattice point nito.
9. Mga multicolor Ramsey number. Isang superexponential lower bound para sa mga multicolor triangle Ramsey number, na lumulutas sa Erdős problem 183.
10. Mga haka-haka tungkol sa extremal number. Mga resulta sa mga haka-haka tungkol sa compactness at degeneracy sa extremal graph theory, na lumulutas sa Erdős problems 146 at 180.

Ang paglitaw ng mga sistemang kayang mag-ambag sa pananaliksik sa matematika ay nagbubukas ng mga tanong na hindi kayang sagutin ng isang kumpanya ng teknolohiya lamang. Maraming pananaw tungkol sa papel ng AI sa matematika, at lubos naming iginagalang at nauunawaan ang mga nag-aalala sa epekto nito, kabilang ang mga lumagda sa Leiden Declaration on AI and Mathematics⁠(magbubukas sa bagong window). Naniniwala kaming dapat matapat na ilarawan ng atribusyon kung paano nabuo ang isang resulta: ang pag-angkin na tao ang may-akda ng isang patunay na ganap na binuo ng AI system ay maling maglalarawan kapwa sa ambag ng sistema at sa tunay na katangian ng intelektuwal na gawain ng tao. Tumulong kaming ihanda ang mga manuskrito at gawing pormal sa Lean ang mga patunay, at pananagutan namin ang kawastuhan ng mga ito, samantalang ang mismong mga argumentong matematikal ay binuo ng aming sistema. Umaasa kaming masusing susuriin ng komunidad ng matematika ang mga resultang ito, iuugnay ang mga ito sa mas malawak na konteksto, at bibigyang-buhay ang mga ideya sa likod ng mga ito sa pamamagitan ng bagong pananaliksik at pagtuklas.

Habang umuunlad ang mga AI system bilang mas sopistikadong katuwang sa pananaliksik, mahalagang tiyakin ang malawak na access upang masuportahan ang mga siyentipiko at matematiko sa pag-unawa at paghubog sa kinabukasan ng kanilang mga larangan sa mapagbagong panahong ito.