AI DeepMind selesaikan soal Olimpiade Matematika Internasional di tingkat medali perak

(deepmind.google)

3 poin oleh GN⁺ 2024-07-26 | 3 komentar | Bagikan ke WhatsApp

Pada IMO 2024, tolok ukur utama untuk penalaran matematika tingkat tinggi, AlphaProof dan AlphaGeometry 2 dari Google DeepMind berhasil menyelesaikan 4 dari 6 soal, mencapai performa setara medali perak untuk pertama kalinya bagi AI
Dari total 42 poin, sistem meraih 28 poin, dan semua soal yang berhasil diselesaikan mendapat nilai sempurna; hasil ini hanya terpaut 1 poin dari ambang medali emas IMO 2024 yaitu 29 poin
Penilaian dilakukan oleh para matematikawan sesuai aturan penskoran IMO; AlphaProof menangani aljabar dan teori bilangan, sementara AlphaGeometry 2 menangani geometri, menggabungkan dua pendekatan penalaran yang berbeda
Soal-soal terlebih dahulu diterjemahkan secara manual ke dalam bahasa matematika formal; sementara peserta manusia mendapat dua sesi masing-masing 4,5 jam, sistem ini menyelesaikan satu soal dalam hitungan menit dan soal lain memerlukan hingga 3 hari
Hasil ini menunjukkan bahwa AI matematika telah melampaui sekadar perhitungan dan mulai mendekati pencarian serta verifikasi pembuktian, meski input yang harus diformalkan dan waktu penyelesaian yang panjang masih menjadi keterbatasan penting

Hasil setara medali perak di IMO 2024

Google DeepMind memperkenalkan sistem penalaran matematika AlphaProof dan versi peningkatan dari sistem pemecah soal geometri AlphaGeometry 2
Kedua sistem menyelesaikan 4 dari 6 soal pada International Mathematical Olympiad 2024
- AlphaProof: menyelesaikan 2 soal aljabar dan 1 soal teori bilangan
- AlphaGeometry 2: membuktikan 1 soal geometri
- 2 soal kombinatorika tidak berhasil diselesaikan
Setiap soal bernilai maksimum 7 poin, sehingga total nilai adalah 42 poin
- Sistem mendapat nilai sempurna pada keempat soal yang berhasil diselesaikan dan meraih 28 poin
- Ini setara dengan bagian atas rentang medali perak IMO 2024
- Ambang medali emas IMO 2024 adalah 29 poin, dan dalam kompetisi resmi 58 dari 609 peserta mencapai rentang medali emas
Ini adalah kasus pertama AI mencetak hasil setara peraih medali perak di IMO

Metode evaluasi dan kondisi penyelesaian

Soal yang digunakan adalah soal kompetisi yang disediakan oleh penyelenggara IMO
Jawaban dinilai sesuai aturan pemberian skor IMO
- Penilai adalah Prof Sir Timothy Gowers, peraih medali emas IMO sekaligus pemenang Fields Medal, serta Dr Joseph Myers, peraih 2 medali emas IMO dan ketua IMO 2024 Problem Selection Committee
Agar sistem dapat memahami soal, semua soal terlebih dahulu diterjemahkan secara manual ke dalam bahasa matematika formal
Dalam kompetisi resmi, siswa mengumpulkan jawaban dalam dua sesi masing-masing 4,5 jam
- Sistem AI menyelesaikan satu soal dalam beberapa menit, sementara soal lain membutuhkan hingga 3 hari
Di antara soal yang diselesaikan AlphaProof terdapat soal tersulit pada IMO 2024 yang hanya berhasil diselesaikan oleh 5 peserta

AlphaProof: penalaran formal berbasis Lean

AlphaProof adalah sistem yang dilatih untuk membuktikan pernyataan matematika dalam bahasa formal Lean
Sistem ini menggabungkan model bahasa pralatih dan algoritme reinforcement learning AlphaZero
- AlphaZero adalah algoritme yang digunakan untuk mempelajari catur, shogi, dan Go secara mandiri
Dengan bahasa formal, verifikasi ketepatan pembuktian yang mencakup penalaran matematika menjadi dimungkinkan
Sebelumnya, data pembuktian formal yang ditulis manusia sangat terbatas, sehingga pemanfaatan bahasa formal dalam machine learning juga terbatas
Pendekatan berbasis bahasa alami dapat memanfaatkan jauh lebih banyak data, tetapi bisa menghasilkan langkah penalaran antara atau jawaban yang tampak meyakinkan namun salah
DeepMind melakukan fine-tuning pada model Gemini agar dapat secara otomatis menerjemahkan soal bahasa alami menjadi pernyataan formal, serta membangun pustaka soal formal dengan berbagai tingkat kesulitan
Saat menerima sebuah soal, AlphaProof menghasilkan kandidat solusi, lalu menelusuri langkah pembuktian yang mungkin di Lean untuk membuktikan atau membantahnya
- Pembuktian yang ditemukan dan diverifikasi digunakan untuk memperkuat model bahasa AlphaProof
- Proses berulang ini digunakan untuk meningkatkan kemampuan menyelesaikan soal yang lebih sulit
Dalam persiapan IMO, sistem ini belajar selama beberapa minggu dengan membuktikan atau membantah jutaan soal
- Bahkan selama kompetisi, diterapkan loop pembelajaran yang memperkuat pembuktian terhadap variasi soal yang dihasilkan sendiri untuk menemukan solusi lengkap

AlphaGeometry 2: diperluas ke soal geometri yang lebih sulit

AlphaGeometry 2 adalah versi yang sangat ditingkatkan dari AlphaGeometry
Sistem ini memiliki arsitektur hibrida neuro-simbolik yang menggabungkan jaringan saraf dan penalaran simbolik
- Model bahasanya berbasis Gemini
- Sistem ini dilatih dari awal menggunakan data sintetis dengan skala satu orde lebih besar dibanding versi sebelumnya
Berkat data yang lebih banyak dan model yang ditingkatkan, sistem ini dapat menangani soal geometri yang lebih sulit, termasuk pergerakan objek serta persamaan sudut, rasio, dan jarak
Mesin simbolik AlphaGeometry 2 bekerja puluhan kali lebih cepat daripada versi sebelumnya
Saat menerima soal baru, sistem ini menangani masalah yang lebih kompleks dengan memanfaatkan kombinasi tingkat lanjut dari pohon pencarian yang berbeda melalui mekanisme berbagi pengetahuan baru
Tingkat penyelesaian soal geometri IMO dalam 25 tahun terakhir: {b:83,53}
- Hingga sebelum kompetisi 2024, AlphaGeometry 2 dapat menyelesaikan 83% soal geometri IMO dalam 25 tahun terakhir
- Tingkat penyelesaian AlphaGeometry sebelumnya adalah 53%
Pada IMO 2024, sistem ini menyelesaikan Problem 4 dalam 19 detik setelah menerima input yang telah diformalkan

Penalaran bahasa alami dan pemanfaatan ke depan

Sebagai bagian dari pekerjaan untuk IMO, DeepMind juga menguji sistem penalaran bahasa alami berbasis Gemini dan riset terbaru
Sistem ini tidak memerlukan penerjemahan soal ke bahasa formal dan dapat digabungkan dengan sistem AI lain
Pendekatan ini juga diuji pada soal IMO 2024 dan hasilnya dinilai menjanjikan
Metodologi AlphaProof yang lebih teknis dipublikasikan dalam makalah Nature
DeepMind menargetkan masa depan di mana matematikawan mengeksplorasi hipotesis bersama alat AI, mencoba pendekatan baru pada masalah lama, dan menyelesaikan bagian pembuktian yang memakan waktu dengan lebih cepat

3 komentar

chabulhwi 2024-07-26

Semakin banyak matematikawan yang berkontribusi pada pengembangan pustaka matematika formal, akan semakin mudah membuat AI matematika dengan kinerja tinggi. Setahu saya, saat ini ada 3 orang Korea yang sedang memindahkan teori matematika yang mereka formalkan sendiri ke dalam bahasa asisten pembuktian Lean ke pustaka matematika Lean, Mathlib.

Tahun lalu saya ikut sedikit berpartisipasi dalam pekerjaan memindahkan Mathlib dari Lean 3 ke Lean 4, dan tahun ini saya membuktikan satu teorema yang belum terselesaikan di pustaka baterai Lean 4.

GN⁺ 2024-07-26

Pendapat di Hacker News

Saya sangat antusias dengan pengumuman ini, tetapi belum jelas seberapa banyak pekerjaan yang ditanggung oleh kalimat “pertama-tama masalah diterjemahkan secara manual oleh manusia ke dalam bahasa matematika formal agar dapat dipahami sistem”
Semua soal non-geometri berbentuk “carilah semua X yang ...”, dan pernyataan teoremanya berbentuk “tunjukkan bahwa himpunan semua X adalah {foo}”
Dari solusi yang bisa diunduh di https://storage.googleapis.com/deepmind-media/DeepMind.com/B... saja, sulit mengetahui apakah pada tahap penerjemahan manusia yang menentukan {foo}, atau komputer yang menemukannya. Saya ingin percaya komputer yang menemukannya, tetapi tidak menemukan dasar untuk memastikannya
- Komputerlah yang menemukan jawabannya sendiri. Artinya, pada P1 ia menemukan bilangan bulat genap, pada P2 {1,1}, dan pada P6 2, serta dalam tiap kasus juga menyajikan pembuktian Lean
- Secara umum, tahap penerjemahan itu jauh lebih mudah daripada tahap pembuktian. Masalah pada penerjemahan otomatis adalah hasil terjemahannya bisa salah
  Manusia pun sering mengalami hal seperti ini saat menangani teknik formal secara langsung, jadi para peneliti mungkin menilai bahwa pada akhirnya semua terjemahan harus diaudit, baik memakai LLM maupun alat lain
- Di halaman yang ditautkan tertulis bahwa “pernyataan soal diformalisasi oleh manusia ke dalam Lean, tetapi jawaban di dalam pernyataan soal dihasilkan dan diformalisasi oleh agen”
  Namun tidak jelas bentuk awal apa yang diberikan kepada agen sehingga tahap ini dimungkinkan
- Menarik bahwa ada alat formalisasi yang digunakan untuk membuat data pelatihan, tetapi tidak dipakai di sini. Sepertinya belum cukup dapat dipercaya
- Kedengarannya seperti penjelasan bahwa “ketika sebuah soal diberikan, AlphaProof menghasilkan kandidat solusi, lalu menelusuri langkah-langkah pembuktian yang mungkin di Lean untuk membuktikan atau membantahnya”
  Jadi apa pun bentuk “soal” yang diterima AlphaProof, dan bagaimanapun “carilah semua X yang ...” diformalisasi, ia tampaknya menghasilkan teorema-teorema kandidat, mungkin dalam Lean. Misalnya, himpunannya bisa berbentuk {n: P(n)} untuk suatu rumus P. Setelah itu ia menelusuri pembuktiannya
  Jika bukan AlphaProof yang menemukan {foo}, melainkan itu diberikan, klaim bahwa ia memecahkan soal akan terasa cukup mengada-ada. Meski begitu, hasil ini tetap sangat membuat saya antusias
Ini jelas mengesankan, tetapi saat IMO disebut, perlu ada catatan kehati-hatian. Medali diberikan kepada 50% peserta, yaitu siswa SMA, dengan rasio emas:perak:perunggu 1:2:3, sehingga peraih emas dan perak berada di 25% teratas dari seluruh peserta
Jadi ungkapannya menjadi “AI menyelesaikan soal IMO lebih baik daripada 75% siswa”, dan sebenarnya ini pun bisa lebih mengesankan
Namun kondisi “satu soal dalam beberapa menit, dan masing-masing soal lainnya hingga 3 hari” berbeda dari 9 jam yang diberikan kepada siswa, sehingga sulit dianggap sebagai perbandingan yang sungguh setara. Jika siswa juga diberi hingga 15 hari alih-alih 9 jam, kemungkinan lebih banyak yang akan menyamai atau melampaui skor ini
Dalam praktiknya, AI hanya menyelesaikan satu soal dalam 9 jam yang diberikan kepada siswa, jadi besar kemungkinan masih jauh dari zona medali. Rasanya tidak perlu mengaburkan hasil yang mengesankan ini dengan membandingkan apel dan jeruk
Secara lebih objektif, cukup laporkan bahwa meski memakan waktu lebih lama, ia menyelesaikan X% dari seluruh soal atau mendapat X poin dari total N
- Saya pernah bertemu peserta IMO, dan mereka benar-benar luar biasa cerdas. Sebelum bertemu kelompok seperti itu, saya tidak pernah membayangkan manusia bisa sepintar itu. Jadi ini sebaiknya dilihat sebagai mendekati 25% teratas dari 0,01% seluruh siswa SMA
  Di sini, waktu bukanlah sumbu yang begitu menarik. Manusia tidak memakai CPU seperti klaster GPU raksasa. Dikotomi yang lebih menarik adalah “dengan sumber daya yang cukup, apakah ia bisa mencapai solusi”, dan jawaban untuk GPT/Claude jelas tidak
- Pernyataan “medali diberikan kepada 50% siswa SMA peserta” bisa membingungkan; siswa SMA yang dimaksud di sini bukan sampel siswa SMA biasa. Setahu saya, tiap negara mengirim tim perwakilan yang terdiri dari sekitar 6 orang jagoan terkuat dalam menyelesaikan soal olimpiade
- Secara pribadi, meski ini bukan posisi Google, saya rasa satu-satunya alasan mereka tidak mendapat medali emas tahun ini adalah kurang beruntung dalam pilihan soal dan tidak membidik nilai parsial pada P3/P5
  Mereka sangat dekat dengan batas nilai, dan biasanya sedikit kemajuan saja bisa mendapat 1 poin. Namun karena alasan teknis, pemberitaan bahwa mereka mendapat emas mungkin tidak akan bagus, jadi tampaknya mereka puas dengan perak yang tidak kontroversial
- Perbedaan utama antara memberi manusia lebih banyak waktu dan memberi program komputer lebih banyak waktu adalah bahwa secara historis kita jauh lebih berhasil membuat yang terakhir berjalan lebih cepat
- Sebagian besar riset DeepMind adalah pusat biaya bagi perusahaan. Siaran pers seperti ini membantu membenarkan investasi berkelanjutan kepada investor dan publik
Ini benar-benar nyata. AlphaGeometry sebelumnya memecahkan kumpulan masalah yang sangat terbatas dengan banyak pencarian brute-force
Metode kali ini jauh lebih luas, dan saya pikir akan berdampak besar pada cara bermatematika. Ini benar-benar mewujudkan pipeline mandiri yang berangkat dari matematika bahasa alami menuju matematika yang diformalisasi, lalu di sana bisa melatih baik formalisasi maupun pembuktian
Pada prinsipnya, pipeline ini juga bisa belajar membangun teori dasar seperti membuat definisi bantu dan lema. Ini mendekati cawan suci asisten pembuktian, dan menurut saya akan memungkinkan sebagian besar matematika yang kita buat secara alami untuk diformalisasi. Manusia akan bekerja dengan cara memperketat secara rigor setelahnya, sementara mesin membantu mengisi detailnya
- Setuju. Ini kemajuan besar. Soal geometri termasuk kategori berbeda karena bisa diterjemahkan menjadi sistem persamaan polinomial lalu diselesaikan dengan algoritma aljabar komputer yang sudah dikenal
  Sebaliknya, formalisasi terbuka seperti ini adalah bidang yang kemajuannya sangat lambat dan bertahap. Lima tahun lalu saya bekerja di bidang yang berdekatan, dan hasil ini bisa dibilang berada pada tingkat yang tidak mungkin dicapai dengan teknik penalaran otomatis tradisional
  Pembuktian teorema otomatis yang sebenarnya jauh lebih berguna daripada sekadar untuk matematika murni. Misalnya, kita bisa menuliskan semantik aksiomatik dari sebuah bahasa pemrograman kecil di Lean dan mengajukan pertanyaan seperti “tunjukkan bahwa ada program yang memenuhi spesifikasi ini”
  Jika pendekatan ini bisa diskalakan, ini akan menjadi lebih penting daripada aplikasi machine learning mana pun yang muncul dalam beberapa tahun terakhir
- Jangan meremehkan pencarian. Mungkin tampak seperti brute-force, tetapi pencarian telah melampaui level manusia dalam Go dan mencapai level medali perak IMO
  Evolusi yang menciptakan kita juga merupakan pencarian yang bekerja lewat percobaan brute-force dalam skala luar biasa, dan penelitian dalam metode ilmiah pun pada dasarnya adalah pencarian
- Sudah ada orang-orang yang mengerjakan bidang ini
  https://leandojo.org/
  https://machine-learning-for-theorem-proving.github.io/
  https://www.youtube.com/watch?v=P5ew0BrRm_I
  https://paperswithcode.com/task/automated-theorem-proving
  https://old.reddit.com/r/math/comments/11mb9lx/future_of_aut...
  https://github.com/RiccardoBiosas/LeanGPT
- Sistem seperti ini sepertinya akan jauh lebih berguna di luar riset matematika
  Untuk melakukan pekerjaan yang bermanfaat, kita tidak perlu membuktikan masalah yang sangat sulit. Sering kali membuktikan hal-hal sederhana saja sudah cukup. Jika kita meminta model bahasa menyelesaikan tugas, merapikan item, menjadwalkan sesuatu, menulis kode untuk melakukan X, dan sebagainya, hasilnya sulit langsung dipercaya. Namun jika sistem bisa menerjemahkan sebagian masalah ke dalam logika dan menemukan solusinya, hasilnya menjadi jauh lebih dapat dipercaya
- Tidak. Ini hanya mirip dengan membuatnya bisa memakai mesin pencari untuk menemukan solusi, tidak lebih dari itu
Poin utamanya agak tertutupi: mereka memakai Lean
Ini penting melampaui soal matematika. Membuat model machine learning bergulat dengan sistem pembuktian adalah cara bagus untuk menghindari omong kosong umum
Ke depannya saya berharap lebih banyak orang menulis tipe di Lean atau sistem serupa, dan memakainya sebagai cara yang jauh lebih baik untuk menulis prompt
- AlphaProof jelas luar biasa, tetapi di IMO komputer juga diberi keunggulan yang tidak dimiliki manusia. Tidak ada orang yang membuat basis Gröbner di kepala, tetapi polyrith cukup dengan mengetik delapan karakter. Saya juga melihat AlphaProof memakai nlinarith
- Menakjubkan. Saya baru saja hendak berkomentar bahwa kalau ini dihubungkan ke Lean, hasilnya akan luar biasa. Matematika tingkat tinggi tampaknya harus bergerak ke arah ini. Sebab pembuktian-pembuktian utama sudah menjadi begitu kompleks sehingga hampir tidak ada orang yang memahami seluruh bagiannya
  1. https://lean-lang.org/
- Dengan ini mereka akan membidik Hipotesis Riemann juga, hehe
Ada ringkasan singkat yang bagus dari Tim Gowers yang menjelaskan peringatan utama dan memberi konteks. Ia adalah peraih Medali Fields dan juga terlibat dalam pekerjaan ini: https://x.com/wtgowers/status/1816509803407040909
Itu benar, tetapi masuk ke tim perwakilan tiap negara sendiri sudah merupakan proses yang sangat berat. Olimpiade matematika regional, olimpiade matematika nasional, dan seterusnya—di setiap tahap penyaringannya brutal
Setelah itu ada pelatihan tambahan untuk kelompok elite ini, dan dalam beberapa kasus bisa ada seleksi tambahan lagi
Singkatnya, terpilih masuk tim IMO suatu negara saja sudah hal besar, dan meraih medali emas atau perak di dalamnya benar-benar prestasi luar biasa
- Beberapa negara mengeluarkan anak-anak ini dari sekolah sepanjang tahun agar mereka bisa fokus pada pelatihan IMO, dan bahkan menjamin mereka masuk universitas terbaik di negara tersebut
  Sumbernya adalah teman saya yang meraih medali perak IMO
Saya benar-benar iri pada orang-orang yang dibayar untuk melakukan pekerjaan ini. Kelihatannya sangat menyenangkan, dan mendorong level tercanggih seperti ini pasti terasa sangat memuaskan
- Belum tentu begitu. Ada banyak pekerjaan yang seharusnya sangat memuaskan tetapi berakhir sangat membosankan atau bahkan merugikan, dan sebaliknya ada juga pekerjaan yang dari luar tampak biasa saja tetapi ternyata benar-benar menarik
  Dalam kepuasan kerja, menurut saya lingkungan kerja lebih penting daripada topiknya. Sekalipun menangani topik yang mengubah dunia, kalau timnya berantakan, Anda akan melewati masa yang berat. Ada orang-orang yang punya bakat menyedot habis semua kesenangan, politik kantor ada di mana-mana, dan itu terutama berlaku untuk topik yang mengubah dunia
  Sebaliknya, bahkan topik yang tampak paling membosankan seperti memasukkan data pelanggan ke database pun bisa menjadi pengalaman terbaik jika ada tim yang baik, arsitektur yang dirancang dengan baik, serta waktu untuk eksperimen dan berbagi pengetahuan. Saya makin menghargai keindahan dari hal sederhana yang bekerja dengan baik. Hal seperti itu mungkin bahkan lebih langka daripada terobosan ilmiah
  Tentu saja lingkungan kerja yang hebat dan topik yang hebat bisa datang bersamaan, dan itu hampir seperti jackpot sehingga pantas membuat iri
- Saya bekerja di bidang ini, khususnya di sisi pretraining LLM. Tidak seglamor kelihatannya. Pekerjaannya mencakup menangani YAML raksasa dan menggunakan regex dalam skala besar. Tentu saja ini sedikit penyederhanaan
  Seharusnya saya merasa bersemangat dan bersyukur bisa melakukan pekerjaan seperti ini, tetapi tooling yang buruk banyak mengurangi kesenangan kerja
- Mungkin yang tepat bukan jealous, melainkan envious
- Yang terbaik yang bisa kita lakukan adalah terus mengikuti informasi terbaru dan mendukungnya
- Bukankah sekarang waktunya mengonfigurasi ulang YML 3.292.329 baris untuk K8s
  (/s)
Mesin sudah bermain catur lebih baik daripada manusia selama beberapa dekade
Namun tidak ada yang peduli. Semua orang sibuk menonton Magnus Carlsen
Karena kita manusia, kita tertarik pada apa yang dilakukan manusia lain. Kita tertarik pada mesin hanya sejauh mesin itu membantu kita
Prinsip ini juga meluas ke pekerjaan dan seni. Selama manusia ada, akan selalu ada tempat bagi manusia di bidang-bidang seperti ini
- Seberapa pun AI lebih baik dalam catur dan seni, manusia akan tetap menikmatinya. Demikian pula, kemungkinan akan tetap ada orang yang mempelajari matematika sebagai hobi
  Namun saya sangat meragukan apakah dalam waktu dekat masih akan ada matematikawan yang mengumumkan kemajuan matematika baru yang sebagian besar atau seluruhnya belum ditemukan oleh AI. Manusia mungkin bisa mendapat kredit atas pembuktian karena mengajukan pertanyaan awal, tetapi hampir tidak ada dunia yang akan bersikeras agar manusia menyelesaikannya lebih lambat dan lebih mahal ketika komputer dapat dengan mudah memecahkan masalah matematika yang bermakna
- Benar, tetapi misalnya jika AI membuktikan konjektur Goldbach, itu akan menjadi hal yang luar biasa
- Dari sudut pandang konsumen, tidak ada bedanya apakah pabrik pengolahan daging atau gudang Amazon mempekerjakan 5.000 orang atau 5 orang
  Prinsip ini jelas berlaku untuk seni, tetapi untuk pekerjaan hanya berlaku pada sebagian atau sebagian besar saja
- Ada orang yang percaya bahwa matematika, tidak seperti catur atau seni, benar-benar berguna. Kebanyakan matematikawan mungkin tidak berpikir begitu, tetapi kalau kita terima dulu gagasan gila ini sejenak, pembuktian hanyalah alat yang memberi tahu bahwa “potongan matematika ini telah diterapkan dengan benar”
  Maka kita tidak perlu memahami pembuktiannya, dan tidak ada yang peduli apakah ada matematikawan di suatu tempat yang sepenuhnya memahami pembuktian itu. Tidak apa-apa jika mesin lebih baik daripada kita dalam menemukan dan memeriksa pembuktian; justru itu menjadi sesuatu yang bisa diperkirakan
- Menurut saya prinsip ini tidak terlalu berlaku untuk pembuktian matematika. Pembuktian jauh, jauh lebih mudah diverifikasi daripada dibuat, dan pembuktian kedua hanya menjadi catatan kaki
  Banyak matematikawan mungkin tidak ingin berkutat pada pekerjaan seperti itu. Namun masih ada jarak yang besar antara IMO dan garis depan matematika riset
Saya selalu berpikir pembuktian teorema adalah permainan satu pemain dengan ruang pencarian yang luar biasa besar, sehingga akan terpecahkan jauh sebelum AGI
Secara pribadi, menurut saya kontributor terbesar AlphaProof adalah orang-orang di balik Lean dan Mathlib, karena mereka mengambil tugas berat untuk memformalkan seluruh matematika
Kurangnya formalisasi dalam makalah matematika terus mematikan upaya otomasi. Sebab para peneliti AI harus bergulat dengan unsur-unsur manusiawi seperti notasi khas penulis, pengetahuan implisit, dan langkah-langkah pembuktian yang dihilangkan
- Pernyataan bahwa “pembuktian teorema adalah permainan satu pemain dengan ruang pencarian yang luar biasa besar, jadi akan terpecahkan jauh sebelum AGI” terdengar aneh
  Saya pikir istilah AGI sendiri tidak terdefinisi, tetapi saya tidak mengerti mengapa orang memperkirakan bahwa membuat “sesuatu yang secara umum cerdas”, yaitu kecerdasan setingkat median manusia, jauh lebih sulit daripada “lebih jago matematika daripada Terrence Tao”
- Mereka tidak memformalkan seluruh matematika. Untungnya IMO tidak membutuhkan seluruh matematika. Namun mereka bahkan belum memformalkan cukup banyak untuk IMO. Mungkin itulah sebabnya mereka tidak bisa menyelesaikan soal kombinatorika
Diskusi terbaik ada di sini: https://leanprover.zulipchat.com/#narrow/stream/219941-Machi...