Buktikan, Bagian 2: Logika Formal, Kebijakan Cedar, dan Ekonomi Verifikasi

Penalaran otomatis menambahkan verifikasi di atas output LLM dengan menerjemahkan kebijakan bisnis ke dalam logika formal dan memeriksanya terhadap aturan tersebut. Ini mendeteksi halusinasi, menegakkan batasan kepatuhan, dan mengontrol tindakan agen dengan cakupan penuh pada biaya yang jauh lebih rendah daripada QA manual.

Di Bagian 1 ('Mungkin Benar' Tidak Cukup Baik”), kami membahas mengapa startups yang membangun AI membutuhkan verifikasi deterministik, bukan hanya perlindungan probabilistik. Dalam posting ini, kami akan membahas seluk-beluknya. Jika Anda adalah salah satu pendiri teknis, pemimpin rekayasa, atau developer senior di startup AI, di sinilah Anda belajar bagaimana penalaran otomatis sebenarnya bekerja, apa yang terjadi ketika LLM Anda menghasilkan respons dan logika formal memeriksanya, serta mengapa dari segi ekonomi hal ini menjadi pilihan yang sangat masuk akal dibandingkan dengan merekrut tim QA.

Tidak ada kode API di posting ini. Hal tersebut akan dibahas di Bagian 3. Di sini kami fokus pada konsep, logika formal, dan jalur verifikasi agar Anda memahami apa yang Anda bangun.

Stokastik vs. deterministik: Perbedaan fundamental

Sebelum membahas mekanismenya, ada baiknya memahami perbedaan inti ini dengan jelas, karena hal ini memengaruhi setiap keputusan arsitektur yang Anda buat.

LLM bersifat stokastik.

Mereka memprediksi token berikutnya berdasarkan distribusi probabilitas yang dipelajari dari data pelatihan. Parameter sampling suhu, top-k, dan top-p memperkenalkan keacakan yang disengaja. Jalankan prompt yang sama dua kali dan Anda mungkin mendapatkan jawaban yang berbeda. Ini adalah fitur, bukan bug: itulah yang membuat LLM fleksibel, kreatif, serta mampu menangani beragam input bahasa alami. Namun, hal ini juga berarti bahwa setiap output tunggal adalah sampel dari distribusi probabilitas, bukan fakta yang terbukti.

Penalaran otomatis (AR) benar.

Dengan diberikan seperangkat aturan dan input, hasilnya bukan tebakan terbaik. Ini adalah bukti. Sebuah pernyataan terbukti valid sehubungan dengan aturan Anda, terbukti tidak valid, atau sistem memberi tahu Anda dengan tepat informasi apa yang hilang atau ambigu. Jika jawabannya salah, AR tidak hanya menandainya; AR memberi Anda contoh tandingan yang menunjukkan dengan tepat mengapa itu gagal. Output-nya dapat diverifikasi secara matematis, bukan probabilistik. Tidak ada kenop suhu. Tidak ada sampling. Ada bukti yang dapat Anda periksa.

Ini bukan tentang satu pendekatan yang "lebih baik." LLM lebih baik dalam memahami bahasa alami dan menghasilkan respons seperti manusia. AR lebih baik dalam memeriksa apakah respons tersebut secara logis benar. Secara bersama, mereka membentuk tumpukan lengkap: LLM menangani percakapan, AR menangani kebenaran. Kombinasi jaringan neural dan logika formal inilah yang oleh para peneliti disebut AI neurosimbolis.

Bagi startup beranggotakan lima orang yang mengirimkan produk ke 100 pelanggan pertama Anda, perbedaan ini memiliki konsekuensi yang sangat praktis. Anda tidak memiliki cukup karyawan untuk tim QA, dan Anda tidak memiliki waktu untuk mengatasi insiden ketidakpatuhan. Verifikasi formal menjadi pengganda kekuatan yang memungkinkan tim kecil untuk mengirimkan produk dengan keyakinan yang jauh lebih besar.

Apa dua lapisan perlindungan di Amazon Bedrock?

AWS menyediakan AR di dua lapisan, dan keduanya memetakan secara rapi kurva kematangan pada sebagian besar startups AI. Ketika Anda berada di tahap awal, produk Anda kemungkinan adalah chatbot atau asisten: LLM menjawab pertanyaan pelanggan, menghasilkan rekomendasi, atau memberikan panduan. Pada tahap ini, penalaran otomatis di Batas Pengaman Amazon Bedrock memverifikasi konten output model terhadap aturan bisnis yang ditentukan

Saat Anda tumbuh, Anda mulai membangun alur kerja agentik: AI Anda membuat janji temu, memproses pengembalian uang, melakukan kueri basis data, memanggil API eksternal. Pada lapisan ini, Kebijakan di Amazon Bedrock AgentCore mengatur tindakan apa yang diizinkan untuk dilakukan oleh agen, menggunakan kebijakan Cedar yang diberlakukan di gateway sebelum setiap pelaksanaan alat.

Kebijakan Cedar mengatur apa yang dapat dilakukan agen. Namun, Anda juga dapat mengekspos API pemeriksaan AR sebagai alat di toolkit agen, membiarkan agen memvalidasi kesimpulan menengahnya sendiri sebelum menindaklanjutinya. Agen memanggil ApplyGuardrail terhadap kebijakan Anda, memeriksa temuan, dan mengoreksi diri tanpa melibatkan pengguna. Sebuah agen yang merencanakan alur kerja multilangkah dapat memeriksa apakah urutan yang diusulkan melanggar batasan apa pun, mendeteksi kontradiksi dalam asumsinya, atau mengonfirmasi bahwa nilai turunan sebenarnya mengikuti dari input. Hal ini menggeser AR dari pemeriksaan batasan ke partner penalaran: agen tidak hanya diblokir di gerbang, tetapi menghindari berjalan menuju gerbang sejak awal.

Berikut adalah bagaimana mereka membandingkan:

Pemeriksaan AR dan Kebijakan di Amazon Bedrock AgentCore melindungi berbagai lapisan aplikasi Anda.

• Pemeriksaan AR memvalidasi apa yang dikatakan AI Anda, yaitu apakah jawaban kelayakan hipotek ini benar sesuai kriteria pinjaman Anda?
• Kebijakan di Amazon Bedrock AgentCore mengontrol apa yang dilakukan AI Anda, yaitu apakah agen ini berwenang untuk memulai pengembalian dana atau menanyakan akun pelanggan?

Bergantung pada apa yang Anda bangun sekarang, Anda mungkin mulai dengan satu atau keduanya.

• Jika MVP Anda adalah chatbot yang menjawab pertanyaan kebijakan, pemeriksaan AR adalah integrasi pertama Anda.
• Jika Anda mengirimkan agen yang membuat janji temu dan memindahkan uang, Kebijakan tidak dapat dinegosiasikan sejak awal.

Sebagian besar startups pada akhirnya akan menjalankan keduanya secara bersama.

Cara kerja pemeriksaan AR: Melakukan enkode aturan bisnis Anda sebagai logika formal

Input ke AR adalah kebijakan, dan kebijakan dimulai dengan dokumen yang sudah Anda miliki.

Jika Anda adalah startup fintech, hal ini dapat menjadi dokumen kriteria pinjaman. Dalam layanan kesehatan, mungkin protokol klinis atau prosedur penanganan HIPAA. Dalam asuransi, pedoman penjaminan. Dokumen-dokumen ini mendefinisikan apa yang seharusnya dan tidak seharusnya dikatakan oleh AI Anda. Dokumen tersebut telah ditinjau oleh penasihat hukum Anda. Investor Anda menanyakannya selama uji tuntas. AR mengubah artefak yang sudah ada menjadi aturan yang dapat ditegakkan. Anda tidak membangun sesuatu yang baru dari awal. Anda mengaktifkan sesuatu yang sudah Anda miliki.

Saat Anda mengunggah dokumen kebijakan (PDF, Markdown, atau teks biasa) ke Amazon Bedrock, sistem mengekstrak dua hal: variabel dan aturan.

Variabel mewakili konsep dalam domain Anda. Setiap variabel memiliki nama, tipe, dan deskripsi. Misalnya, dalam kebijakan kelayakan hipotek:

Deskripsi variabel adalah satu-satunya faktor terpenting dalam akurasi. Deskripsi yang tidak jelas membuat LLM menebak apa yang diwakili oleh variabel. Deskripsi terperinci yang menjelaskan apa arti konsep tersebut, bagaimana pengguna Anda merujuknya, dan bagaimana konsep tersebut muncul dalam dokumen kebijakan Anda memberikan LLM konteks yang dibutuhkan untuk memetakan bahasa alami ke variabel formal yang tepat. Di sinilah keahlian domain Anda sebagai pembuat startup sangat penting.

Aturan adalah ekspresi logika formal yang mendeteksi hubungan antarvariabel. Aturan menggunakan subset sintaksis SMT-LIB, dan sebagian besar mengikuti format jika-maka (implikatif):

Inilah yang dihasilkan Bedrock secara detail ketika Anda mengunggah dokumen kebijakan hipotek Anda. Anda dapat meninjau aturan ini di konsol untuk memverifikasi bahwa sistem mengambil maksud Anda dengan benar, tetapi Anda tidak menulis SMT-LIB secara manual. Anda menulis kebijakan dalam bahasa alami, dan sistem menerjemahkannya ke dalam logika formal.

Proses verifikasi dua langkah

Setelah Anda menyiapkan kebijakan AR dan melampirkannya ke batasan pengaman (tercakup di Bagian 3), setiap respons LLM yang dikirim aplikasi Anda ke ApplyGuardrail melewati proses verifikasi dua langkah. Memahami pemisahan ini sangat penting karena memberi tahu Anda di mana harus menginvestasikan usaha Anda.

Langkah 1: Terjemahan

Sistem mengonversi bahasa alami dalam pertanyaan pengguna dan respons LLM menjadi predikat logika formal, pernyataan seperti penghasilan “>= 180 & penghasilan <= 220” alih-alih penugasan sederhana, menggunakan variabel yang dinyatakan dalam kebijakan Anda. Di sinilah deskripsi variabel berperan.

Misalnya, jika responsnya mengatakan “pelanggan dengan uang muka 30.000 USD untuk rumah seharga 350.000 USD memenuhi syarat untuk hipotek konvensional,” langkah terjemahan menghasilkan: downPaymentAmount = 30000, purchasePrice = 350000, mortgageType = KONVENSIONAL.

Fakta bahwa kami menggunakan LLM untuk menerjemahkan bahasa alami input Anda ke dalam logika adalah alasan mengapa sistem ini mengeklaim akurasi verifikasi hingga 99 persen. Untuk memastikan terjemahan kami benar, kami tidak hanya mengandalkan satu LLM. Alih-alih, kami menggunakan banyak LLM pada suhu yang berbeda secara paralel untuk melakukan terjemahan yang sama. Hanya ketika terjemahan yang berlebihan tersebut setara secara semantik, kami dapat membuat hasil validasi. Ketika terjemahan tidak setuju, kami mengembalikan hasil AMBIGU yang mencakup dua kemungkinan interpretasi input. LLM Anda dapat menggunakan umpan balik ini untuk memisahkan jawabannya atau mengajukan pertanyaan klarifikasi kepada pengguna. Ketika kami membandingkan sistem kami terhadap set data QA kondisional dari Carnegie Mellon, di lebih dari 99 persen kasus dengan jawaban ditandai sebagai VALID dari sistem kami, tanda tersebut benar. Anda dapat menemukan detail selengkapnya tentang metodologi di makalah ini.

Langkah 2: Verifikasi

Pemecah Satisfiability Modulo Theories (SMT) mengevaluasi apakah penugasan yang diterjemahkan memenuhi semua aturan kebijakan Anda. Langkah ini secara matematis masuk akal menurut definisi. Setelah terjemahannya benar, verifikasi terbukti benar.

Untuk contoh hipotek: pemecah menghitung downPaymentPercentage = (30000/350000) * 100 = 8,57 persen, memeriksa ini terhadap aturan (=> (< downPaymentPercentage 20,0) (not (= mortgageType KONVENSIONAL))), menemukan bahwa 8,57 < 20, dan menyimpulkan bahwa mortgageType = KONVENSIONAL secara logis tidak valid. Sistem mengembalikan temuan yang tidak valid dengan jejak lengkap yang menunjukkan dengan tepat aturan mana yang dilanggar dan mengapa.

Hal penting yang praktis bagi para pembuat startup? Kualitas terjemahan adalah sesuatu yang Anda kontrol melalui deskripsi variabel yang lebih baik. Matematika verifikasi adalah sesuatu yang tidak perlu Anda khawatirkan. Anda berinvestasi dalam mendeskripsikan domain Anda dengan baik, dan pemecah menangani sisanya.

Apa arti dari temuan tersebut?

Pemeriksaan AR tidak hanya mengembalikan “lulus” atau “gagal. “Mereka mengembalikan temuan terstruktur yang memberi tahu Anda apa yang terjadi dan apa yang harus dilakukan selanjutnya. Setiap temuan adalah salah satu dari jenis ini:

Ini penting: Pemeriksaan AR beroperasi dalam mode deteksi. Pemeriksaan AR mengembalikan temuan dan umpan balik, tetapi tidak memblokir respons. Aplikasi Anda memeriksa temuan serta memutuskan apa yang harus dilakukan: menyajikannya, menulis ulang, meminta klarifikasi, atau kembali ke default yang aman. Ini memberi Anda kontrol penuh atas pengalaman pengguna sambil mendapatkan verifikasi matematis pada setiap respons. Untuk contoh kerja dari pola ini, lihat implementasi chatbot penulisan ulang sumber terbuka, yang menunjukkan cara mengambil temuan AR dan memasukkannya kembali ke LLM untuk koreksi otomatis.

Kebijakan AgentCore: Batasan deterministik untuk agen AI

Jika startup Anda membangun aplikasi agentik, AI Anda mengatur alur kerja multilangkah, memanggil alat, dan mengambil tindakan atas nama pengguna, Anda memiliki masalah kepercayaan yang berbeda. Hal ini bukan hanya tentang apa yang dikatakan AI. Ini tentang apa yang dilakukan AI.

Untuk startups di bidang layanan kesehatan, fintech, atau hukum, “agen melakukan sesuatu yang tidak terduga” tidak dapat diterima dari perspektif kepatuhan atau peraturan. Anda membutuhkan batasan yang dapat dibuktikan pada perilaku agen, dan batas-batas tersebut perlu dipertahankan bahkan ketika agen dimanipulasi dengan injeksi prompt atau membuat kesalahan penalaran.

Kebijakan di Amazon Bedrock AgentCore menyelesaikan ini dengan lapisan otorisasi yang diberlakukan pada setiap interaksi agen-alat di batas gateway. Kebijakan ditulis dalam Cedar, bahasa otorisasi yang dibuat oleh AWS untuk diverifikasi dengan AR. Kebijakan Cedar menentukan siapa (principal) yang dapat melakukan apa (tindakan) pada sumber daya mana, dalam kondisi apa. Tidak ada invokasi alat yang melewati gateway tanpa izin yang cocok. Anda dapat menulis kebijakan langsung di Cedar atau menjelaskan aturan Anda dalam bahasa alami dan membiarkan sistem menghasilkan Cedar untuk Anda.

Sebelum kebijakan Anda di-deploy, penalaran otomatis menjalankan validasi semantik untuk mendeteksi masalah, termasuk:

• Kebijakan yang terlalu permisif yang akan memungkinkan semua permintaan untuk kombinasi principal/tindakan/sumber daya tertentu
• Kebijakan yang terlalu ketat yang akan menyangkal segalanya
• Kebijakan yang tidak efektif yang Izinnya tidak mengizinkan apa pun atau Larangan tidak melarang apa pun

Penegakan mengikuti dua prinsip yang sangat penting bagi startups di industri yang diatur:

1. Tolak secara default: jika tidak ada kebijakan yang secara eksplisit mengizinkan tindakan, tindakan tersebut diblokir. Agen Anda tidak dapat melakukan apa pun yang tidak Anda otorisasi.
2. Larangan selalu menang atas izin: Anda dapat mengatur aturan tegas yang tidak dapat diganti, terlepas dari kebijakan lain yang ada.

Pertimbangkan startup layanan kesehatan yang membangun agen penjadwalan janji temu. Dengan Kebijakan AgentCore, Anda dapat menegakkan bahwa pasien hanya mengakses catatan mereka sendiri, bahwa pemesanan janji temu dibatasi pada jam kerja, dan jumlah pengembalian dana dibatasi oleh kebijakan. Aturan ini berlaku terlepas dari bagaimana agen diminta, bug apa pun yang ada dalam kode Anda, atau seberapa kreatif pengguna dengan permintaan mereka. Penegakan terjadi di batas gateway, di luar agen sepenuhnya.

Berapa biaya penalaran otomatis dibandingkan dengan QA manual?

Untuk memahami ekonomi penalaran otomatis, berguna untuk membandingkannya dengan acuan dasar yang digunakan sebagian besar tim saat ini: tinjauan QA manual dari output model.

Cara lama: QA Manual

Seorang peninjau yang memeriksa output AI dapat menangani sekitar 50 interaksi per jam pada biaya yang dibebankan sekitar 40 USD/jam. Untuk startup yang menangani 100.000 interaksi pelanggan setiap bulan, meninjau setiap interaksi membutuhkan biaya 80.000 USD/bulan. Bahkan sampling 10 persen berharga 8.000 USD/bulan, dan Anda masih belum diverifikasi pada 90 persen lainnya. Pada biaya 80 ribu USD hingga 150 ribu USD per peninjau setiap tahun, tim yang terdiri dari 5 hingga 10 peninjau menghabiskan biaya 400 ribu USD hingga 1,5 juta USD per tahun. Bagi sebagian besar startups, hal tersebut merupakan sejumlah besar dana yang dihabiskan untuk memeriksa apakah AI Anda benar.

Cara baru: penalaran otomatis

Pemeriksaan AR dihargai per permintaan validasi. (Harga yang tepat harus dikonfirmasi di halaman harga Bedrock karena tarif dapat bervariasi.) Tidak seperti peninjauan manual, setiap interaksi dapat diverifikasi alih-alih hanya diambil sampelnya. Batas Pengaman Amazon Bedrock menggunakan unit teks sebagai unit validasi, yang setiap unit teks adalah 1.000 karakter. Berikut tampilannya untuk startup pada umumnya:

Asumsi

Perhitungan

Menggunakan contoh di atas dari startup yang menangani 100 ribu interaksi per bulan, dan dengan asumsi bahwa output dari setiap interaksi adalah ~200 token, kami dapat dengan mudah memperkirakan biaya penggunaan pemeriksaan AR untuk validasi. Batas Pengaman Amazon Bedrock mengukur penggunaan di Unit Teks, yang satu unit teks adalah 1000 karakter. Dengan menggunakan rata-rata 4 karakter per token, kami memperkirakan setiap interaksi menjadi ~800 karakter dan karenanya 0,8 unit teks.

Validasi 100.000 interaksi dengan masing-masing 0,8 unit teks memberi kami total 80 ribu unit teks per bulan. Dengan harga pemeriksaan AR 0,17 USD per 1000 unit teks, total biaya bulanan kami untuk satu kebijakan adalah 13,60 USD. Dengan beberapa kebijakan yang diterapkan, biaya berskala secara linier. Bahkan dengan beberapa kebijakan, total biaya tetap jauh lebih rendah dibandingkan peninjauan manual.

Matematika kepatuhan bahkan lebih menarik. Satu kategori pelanggaran HIPAA dapat dikenai biaya hingga 2.067.813 USD per tahun berdasarkan angka yang disesuaikan dengan inflasi saat ini. Bagi startup layanan kesehatan yang AI-nya memproses ribuan interaksi pasien setiap hari, paparan peraturan dari output yang tidak diverifikasi bersifat eksistensial. Dalam konteks ini, AR berfungsi kurang seperti biaya perangkat lunak dan lebih seperti kontrol manajemen risiko.

Bagi developer, analogi terdekat adalah pemeriksa pinjaman dari Rust. Rust mendeteksi kerusakan memori pada waktu kompilasi, sebelum kode mencapai produksi. AR mendeteksi pelanggaran kebijakan pada waktu verifikasi, sebelum mencapai pelanggan Anda. Mengambil kesalahan sebelum menyebabkan kerusakan selalu lebih murah dibandingkan membersihkan sesudahnya.

Ada pertukaran: Validasi AR menambahkan latensi ke setiap respons, dan menulis ulang berarti LLM Anda berjalan dua kali pada output yang ditandai. Namun, untuk sebagian besar aplikasi, biaya tersebut tidak seberapa dibandingkan dengan dampak operasional, hukum, atau reputasi dari output yang salah.

Argumen yang sama bergema dengan investor. Mampu mengatakan bahwa output AI diverifikasi secara sistematis terhadap kebijakan bisnis formal bukan hanya fitur produk. Ini adalah bukti bahwa risiko dikelola secara proaktif. Itulah jenis klaim konkret dan dapat diverifikasi yang memperkuat profil risiko startup.

Apa langkah selanjutnya?

Di Bagian 3: Playbook Implementasi Langkah demi Langkah, kami akan membahas dari konsep hingga kode. Anda akan mempelajari cara membuat kebijakan AR dari dokumen yang ada, melakukan deployment ke batasan pengaman, mengintegrasikan dengan API ApplyGuardrail, menangani temuan secara terprogram, menyiapkan Kebijakan AgentCore melalui AgentCore Gateway, dan membangun jejak audit. Semua yang Anda butuhkan mulai dari membaca tentang verifikasi matematis hingga mengirimkannya di produksi.