AlphaGeometry, Sistem AI Geometri Tingkat Olimpiade

 (deepmind.google)
1 poin oleh GN⁺ 2024-01-18 | 1 komentar | Bagikan ke WhatsApp
  • Saat Olimpiade Matematika Internasional menjadi ajang uji penalaran matematika AI, AlphaGeometry menyelesaikan 25 dari 30 soal geometri dalam batas waktu, mendekati rata-rata peraih medali emas manusia yaitu 25,9 soal
  • Kuncinya adalah gabungan model bahasa jaringan saraf dan mesin penalaran simbolik berbasis aturan, yang menangani usulan konstruksi intuitif dan verifikasi logika formal dalam satu loop
  • 100 juta contoh sintetis unik yang dibuat tanpa demonstrasi manusia mengurangi bottleneck pelatihan, dan 9 juta di antaranya mencakup konstruksi bantu yang diperlukan untuk pembuktian
  • Semua solusi olimpiade diverifikasi dengan komputer, dan Evan Chen menilai keluarannya dapat diverifikasi mesin sekaligus dapat dibaca manusia, serta mengikuti aturan geometri klasik yang dipakai siswa
  • Dalam satu edisi IMO, biasanya hanya 2 dari 6 soal yang berupa geometri sehingga cakupan penerapannya terbatas, tetapi ini menjadi model AI pertama yang, hanya dengan kemampuan geometrinya, dapat melampaui standar medali perunggu IMO tahun 2000 dan 2015

Performa pada benchmark geometri IMO

  • AlphaGeometry yang dipublikasikan di Nature memecahkan soal geometri kompleks pada tingkat yang mendekati peraih medali emas olimpiade manusia
  • Benchmark terdiri dari 30 soal geometri IMO-AG-30 yang dipilih dari olimpiade tahun 2000 hingga 2022
    • AlphaGeometry: menyelesaikan 25 soal dalam batas waktu
    • Pendekatan terbaik sebelumnya, Wu’s method: menyelesaikan 10 soal
    • Rata-rata peraih medali emas manusia: menyelesaikan 25,9 soal
  • Google DeepMind merilis kode dan model AlphaGeometry sebagai open source

Struktur sistem neuro-simbolik

  • AlphaGeometry adalah sistem neuro-simbolik, tempat model bahasa jaringan saraf dan mesin penalaran simbolik bekerja bersama untuk menemukan pembuktian teorema geometri yang kompleks
  • Model bahasa dengan cepat mengidentifikasi pola dan relasi umum dari data untuk memprediksi konstruksi yang kemungkinan berguna
    • Namun, kemampuannya untuk melakukan penalaran ketat atau menjelaskan keputusan bisa jadi terbatas
  • Mesin penalaran simbolik mencapai kesimpulan dengan mengikuti logika formal dan aturan yang jelas
    • Dapat dijelaskan dan rasional, tetapi ketika menangani masalah besar sendirian, bisa lambat dan kurang fleksibel
  • Dengan menggunakan kedua komponen bersama-sama, model bahasa mengusulkan komponen bantu seperti titik, garis, atau lingkaran baru, lalu mesin penalaran menurunkan kesimpulan tambahan tentang bangun berdasarkan usulan tersebut

Loop pemecahan untuk menemukan konstruksi bantu

  • Soal geometri olimpiade tidak selalu bisa langsung diselesaikan hanya dengan bangun yang diberikan, dan terkadang perlu menambahkan komponen geometri baru yang dibutuhkan untuk solusi
  • Proses pemecahan AlphaGeometry bekerja dengan penalaran simbolik dan usulan model bahasa yang berjalan bergantian
    • Dari bangun yang diberikan dan premis teorema, mesin penalaran simbolik menurunkan proposisi baru
    • Jika solusi tidak ditemukan atau tidak ada lagi proposisi baru yang bisa dibuat, model bahasa menambahkan satu komponen bantu yang kemungkinan berguna
    • Komponen yang ditambahkan membuka jalur baru bagi mesin penalaran, dan proses ini diulang sampai solusi ditemukan
  • Pada soal nomor 3 Olimpiade Matematika Internasional 2015, solusi AlphaGeometry terdiri dari 109 langkah logis

Pembuatan 100 juta data sintetis

  • Geometri berbasis pada pemahaman ruang, jarak, bentuk, dan posisi relatif, serta menjadi fondasi berbagai bidang seperti seni, arsitektur, dan teknik
  • Metode pembuatan data sintetis AlphaGeometry meniru secara masif proses manusia mengamati bangun dan menggunakan pengetahuan yang ada untuk menemukan sifat serta relasi geometri baru
  • Sistem ini menghasilkan 1 miliar bangun acak dengan komputasi yang sangat diparalelkan
    • Menurunkan secara menyeluruh semua relasi antara titik dan garis pada tiap bangun
    • Menemukan semua pembuktian yang terkandung dalam tiap bangun
    • Melacak mundur komponen tambahan apa yang diperlukan untuk mencapai pembuktian tersebut
  • Proses ini disebut penalaran simbolik dan traceback (symbolic deduction and traceback)
  • Kumpulan data raksasa difilter untuk mengecualikan contoh yang mirip, sehingga akhirnya menjadi 100 juta contoh pelatihan unik dengan tingkat kesulitan beragam
    • 9 juta di antaranya adalah kasus yang menambahkan komponen bantu
    • Model bahasa mempelajari banyak contoh ketika konstruksi bantu mengarah ke pembuktian, sehingga dapat mengusulkan konstruksi baru juga pada soal olimpiade

Kemampuan verifikasi dan batas penerapan

  • Semua solusi soal olimpiade yang diberikan AlphaGeometry diperiksa dan diverifikasi dengan komputer
  • Hasilnya dibandingkan dengan metode AI sebelumnya dan performa manusia di olimpiade
  • Evan Chen, pelatih matematika sekaligus mantan peraih medali emas olimpiade, mengevaluasi sebagian solusi
    • Keluaran AlphaGeometry dapat diverifikasi dan rapi
    • Solusi AI untuk soal kompetisi berbasis pembuktian sebelumnya kadang benar dan kadang salah, sehingga bisa memerlukan pemeriksaan manusia
    • Solusi AlphaGeometry memiliki struktur yang dapat diverifikasi mesin sekaligus dapat dibaca manusia
    • Alih-alih memaksakan perhitungan aljabar masif dengan sistem koordinat, ia menggunakan aturan geometri klasik seperti sudut dan segitiga sebangun layaknya siswa
  • Satu edisi IMO terdiri dari 6 soal, dan biasanya hanya 2 di antaranya yang berfokus pada geometri
    • Karena itu, AlphaGeometry hanya dapat diterapkan pada sekitar sepertiga soal dalam satu edisi
    • Meski begitu, ini menjadi model AI pertama yang, hanya dengan kemampuan geometrinya, dapat melewati standar medali perunggu IMO tahun 2000 dan 2015

Ekspansi menuju AI penalaran matematika

  • AlphaGeometry menunjukkan bahwa kemampuan AI untuk bernalar secara logis serta menemukan dan memverifikasi pengetahuan baru makin meningkat
  • Pemecahan soal geometri tingkat olimpiade adalah tonggak penting menuju penalaran matematika yang lebih dalam dan sistem AI serbaguna yang lebih maju
  • Pendekatan melatih AI dari nol dengan data sintetis berskala besar dapat memengaruhi cara penemuan pengetahuan baru dalam sains dan AI, melampaui matematika
  • AlphaGeometry berada di atas alur kerja AI penalaran matematika dari Google DeepMind dan Google Research
  • Tujuan jangka panjangnya adalah membuat sistem AI yang dapat melakukan generalisasi di berbagai bidang matematika, mengembangkan pemecahan masalah dan penalaran canggih yang dibutuhkan sistem AI serbaguna, serta memperluas batas pengetahuan manusia

Bacaan terkait

1 komentar

 
GN⁺ 2024-01-18
Pendapat di Hacker News

  • Sebagai orang yang pernah menjadi pembuat soal untuk kompetisi seperti IMO, saya membaca makalah ini dengan sangat tertarik. Di saat yang sama, menurut saya topik pertama yang pasti runtuh oleh AI—yakni indeks pengetahuan yang cerdas dan indeks cara bernalar—memang adalah geometri
    Di antara topik olimpiade matematika, soal geometri pada umumnya paling “mekanis”. Jika sebuah soal bisa direpresentasikan dalam koordinat, misalnya koordinat XY atau bidang kompleks, maka muncul sekumpulan langkah terbatas yang bisa dipakai komputer untuk menemukan solusi. Tentu saja, di arena IMO, batas waktu dan kesalahan manusia membuatnya tidak praktis. Dulu, saya sering memverifikasi pembuktian soal geometri dan konjektur yang saya buat dengan WolframAlpha menggunakan cara seperti ini
    Aljabar, terutama pertidaksamaan, juga mirip; sering kali jawabannya keluar jika komputasi yang kuat dipaksakan
    Bidang tempat saya ingin melihat sistem cerdas benar-benar berkembang adalah teori bilangan dan kombinatorika. Ruang pencariannya jauh lebih kompleks, dan sering kali menuntut pembuktian bahwa sesuatu itu mustahil. Masalah-masalah seperti ini sulit diselesaikan dengan komputasi brute-force

    • Dari sudut pandang orang yang mengerjakan soal-soal itu, pertama-tama terima kasih. Meski sudah puluhan tahun sejak lulus SMA, saya masih sesekali menikmatinya
      Saya setuju bahwa geometri akan menjadi yang pertama. Dari yang saya lihat di sini, ini bukan “brute force” dalam arti bergantung pada geometri aljabar, vektor, atau solusi bilangan kompleks, tetapi lebih mendekati pencarian brute-force dalam arti menyisir konstruksi bantu yang “menarik”
      Geometri selalu menjadi mata pelajaran terburuk saya, tetapi saya merasa jika konstruksi yang tepat diberikan, soalnya menjadi jauh lebih mudah. Hanya saja saya tidak pernah menguasai intuisi untuk cepat memikirkan konstruksi seperti itu. AI ini juga tampaknya tidak memiliki intuisi semacam itu, tetapi bisa memuntahkannya jauh lebih cepat. Kandidat yang bisa dibuat seperti garis tegak lurus, garis sejajar, dan garis bagi pada akhirnya terbatas, dan dapat dievaluasi cukup mekanis dengan membentangkan semua sudut dan rasio atau mencoba pangkat titik
      Sangat mengesankan, tetapi dalam arti “engine vs AI”, ini terlihat seperti DeepMind:Kasparov::AlphaGeo:Terry Tao
      Saya setuju bahwa aljabar kemungkinan besar berikutnya. Seperti geometri, biasanya cukup menemukan satu, dua, atau tiga substitusi cerdik, dan pilihannya terbatas
      Sebagian soal kombinatorika juga bisa cocok dengan strategi pencarian ini. Misalnya soal yang menghitung objek yang sama dengan dua cara. Namun itu adalah jembatan yang lebih jauh, dan hanya bisa menangkap sebagian dari keseluruhan soal
      Teori bilangan sepertinya akan menjadi batas terakhir sebelum mencapai skor penuh 42
    • Saya suka sikap yang memandang perkembangan seperti ini secara positif. Saya penasaran apakah Anda merasa kehilangan karena ada kemungkinan kemampuan yang sangat hebat dalam matematika bisa segera dikejar oleh mesin. Atau apakah Anda melihat hal seperti itu tidak mungkin terjadi dalam waktu dekat?
    • Saya penasaran bagaimana Anda bisa masuk ke posisi pembuat soal seperti itu. Apakah ada semacam proses pendaftaran?
      Setelah memverifikasi bahwa soal bisa diselesaikan, saya juga penasaran bagaimana memilih soal tertentu yang masuk ke set soal akhir. Apakah lewat voting, atau metode evaluasi lain?
    • Awalnya saya kira pertidaksamaan tiga variabel akan runtuh lebih dulu. Karena ambiguitas tentang apa yang dianggap sebagai pembuktian lebih sedikit. Namun saya tidak tahu bahwa soal-soal di bagian belakang sudah diselesaikan pada tahun 2000 (http://www.mmrc.iss.ac.cn/~xgao/paper/jar-gdbase.pdf)
      Seseorang seharusnya membuat geometri sintetis menjadi game petualangan. Bisa memakai bahasa penulisan bukti yang lebih sederhana daripada Lean, dan juga bisa dibuat menarik secara visual

  • Jika saya memang membaca makalahnya dengan benar, ini tampak seperti pekerjaan yang sungguhan. Jauh lebih sahih daripada makalah matematika AI bulan lalu ketika DeepMind keliru mempromosikan bahwa mereka telah memecahkan masalah riset matematika terbuka. Meski begitu, cukup mencolok betapa strukturnya berbeda dari apa yang biasanya dibayangkan sebagai penalaran/kecerdasan otomatis
    Pemahaman saya, mereka melatih Transformer dengan jutaan teorema geometri elementer dan menggunakannya untuk melakukan pencarian brute force atas pembuktian. Karena konteksnya geometri elementer, strukturnya niscaya elementer, dan benar/salah dapat ditentukan secara simbolik dengan mudah. Saya mengira caranya adalah, jika pencarian brute force gagal, mereka menambahkan konstruksi geometri bantu secara acak, seperti menambahkan titik tengah, lalu melihat apakah pencarian bisa dilakukan dengan bahan tambahan itu
    Edit: seperti koreksi Imnimo, ternyata saya memahaminya terbalik. Pencarian brute force adalah pencarian brute force murni, sedangkan Transformer dipakai untuk memprediksi konstruksi bantu apa yang perlu ditambahkan
    Selain itu, meski tidak ada di tulisan blognya, kalimat soal sebenarnya juga harus diubah/diadaptasi. Misalnya kalimat asli seperti “misalkan tinggi-tinggi segitiga ABC adalah AH1, BH2, CH3...” diubah menjadi daftar definisi yang jauh lebih eksplisit seperti “Misalkan ABC adalah segitiga. Definisikan titik I sehingga AI adalah garis bagi sudut BAC dan CI adalah garis bagi sudut ACB...”, dan pada akhirnya menjadi bentuk “buktikan T1I=IZ”

    • Penjelasan ini sepertinya agak tidak tepat. Pencarian brute force dilakukan oleh solver simbolik, bukan Transformer. Ketika tidak ada penalaran baru yang keluar lagi, Transformer diminta mengusulkan konstruksi bantu yang mungkin; bukan ditambahkan secara acak
    • Saya tidak mengerti mengapa ini dianggap jauh dari gagasan umum tentang penalaran/kecerdasan otomatis. Penalaran pada dasarnya adalah masalah pencarian
      Proses yang dijelaskan persis sama dengan proses yang dipakai manusia. Menebak sesuatu yang tampak berguna, lalu menyelesaikan detailnya secara mekanis. Jika buntu, membuat tebakan lain. Pada akhirnya mirip dengan menelusuri sebuah pohon
      Orang-orang sudah memahami proses ini pada 1955, dan bahkan membuat prototipe berjalan yang bisa membuktikan teorema: https://en.wikipedia.org/wiki/Logic_Theorist Kuncinya terletak pada penggunaan heuristik yang baik. Jaringan saraf masuk akal di sini karena dapat mengekstrak heuristik dari data
      Saya penasaran apa yang Anda bayangkan sebagai gagasan umum “penalaran otomatis”. Apakah semacam perangkat ajaib yang menyelesaikan masalah apa pun dalam satu pass linear?
    • Cara “jika pencarian brute force gagal, tambahkan konstruksi geometri bantu seperti titik tengah, lalu lihat apakah pencarian bisa berjalan dengan bahan tambahan itu” persis seperti geometri yang saya pelajari di sekolah, dan saya sangat membencinya
      Baru setelah masuk jurusan matematika di universitas saya belajar cara yang benar dan bisa menikmatinya
    • Memakai LLM untuk peran menggambar garis bantu itu terlalu tidak efisien. Sulit membayangkan mengerahkan begitu banyak mesin hanya untuk menyelesaikan soal IMO sederhana
      Bidang ini masih tahap awal, dan tampaknya masih banyak pekerjaan yang belum selesai. Bagian pencarian seharusnya diganti dengan jaringan saraf kecil, sedangkan bagian penalarannya tidak sulit dan sepertinya tidak perlu banyak diperbaiki
      Sekarang sudah waktunya meningkatkan kinerja lewat self-play. Dalam soal geometri bidang, kesimpulan yang harus dibuktikan bisa dipandang sebagai satu titik pada gambar, sementara kondisi sebagai titik lain; dua pemain dapat bergerak semaksimal mungkin ke arah satu sama lain dan berbagi data. Dalam proses ini, kontribusi masing-masing pemain dapat dianalogikan dengan perhitungan menang-kalah dalam Go untuk dipakai meningkatkan kinerja

  • Model khusus ini tampaknya tidak bisa digeneralisasi, tetapi pendekatan neuro-simbolik terlihat sangat menjanjikan
    Ini adalah cara menghubungkan alat “Sistem 1” yang semakin kuat, yang merupakan sebagian besar machine learning saat ini, dengan alat “Sistem 2” yang terstruktur seperti pembuatan bukti logis. Sistem 2 dapat menyusun rencana dan memeriksa kebenaran atau nilai dari output
    Sistem 2 berjalan sampai buntu; ketika buntu, Sistem 1 memberikan tebakan intuitif tentang bagian ruang keadaan mana yang sebaiknya diperiksa berikutnya
    Di sini mereka memanfaatkan fakta bahwa komputer dapat menghasilkan pembuktian untuk membuat dataset 100 juta bukti, sehingga memungkinkan pembelajaran self-supervised yang dapat diskalakan. Ranah simbolik tampaknya memiliki bentuk yang memungkinkan pembuatan data seperti ini dengan baik. Nilai tiap instance mungkin rendah, tetapi jika dikumpulkan, bisa memungkinkan pralatih yang berguna
    Jika unsur-unsur ini digabungkan, pendekatan ini bisa melangkah cukup jauh
    Tonggak utamanya adalah keluar dari kebutuhan untuk bergantung pada ranah formal/simbolik tertentu, dan membuat sistem pralatih yang dapat menggeneralisasi teknik yang dipelajari dari ranah itu

    • Tidak perlu menyelesaikan semuanya sekaligus. Pendekatan ini berpotensi mengubah matematika dan pemrograman. Sebab verifikasi formal bisa berpindah dari alat ceruk yang hanya dipakai sebagian menjadi bagian dari kotak alat umum semua praktisi
      Selain itu, di dalam ranah tempatnya dapat diterapkan, pendekatan ini sepenuhnya menyelesaikan salah satu masalah mendasar yang dalam arus AI saat ini disebut “halusinasi”. Namun solusi itu dimungkinkan karena ada sistem non-AI yang membuktikan kebenaran
      Dalam gambaran besar, pendekatan ini tidak sepenuhnya baru. Dalam biokimia, sudah dipakai cara mencari molekul kandidat dengan AI lalu memverifikasinya lewat eksperimen fisik
      AI permainan kombinatorial juga sudah lama memakai AI sebagai masukan untuk pencarian Monte Carlo gaya lama
    • Ini tampak seperti kemungkinan terdekat untuk mencapai suatu bentuk kecerdasan umum buatan

  • Saya menghargai bahwa mereka merilis kode dan bobot bersama makalahnya. Sejauh yang saya ingat, ini pertama kalinya makalah DeepMind terkenal merilis kode inferensi yang bisa dijalankan beserta checkpoint. Saya terbuka untuk dikoreksi jika ada contoh yang lebih awal
    Saya belum melihat set pelatihan yang dirilis atau contoh kode pelatihan, tetapi tetap saja ini kemajuan yang baik karena mereka menyediakan sesuatu yang bisa dibangun di atasnya oleh peneliti lain. Pada akhirnya, itu juga tujuan makalah akademik

    • Sayang dataset-nya juga tidak ada. Mereka mengatakan membuat 100 juta contoh sintetis; apakah contoh-contoh ini dibuat dengan AlphaGeometry? Di mana kode penyaringan dan input awal untuk membuat data sintetis ini?
      Kalau saya tidak salah, apakah mereka memakai model t5? Setidaknya tampaknya memakai kosakata SentencePiece t5
      Saya juga penasaran berapa banyak waktu GPU yang dipakai untuk melatih model ini, dan parameter pelatihan apa yang digunakan
      Jangan salah paham. Sistem ini memikat, dan menunjukkan seperti apa rekayasa terapan seharusnya. Hanya saja saya ingin tahu lebih banyak tentang detail pelatihan, data awal, dan cara pembuatan data sintetisnya

  • Saya sangat penasaran seberapa sering model bahasa menghasilkan konstruksi bantu yang berguna. Jelas lebih baik daripada acak, tetapi saya tidak tahu apakah ia melempar ribuan konstruksi sampai menemukan yang bagus, atau apakah ia memberi usulan berguna dengan rasio yang mirip pakar manusia
    Dalam makalahnya disebutkan: “Karena proses decoding model bahasa mengembalikan k sekuens berbeda yang menjelaskan k alternatif konstruksi bantu, kami menggunakan skor tiap beam sebagai fungsi nilai untuk melakukan beam search atas k opsi ini. Pengaturan ini sangat mudah diparalelkan antar-beam sehingga menjadi jauh lebih cepat jika ada sumber daya komputasi paralel. Dalam eksperimen, kami menggunakan ukuran beam k=512, jumlah iterasi maksimum 16, dan faktor percabangan tiap node, yaitu ukuran batch decoding, 32”
    Namun saya belum sepenuhnya paham bagaimana 512 dan 16 dikonversi menjadi total jumlah konstruksi yang diusulkan. Mereka juga mengatakan bahwa meski ukuran beam dan iterasi maksimum dihilangkan, performanya hanya turun sampai tingkat tertentu. Apakah ini berarti model tersebut sebenarnya cukup baik menaruh konstruksi yang berguna di peringkat atas, dan ribuan konstruksi hanya dibutuhkan untuk soal yang paling sulit?

    • Dugaan pribadi saya, bagian ini berbenturan keras dengan keterbatasan bahasa dan analogi manusia-mesin
      Namun kalau dicoba diringkas, angkanya 262.144, tetapi jangan diterima secara harfiah
      Keluaran fungsi decoding adalah token, kira-kira sekitar 3/4 kata, tetapi anggap saja 1 kata
      Jumlah token yang dipertimbangkan per satu token keluaran adalah beam_size * branching_factor * max_iterations = 512 * 32 * 16 = 262.144
      Kita bisa menghitung jumlah kata dalam contoh solusi: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
      Total jumlah token solusi adalah 2289, dan total token yang dipertimbangkan adalah 262.144 * 2289 = 600.047.616
      Jika dengan perhitungan agak dipaksakan “jumlah solusi yang dipertimbangkan” didefinisikan sebagai total token yang dipertimbangkan / total token solusi, hasilnya 262.144. Nilai yang sama dengan jumlah token yang dilihat di tiap langkah iterasi, jadi masih masuk akal

  • Menarik bahwa Transformer yang digunakan berukuran kecil. Menurut makalahnya, model dilatih dengan pengaturan default dari pustaka Meliad, memiliki 12 layer, dimensi embedding 1.024, 8 attention head, serta dense layer antar-attention berdimensi 4.096 yang memakai aktivasi ReLU
    Jika lapisan embedding untuk input dan output head dikecualikan, keseluruhan Transformer memiliki 151 juta parameter. Tokenizer khusus dilatih dalam mode ‘word’ SentencePiece, dengan ukuran kosakata 757. Panjang konteks maksimum dibatasi 1.024 token dan memakai embedding posisi relatif gaya T5. Karena lebih dari 90% sekuens panjangnya di bawah 200, mereka juga memakai sequence packing

    • Sulit menyebutnya kecil. Di luar bidang LLM, itu ukuran yang cukup normal. Misalnya setara dengan model bahasa, model terjemahan, atau model akustik berukuran umum. Sebagian orang bahkan akan menyebut ukuran ini besar
    • Hasil ini mengisyaratkan bahwa, asalkan bisa diformalkan dengan baik, mungkin masih ada low-hanging fruit lain di hard science yang cocok digarap Transformer. Tampaknya kasus ini bukan soal skala perluasan

  • Hal yang benar-benar baru bagi saya adalah bahwa sistem terbaik sebelumnya pun bisa menyelesaikan 10 soal seperti ini. Saya pernah mendengar ada algoritma keputusan untuk soal geometri bidang, tetapi tidak tahu bahwa algoritmanya praktis. Setelah dicari, referensi yang muncul adalah http://www.mmrc.iss.ac.cn/~xgao/paper/book-area.pdf

    • Benar. Dan bagian non-jaringan saraf dari AlphaGeometry, yaitu komponen pemrosesan simbolik dan aljabar linear saja, juga sudah bisa melampaui performa terbaik sebelumnya. Cukup banyak pekerjaan di sini juga masuk ke komponen non-neural
    • Menarik, tetapi kalau memaksakan perhitungan koordinat barycentric dengan rumus-rumus dalam buku Evan Chen, sepertinya laptop modern pun bisa menyelesaikan sekitar 30% soal IMO. Mengingat sebagian besarnya adalah soal segitiga, itu masuk akal

  • Saya tadinya siap skeptis karena hasil semacam ini biasanya dikatakan “tidak seperti pembuktian manusia”, tetapi saya berubah pikiran setelah melihat Evan Chen mengatakan bahwa buktinya benar-benar rapi dan bisa dibaca manusia
    Evan Chen adalah tokoh terkenal di komunitas matematika olimpiade dan juga penulis buku geometri olimpiade yang terkenal[1], jadi kali ini saya harus mengakui bahwa mesin benar-benar telah menaklukkan sebagian soal IMO
    [1]: https://web.evanchen.cc/geombook.html

    • Namun dalam pembuktian lengkap di materi tambahan[1], saya merasa ada kesalahan pada bukti IMO P3 Fig1.f dan Step 26. Dikatakan bahwa ∠GMD = ∠GO2D, tetapi menurut saya itu salah dan seharusnya ∠GMD + ∠GO2D = π. Saya mencoba mengikuti logikanya, tetapi tidak bisa menafsirkan Step 25. Saya sempat mengira langkah ini halusinasi
      Meski begitu, gagasan bahwa O2 berada di lingkaran sembilan titik memang benar
      Edit: saya tarik kembali ucapan saya. Sepertinya mereka memakai sudut berarah[2], dan kalau begitu kalimat itu benar
      [1]: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
      [2]: https://web.evanchen.cc/handouts/Directed-Angles/Directed-An...

  • Terkait hal ini, https://www.nytimes.com/2024/01/17/science/ai-computers-math... juga layak dibaca
    Ini berasal dari https://news.ycombinator.com/item?id=39030186, dan thread tersebut akan digabungkan ke sini

  • Terkait: https://aimoprize.com/
    Ini adalah hadiah 10 juta dolar untuk model yang berkinerja baik di IMO