Saya, seperti banyak orang, adalah pengguna perangkat lunak matematika yang tajam seperti Mathematica dan Maple. Namun, saya menjadi semakin frustrasi dengan banyak kasus di mana perangkat lunak seperti itu hanya memberi Anda jawaban yang salah tanpa peringatan. Ini dapat terjadi ketika melakukan semua jenis operasi dari jumlah sederhana hingga optimasi di antara banyak contoh lainnya.
Saya bertanya-tanya apa yang bisa dilakukan dengan masalah serius ini. Apa yang dibutuhkan adalah beberapa cara untuk memungkinkan pengguna memverifikasi kebenaran dari jawaban yang diberikan sehingga mereka memiliki kepercayaan pada apa yang mereka katakan. Jika Anda mendapatkan solusi dari kolega matematika, dia mungkin akan duduk dan menunjukkan kepada Anda pekerjaan mereka. Namun ini tidak layak untuk dilakukan komputer dalam banyak kasus. Dapatkah komputer sebagai gantinya memberikan Anda kesaksian yang sederhana dan mudah diperiksa kebenaran jawaban mereka? Memeriksa mungkin harus dilakukan oleh komputer tetapi semoga memeriksa algoritma pemeriksaan akan jauh lebih mudah daripada memeriksa algoritma untuk menghasilkan saksi di tempat pertama. Kapan ini layak dan bagaimana tepatnya ini bisa diformalkan
Jadi secara ringkas, pertanyaan saya adalah sebagai berikut.
Mungkinkah setidaknya dalam teori untuk perangkat lunak matematika untuk memberikan bukti yang dapat diperiksa pendek bersama dengan jawaban yang Anda minta?
Kasus sepele di mana kita dapat melakukan ini dengan segera adalah untuk faktorisasi bilangan bulat tentu saja atau banyak masalah klasik NP-complete (misalnya sirkuit Hamiltonian dll.).
sumber
Jawaban:
Konsep "saksi" atau "bukti yang dapat diperiksa" tidak sepenuhnya baru: seperti yang disebutkan dalam komentar, cari konsep "sertifikat". Tiga contoh muncul di benak, ada lebih banyak (di komentar dan di tempat lain):
Kurt Mehlhorn menggambarkan pada tahun 1999 masalah yang sama dalam algoritma geometri komputasi (misalnya kesalahan kecil dalam koordinat dapat menghasilkan kesalahan besar dalam hasil beberapa algoritma), diselesaikan dengan cara yang sama di perpustakaan Leda , dengan menegaskan bahwa setiap algoritma menghasilkan "sertifikat" dari jawabannya selain dari jawaban itu sendiri.
Demaine, Lopez-Ortiz dan Munro pada tahun 2000 menggunakan konsep sertifikat (mereka menyebutnya "bukti") untuk menunjukkan batas bawah adaptif pada perhitungan serikat dan persimpangan (dan perbedaan, tetapi ini sepele) dari set diurutkan. Jangan mengecualikan pekerjaan mereka karena mereka tidak menggunakan sertifikat untuk melindungi dari kesalahan komputasi: mereka menunjukkan bahwa meskipun sertifikat dapat linier dalam ukuran instance dalam kasus terburuk, sering kali lebih pendek, dan karenanya dapat "diperiksa "dalam waktu sublinear (diberikan akses acak ke input sebagai array yang diurutkan atau B-Tree), dan khususnya dalam waktu kurang dari yang diperlukan untuk menghitung sertifikat semacam itu.
Saya telah menggunakan konsep sertifikat pada berbagai masalah lain sejak melihat Ian Munro mempresentasikan implementasinya di Alenex 2001 , dan khususnya untuk permutasi (permintaan maaf untuk plug tak tahu malu, yang lain akan datang), di mana sertifikat lebih pendek dalam kasus terbaik daripada dalam kasus terburuk atau rata-rata, yang menghasilkan struktur data terkompresi untuk permutasi. Di sini sekali lagi, memeriksa sertifikat (yaitu pesanan) paling banyak memakan waktu linier, kurang dari menghitungnya (yaitu menyortir).
Konsep ini tidak selalu berguna untuk pemeriksaan kesalahan: ada masalah di mana memeriksa sertifikat membutuhkan waktu sebanyak waktu untuk memproduksinya (atau hanya menghasilkan hasilnya). Dua contoh muncul dalam pikiran, satu sepele dan satu rumit, Blum dan Kannan (disebutkan dalam komentar) memberi yang lain.
Perpustakaan Leda adalah upaya paling umum (yang saya tahu) untuk membuat algoritma penentuan sertifikat deterministik menjadi norma dalam praktiknya. Makalah Blum dan Kannan adalah upaya terbaik yang saya lihat untuk menjadikannya norma dalam teori, tetapi mereka menunjukkan batas-batas pendekatan ini.
Semoga ini bisa membantu ...
sumber