Pandangan Terence Tao tentang Proof Checker dan Program AI

 (scientificamerican.com)
1 poin oleh GN⁺ 2024-06-13 | 1 komentar | Bagikan ke WhatsApp

AI akan menjadi 'co-pilot' bagi para matematikawan

Perubahan dalam matematika

  • Matematika secara tradisional merupakan disiplin yang bersifat soliter.
  • Belakangan ini, banyak bagian dari matematika dapat diuraikan secara ketat menjadi komponen-komponen terpisah sehingga bisa diverifikasi oleh komputer.
  • Terence Tao dari UCLA meyakini bahwa metode-metode ini membuka kemungkinan kolaborasi baru dalam matematika.

Munculnya pemeriksa bukti otomatis

  • Melalui pemeriksa bukti otomatis, para matematikawan dapat berkolaborasi dengan ratusan orang.
  • Sebagai contoh, Tao membuktikan konjektur Polynomial Freiman-Ruzsa (PFR) dengan berkolaborasi bersama lebih dari 20 orang.
  • Prosesnya berjalan dengan cara setiap individu menyumbangkan pembuktian langkah-langkah kecil, sementara arah keseluruhan dikelola secara terpusat.

Formalisasi matematika

  • Tidak semua orang perlu menjadi programmer; peran dapat dibagi antara orang yang berfokus pada arah matematis dan orang yang membuat bukti formal.
  • Pengembangan pustaka matematika standar membuat matematika formal menjadi praktis.
  • Proyek bernama Lean memiliki pustaka yang sangat besar, termasuk teorema-teorema matematika dasar.

AI dan masa depan matematika

  • AI berpotensi berperan sebagai asisten bagi para matematikawan.
  • AI dapat membantu pekerjaan seperti memformalkan bukti dan menulis lalu mengajukan makalah.
  • Kolaborasi dapat terjadi dengan cara manusia memberikan ide, lalu AI memformalkannya.

Cara baru dalam bermatematika

  • Ada kemungkinan muncul cara baru dalam bermatematika melalui kolaborasi dengan AI.
  • Peran matematikawan bisa berubah menjadi seperti manajer proyek yang membagi tugas, sementara AI membantu pembuktian.
  • Buku teks matematika dapat diformalisasi untuk membuat alat belajar yang lebih interaktif.

Batasan dan potensi AI

  • AI dapat membantu menyelesaikan masalah besar dalam matematika, tetapi intuisi dan pemahaman manusia tetap penting.
  • Mungkin akan dibutuhkan tipe matematikawan baru yang menganalisis dan memahami bukti yang diberikan AI.
  • AI dapat menjelajahi wilayah baru dalam matematika dan membantu pada bagian-bagian yang sulit dipahami manusia.

Opini GN⁺

  • Peran AI: AI dapat memainkan peran penting sebagai alat yang membantu para matematikawan memecahkan masalah yang lebih besar.
  • Pentingnya kolaborasi: Kolaborasi antara AI dan manusia dapat membuka kemungkinan baru dalam matematika.
  • Kebutuhan formalisasi: Formalisasi matematika dapat membuat lebih banyak pengetahuan menjadi eksplisit dan mendorong kolaborasi.
  • Matematikawan masa depan: Mungkin akan dibutuhkan tipe matematikawan baru yang bekerja sama dengan AI untuk menganalisis dan memahami bukti.
  • Perkembangan teknologi: Perpaduan AI dan matematika dapat membuka lebih banyak kemungkinan seiring kemajuan teknologi.

Bacaan terkait

1 komentar

 
GN⁺ 2024-06-13
Opini Hacker News

  • Tulisan Edsger Dijkstra: Menyebut sebuah tulisan tahun 1975 yang menyindir cara produksi perangkat lunak, dengan isi utama berupa kritik terhadap hak kekayaan intelektual.

  • Kemampuan LLM: Saat ini berperan sebagai asisten, tetapi ke depan berpotensi memberikan wawasan pada tingkat yang lebih tinggi. Misalnya, menangkap hal-hal yang terlewat oleh manusia, seperti memahami hubungan antara bom nuklir dan tumpukan kompos.

  • Ringkasan wawancara:

    • Matematikawan manajer proyek: AI dan alat bantu pembuktian dapat menjadi revolusioner dalam menghasilkan wawasan matematis.
    • Pengetahuan implisit: Karena pengetahuan tentang intuisi dan kegagalan tidak dimasukkan ke dalam makalah, komunikasi antarmatematikawan menjadi penting.
    • Formalisasi matematika: Alat bantu pembuktian perlu membuat matematika lebih formal agar membantu pemahaman.

  • Pembuktian yang diverifikasi komputer: AI dapat berguna untuk verifikasi bukti seperti mesin catur. Ada kesulitan dalam menangani banyak teorema dan lema, tetapi AI dapat memperbaiki hal ini.

  • Sejarah perangkat lunak dan matematika: Membandingkan proyek perangkat lunak masa lalu dengan rekayasa perangkat lunak modular saat ini, dengan pandangan bahwa matematika juga bisa menempuh jalur serupa.

  • Ceramah Terence Tao: Merekomendasikan ceramah yang menjelaskan lebih rinci cara menggunakan Lean dalam riset matematika.

  • Pembuktian matematika dengan GPT-4: Memperkenalkan contoh ketika GPT-4 berhasil membuktikan lema baru. Ini dapat berguna untuk riset matematika.

  • Matematikawan awal karier dan Lean: Ada pendapat bahwa matematikawan di awal karier mungkin lebih baik mempercayai intuisi mereka dan menulis makalah.

  • Belajar dari kegagalan: Ada pendapat bahwa belajar dari kegagalan orang lain sangat produktif.