Pelancaran ProofOfThought , sebuah sistem yang menggabungkan model bahasa besar dengan pembuktian teorem Z3 untuk penaakulan formal, telah mencetuskan perbincangan hangat dalam komuniti AI mengenai sifat penaakulan mesin dan keberkesanan pendekatan hibrid terhadap kecerdasan buatan.
ProofOfThought mewakili percubaan untuk merapatkan jurang antara sifat kabur dan kebarangkalian LLM dengan ketepatan yang ketat dalam sistem logik formal. Projek ini membolehkan pembangun untuk membuat pertanyaan kepada model bahasa untuk tugasan penaakulan yang kompleks sambil menggunakan pembuktik teorem matematik untuk mengesahkan konsistensi logik hasil tersebut.
Janji dan Perangkap Sistem AI Hibrid
Perbincangan komuniti mendedahkan kedua-dua keterujaan dan keraguan mengenai penggabungan model bahasa statistik dengan alat pengesahan formal. Beberapa pembangun telah berkongsi pengalaman positif dengan pendekatan yang serupa, terutamanya apabila menggunakan LLM untuk menjana kod bagi pakej pengiraan simbolik seperti SymPy atau Prolog . Sistem hibrid ini memanfaatkan keupayaan pemahaman bahasa semula jadi LLM sambil bergantung pada alat matematik deterministik untuk pengiraan sebenar.
Walau bagaimanapun, keputusan penilaian projek itu sendiri menyerlahkan cabaran yang ketara. Sistem ini menunjukkan kadar positif palsu yang membimbangkan sebanyak 51% pada penanda aras logik, menunjukkan bahawa LLM bergelut untuk menterjemah pertanyaan bahasa semula jadi kepada representasi logik formal dengan tepat. Jurang autoformalisasi ini mewakili cabaran asas dalam merapatkan penaakulan manusia dan logik mesin.
SymPy: Perpustakaan Python untuk matematik simbolik yang boleh melakukan manipulasi algebra, kalkulus, dan penyelesaian persamaan Z3: Pembuktik teorem yang dibangunkan oleh Microsoft Research yang boleh menyelesaikan kekangan logik dan matematik yang kompleks
Metrik Prestasi ProofOfThought
| Metrik | Nilai | Nota |
|---|---|---|
| Kadar Positif Palsu | 51% | Pada penanda aras logik dengan GPT-4o |
| Jaminan Kekukuhan | 99%+ | Dalam pelaksanaan komersial AWS |
| Lapisan Seni Bina | 2 | API peringkat tinggi dan DSL peringkat rendah |
Keperluan Pemasangan
- z3-solver
- openai
- scikit-learn
- numpy
- Persekitaran Python
Persoalan Asas Penaakulan Mesin
Projek ini telah mencetuskan semula perdebatan falsafah mengenai sama ada LLM benar-benar boleh berfikir atau hanya mensimulasikan penaakulan melalui padanan corak. Pengkritik berhujah bahawa model bahasa statistik tidak mempunyai kekangan logik tulen dalam proses generatif mereka, menjadikan mereka pada asasnya tidak sesuai untuk tugasan penaakulan formal.
LLM adalah model bahasa statistik bukan pereka akal selepas semua. Saya mendapati menjana program logik, dan kod sumber Prolog secara khusus, berfungsi dengan luar biasa baik, mungkin kerana Prolog diperkenalkan untuk pemprosesan bahasa semula jadi simbolik.
Perspektif ini menunjukkan bahawa walaupun LLM mungkin cemerlang dalam menjana kod dalam bahasa pengaturcaraan logik disebabkan pertindihan data latihan, mereka tidak terlibat dalam penaakulan logik sebenar. Langkah pengesahan formal menjadi kurang mengenai memastikan ketepatan dan lebih mengenai mengklasifikasikan sama ada output LLM kebetulan logik yang kukuh.
Cabaran Pelaksanaan Teknikal
Pembangun telah mencatatkan isu praktikal dengan pelaksanaan semasa, termasuk kesukaran dengan menghurai output bahasa khusus domain yang kompleks dan keperluan untuk pengawasan manual representasi formal yang dijana. Pergantungan sistem pada pendekatan API yang lebih lama dan bukannya ciri output berstruktur moden juga telah menarik kritikan daripada pengamal yang biasa dengan keupayaan LLM semasa.
Evolusi projek ke arah menggunakan sintaks SMT (Satisfiability Modulo Theories) dalam penyelidikan susulan menunjukkan usaha berterusan untuk menangani had teknikal ini. Walau bagaimanapun, cabaran teras kekal: memastikan bahawa LLM boleh menterjemah penaakulan bahasa semula jadi kepada kenyataan logik formal dengan boleh dipercayai.
SMT: Rangka kerja untuk memeriksa kepuasan formula logik berkenaan dengan gabungan teori latar belakang
Aplikasi Dunia Sebenar dan Hala Tuju Masa Depan
Walaupun terdapat cabaran, beberapa organisasi sedang meneroka pendekatan yang serupa untuk aplikasi praktikal. Syarikat sedang bereksperimen dengan menggunakan pengesahan formal untuk mengesahkan kandungan yang dijana AI terhadap dokumen dasar dan keperluan pematuhan, dengan sesetengahnya mendakwa jaminan kekukuhan melebihi 99% dalam domain tertentu.
Perbincangan mendedahkan pengiktirafan yang semakin meningkat bahawa pendekatan hibrid mungkin diperlukan untuk sistem AI yang boleh dipercayai, walaupun pelaksanaan semasa menghadapi had yang ketara. Apabila model bahasa terus bertambah baik, jurang antara penaakulan bahasa semula jadi dan representasi logik formal mungkin mengecil, menjadikan sistem sedemikian lebih praktikal untuk penggunaan dunia sebenar.
Projek ProofOfThought , walaupun menyerlahkan had semasa, mewakili langkah penting ke arah sistem penaakulan AI yang lebih boleh dipercayai. Sambutan bercampur komuniti menggariskan kedua-dua potensi dan cabaran ketara yang masih wujud dalam mencipta kecerdasan buatan yang benar-benar boleh dipercayai.
Rujukan: ProofOfThought