Lewati ke konten utamaAWS Startups
  1. Pelajari
  2. Buktikan, Bagian 1: Mengapa “Mungkin Benar” Tidak Cukup Baik untuk Startup AI Anda

Buktikan, Bagian 1: Mengapa “Mungkin Benar” Tidak Cukup Baik untuk Startup AI Anda

Bagaimana konten ini?

Startups yang menang di era AI tidak akan ditentukan oleh model tercanggih atau set data pelatihan terbesar, tetapi oleh kepercayaan. Pembeda utama adalah apakah pengguna memercayai mereka, dan apakah mereka dapat menjawab “apa yang terjadi ketika AI Anda salah?” dengan kepastian matematis, bukan hanya jaminan probabilistik. Di pasar yang teregulasi, verifikasi menjadi lebih penting daripada hanya kemampuan model.

Anda baru saja menyelesaikan putaran pendanaan awal. Asisten pinjaman bertenaga AI Anda diluncurkan minggu lalu dengan 200 pengguna beta. Pada hari ketiga, seorang pelanggan mengambil tangkapan layar chatbot Anda yang memberi tahu mereka bahwa mereka memenuhi syarat untuk hipotek konvensional dengan uang muka 8 persen. Mereka memostingnya di media sosial. Kebijakan Anda membutuhkan 20 persen.

Rekan pendiri Anda melihatnya pertama kali. Investor Anda melihatnya kedua. Penasihat hukum Anda melihatnya ketiga.

Ini bukan hipotetis. Ini adalah realitas nyata dalam membangun produk AI pada tahun 2026. Tim yang terdiri dari tiga orang mampu mengirimkan produk yang dua tahun lalu membutuhkan lima puluh rekayasawan, beralih dari ide ke MVP dalam hitungan hari, bukan bulan.

Namun, kecepatan tanpa verifikasi adalah sebuah kelemahan. AI generatif telah membuat pengiriman sesuatu yang mengalami halusinasi menjadi sangat mudah dan berbahaya, bertentangan dengan kebijakan Anda sendiri, atau memberi pelanggan Anda jawaban yang terbukti salah. Kesenjangan antara “kami mengirim” dan “kami mengirimkan sesuatu yang dapat dipercaya” adalah tempat startups gagal.

Akar penyebabnya adalah struktural. Model bahasa besar adalah sistem stokastik. Mereka menghasilkan teks dengan memprediksi token kemungkinan berikutnya. Proses ini melibatkan keacakan berdasarkan desain: suhu, strategi sampling, dan parameter top-k/top-p semuanya memperkenalkan variabilitas. Prompt yang sama dapat menghasilkan jawaban yang berbeda pada proses yang berbeda. Inilah yang membuat LLM kreatif dan bermanfaat. Hal ini juga yang membuat mereka pada dasarnya tidak dapat diandalkan untuk tugas yang membutuhkan kebenaran. Model Anda tidak mencoba memberikan saran hipotek yang buruk. Model tersebut memprediksi token berikutnya yang paling mungkin.

Setiap startup AI harus menyelesaikan ketegangan ini: bagaimana Anda membangun sistem probabilistik sambil memberikan jaminan kebenaran kepada pelanggan Anda, regulator Anda, dan investor Anda?

Apa yang terjadi ketika AI memberikan jawaban yang salah?

Ketika AI Anda memberikan panduan yang salah dan pelanggan bertindak berdasarkan panduan tersebut, Anda bertanggung jawab atas hasilnya. Jika AI layanan kesehatan Anda salah menyatakan keputusan cakupan di beberapa ratus interaksi pasien, sanksi perdata HIPAA berkisar dari 137 USD hingga 68.928 USD per pelanggaran bergantung pada tingkat kepelikan, dengan batas tahunan mencapai 2.067.813 USD per kategori pelanggaran berdasarkan angka terbaru yang disesuaikan dengan inflasi. Denda dapat melebihi total pendanaan Anda bahkan sebelum Anda mengetahui adanya masalah. Berdasarkan GDPR, denda untuk pelanggaran serius dapat mencapai 20 juta EUR atau 4 persen dari total omzet tahunan di seluruh dunia, mana yang lebih tinggi. Bagi startup tahap awal yang memproses data pelanggan UE, ini bukan denda. Ini adalah penutupan. Chatbot fintech yang menyetujui pinjaman untuk seseorang yang tidak memenuhi syarat menciptakan tanggung jawab regulasi. Bot asuransi yang salah mengutip ketentuan cakupan menciptakan sengketa kontrak yang tidak dapat Anda menangkan.

Di luar hukuman langsung, ada biaya urutan kedua: kesepakatan korporasi yang gagal karena Anda tidak dapat lulus peninjauan keamanan mereka, audit SOC 2 yang terhenti karena Anda tidak dapat menjelaskan bagaimana AI Anda mengambil keputusan, investor Seri A yang bertanya “apa yang terjadi ketika AI Anda salah?“dan tidak mendapatkan jawaban yang memuaskan.

Mengapa rekayasa prompt dan RAG tidak cukup

Setiap startup yang membangun dengan LLM memiliki versi tumpukan keamanan yang sama: rekayasa prompt yang cermat, retrieval-augmented generation (RAG), dan sejumlah peninjauan manual. Ini adalah praktik yang baik. Namun, praktik ini juga tidak cukup.

Rekayasa prompt bersifat heuristik, tidak dapat dibuktikan. Anda membuat instruksi yang mendorong model menuju perilaku yang benar, tetapi tidak ada jaminan model mengikutinya. Saat Anda meningkatkan ke versi model yang lebih baru, atau menyesuaikan prompt sistem Anda untuk menangani kasus edge baru, perilaku yang sebelumnya aman dapat rusak secara diam-diam. Anda membangun keamanan pada kontrak informal tanpa mekanisme penegakan hukum.

RAG mengurangi kemungkinan halusinasi dengan mendasarkan model dalam dokumen yang diambil. Ini adalah peningkatan nyata. Namun, model ini masih dapat mengabaikan, salah menafsirkan, atau secara selektif menggunakan konteks yang diambil. RAG menggeser distribusi probabilitas ke arah jawaban yang lebih baik. Hal ini tidak menghilangkan kemungkinan yang salah. “Biasanya benar” bukanlah strategi kepatuhan.

QA manual tidak akan mampu mengimbangi pertumbuhan Anda. Bahkan pengambilan sampel agresif (memeriksa 10 persen interaksi) menyisakan 90 persen yang tidak diverifikasi. Bagi startup yang menangani 100.000 interaksi pelanggan setiap bulan, mempekerjakan peninjau untuk memeriksa sampel output akan menghabiskan ratusan ribu dolar per tahun. Itu adalah jumlah karyawan yang tidak Anda miliki dalam tim tahap awal, dan Anda masih beroperasi dengan harapan untuk 90 persen yang tidak Anda periksa. Biaya ini bukan biaya sekali saja. Cara pelanggan Anda menuliskan pertanyaan berubah seiring waktu. Model itu sendiri berubah di bawah Anda. Perilaku yang sebelumnya dapat diandalkan dapat menurun setelah pembaruan model rutin. Prompting secara cermat yang berhasil bulan lalu dapat gagal secara diam-diam bulan berikutnya. Anda harus terus mengevaluasi, menguji ulang, dan menyesuaikan proses QA, menjadikannya pusat biaya yang berkelanjutan alih-alih masalah yang Anda selesaikan sekali saja.

Benang merah dari semua pendekatan ini adalah mengurangi risiko tanpa memberikan kepastian. Ketika investor Anda bertanya “dapatkah AI Anda menghasilkan output yang salah? “jawaban jujur dengan hanya menggunakan alat-alat ini adalah “mungkin tidak, sebagian besar waktu. “Itu bukanlah jawaban yang akan menutup pendanaan Seri A, atau yang memuaskan regulator.

Apa itu penalaran otomatis?

Penalaran otomatis adalah bidang ilmu komputer yang menggunakan logika matematis untuk memberikan jaminan tentang apa yang akan atau tidak akan dilakukan suatu sistem. Tidak seperti machine learning, yang mempelajari pola dari data, penalaran otomatis menggunakan logika matematis, pembuktian teorema, dan pemecahan kendala untuk membuktikan bahwa properti tertentu bertahan di ruang tidak terbatas dari semua input yang mungkin.

Perbedaannya sangat penting. Ketika model machine learning mengatakan “output ini 95 persen kemungkinan benar,” hal tersebut membuat klaim statistik. Ketika sistem penalaran otomatis mengatakan “output ini valid,” sistem telah membangun bukti matematis bahwa output memenuhi setiap batasan yang Anda tentukan. Tidak ada interval kepercayaan. Buktinya ada atau tidak.

Penalaran otomatis bukanlah pengganti model bahasa besar (LLM). Chatbot Anda masih membutuhkan model bahasa untuk memahami pertanyaan pelanggan dan menghasilkan respons alami. Apa yang disediakan penalaran otomatis adalah lapisan verifikasi di atas: LLM menghasilkan, penalaran otomatis memverifikasi.

Secara bersama, mereka membentuk tumpukan lengkap dengan kreativitas dan kebenaran hidup berdampingan. AI Anda masih dapat berbicara, membantu, dan cepat. Namun, penalaran otomatis memastikannya tetap dalam batasan bisnis serta kepatuhan yang Anda tentukan.

Bagaimana AWS menggunakan penalaran otomatis

AWS telah menggunakan penalaran otomatis dalam produksi selama bertahun-tahun, melindungi infrastruktur yang dijalankan oleh startups (dan semua orang).

  • Zelkova, mesin penalaran otomatis yang mendasari Penganalisis Akses AWS IAM, menggunakan pemecahan teori modulo kepuasan (SMT) untuk memverifikasi secara matematis bahwa kebijakan IAM dan Amazon Simple Storage Service (Amazon S3) Anda bekerja persis seperti yang dimaksudkan, mendeteksi jalur akses yang tidak diinginkan yang tidak terlihat oleh peninjauan manual
  • Cedar, sekarang proyek Sandbox CNCF, adalah bahasa kebijakan otorisasi pertama yang dibangun dari bawah ke atas untuk diverifikasi dengan penalaran otomatis, dan mendukung Izin Terverifikasi Amazon
  • Nitro Isolation Engine, hypervisor cloud pertama yang diverifikasi secara resmi, memastikan isolasi tenant untuk Amazon Elastic Compute Cloud (Amazon EC2) dengan sekitar 260.000 baris bukti yang diperiksa mesin
  • s2n-tls, pustaka TLS sumber terbuka AWS, menggunakan bukti formal untuk memverifikasi bahwa operasi kriptografisnya menahan waktu serangan channel sisi

Intinya bagi para pembuat startup adalah ini: teknik verifikasi matematis yang tersedia untuk Anda melalui Amazon Bedrock dan Amazon Bedrock AgentCore bukanlah prototipe penelitian. Mereka berasal dari disiplin rekayasa yang sama yang digunakan AWS untuk menjamin persisten S3, isolasi EC2, serta keamanan setiap koneksi TLS ke layanan AWS. Hingga saat ini, mengakses disiplin ini berarti membangun tim internal metode formal PhD, sebuah kemewahan yang disediakan bagi organisasi dengan anggaran laboratorium penelitian. Bedrock dan AgentCore menjadikannya panggilan API bayar per penggunaan.

Bagaimana startups dapat menggunakan Penalaran Otomatis?

Bagi tim startup, disiplin verifikasi matematis yang sama kini tersedia langsung melalui dua produk, yang masing-masing menangani lapisan yang berbeda dari masalah kepercayaan AI.

Pemeriksaan penalaran otomatis di Batas Pengaman Amazon Bedrock menggunakan logika formal berbasis SMT (pendekatan yang sama di balik Zelkova) untuk memverifikasi bahwa konten output LLM Anda mengikuti aturan bisnis Anda. Pertama, Anda menentukan kebijakan Anda: kriteria pinjaman, protokol layanan kesehatan, aturan kepatuhan, apa pun yang dibutuhkan bisnis Anda. Kemudian, sistem menerjemahkannya ke dalam logika formal dan memverifikasi setiap respons LLM terhadap aturan tersebut. Ketika model mengatakan sesuatu yang bertentangan dengan kebijakan Anda, sistem menangkapnya serta memberi tahu Anda dengan tepat aturan mana yang dilanggar dan mengapa.

Untuk skenario hipotek di bagian atas posting ini, sistem akan mendeteksi kesalahan uang muka 8 persen dan menyarankan nilai yang benar untuk LLM untuk menulis ulang jawaban sebelum sampai ke pengguna.

Kebijakan di Amazon Bedrock AgentCore menggunakan Cedar (bahasa kebijakan sumber terbuka untuk otorisasi) untuk menegakkan batasan deterministik pada tindakan agen AI. Jika Anda membangun aplikasi agentik yang AI Anda mengambill keputusan penting dengan menginvokasi alat, apakah itu berarti mengakses data sensitif, menulis ke sistem eksternal, atau mengambil tindakan atas nama pengguna, Kebijakan mencegat setiap permintaan agen ke alat di batasan gateway dan mengevaluasinya terhadap kebijakan Cedar sebelum pelaksanaan. Penegakannya bersifat deterministik. Hal ini beroperasi secara independen dari penalaran agen dan tidak dapat dilewati dengan injeksi prompt, halusinasi, atau bug dalam kode agen Anda. Untuk startup di bidang layanan kesehatan, fintech, atau hukum, ini berarti Anda dapat memberi tahu regulator Anda dengan tepat apa yang dapat serta tidak dapat dilakukan oleh agen Anda, didukung oleh kebijakan yang divalidasi secara matematis.

Sistem lain dalam portofolio metode formal AWS (Nitro Isolation Engine, s2n-tls, s2n-quic, Dafny) memberikan manfaat tidak langsung kepada Anda: setiap instans EC2 yang Anda jalankan berada pada isolasi yang diverifikasi secara resmi, dan setiap koneksi TLS menggunakan kriptografi yang diverifikasi secara resmi. Batas Pengaman Bedrock dan Kebijakan di AgentCore adalah tempat metode formal memasukkan kode aplikasi Anda secara langsung.

Dua lapisan, satu prinsip: verifikasi matematis formal atas kepercayaan stokastik.

Apa yang akan dibahas seri ini selanjutnya

Ini adalah Bagian 1 dari seri tiga bagian. Di Bagian 2: Logika Formal, Kebijakan Cedar, dan Ekonomi Verifikasi, kami akan membahas secara mendalam tentang: bagaimana kebijakan penalaran otomatis bekerja, bagaimana aturan bisnis Anda menjadi logika formal, seperti apa jalur verifikasi, dan ekonomi verifikasi matematis versus tim QA manual. Di Bagian 3: Playbook Implementasi Langkah demi Langkah, kami menyediakan panduan praktik langsung dengan pola kode siap produksi untuk mengintegrasikan pemeriksaan serta Kebijakan AR Batas Pengaman Bedrock di AgentCore ke dalam tumpukan Anda.


Harshvardhan Chunawala

Harshvardhan Chunawala

Harshvardhan Chunawala adalah Solutions Architect di AWS dan AWS Academy Authorized Educator, yang berbasis di Amerika Serikat. Beliau berpartner dengan para pimpinan korporasi besar, pendiri startup, dan eksekutif C-suite di seluruh dunia untuk merancang infrastruktur cloud yang dapat diskalakan serta aman di AWS di seluruh industri. Beliau adalah penerima penghargaan AWS Golden Jacket dan berkolaborasi di berbagai tim Amazon untuk membentuk dan memberikan kemampuan cloud terdepan di bidang keamanan, satelit, serta layanan AI agentik yang tepercaya. Di luar pekerjaannya di AWS, beliau adalah seorang teknolog dan ahli keamanan cloud yang diakui secara global dengan pengalaman lebih dari satu dekade. Beliau juga berafiliasi dengan Carnegie Mellon University, tempat beliau berkontribusi pada penelitian dan bimbingan dalam komputasi cloud serta teknologi baru. Jauh dari keyboard, beliau menikmati olahraga terjun payung dan menerbangkan pesawat.

Mike Miller

Mike Miller

Mike Miller adalah Director of AI Product Management di AWS, tempat beliau memberikan nasihat tentang inisiatif AI generatif utama, termasuk kemampuan penalaran otomatis untuk mencegah halusinasi, Amazon Q, dan Amazon Bedrock. Beliau memberikan PartyRock, playground no-code untuk membangun aplikasi AI generatif, ke publik setelah versi internalnya menjadi viral di kalangan karyawan Amazon. Sebelumnya, Mike memimpin tim Thought Leadership AWS Machine Learning, tempat beliau meluncurkan AWS DeepLens, AWS DeepRacer, dan AWS DeepComposer, menempatkan machine learning langsung ke tangan para developer di seluruh dunia dengan cara yang menyenangkan serta menarik. Mike telah bekerja di Amazon selama lebih dari 13 tahun, sebelumnya memimpin manajemen produk untuk Fire TV di Lab126 sebelum bergabung bersama AWS.

Rahul Kumar

Rahul Kumar

Dr. Rahul Kumar adalah Senior Applied Science Manager di AWS, tempat beliau memimpin upaya untuk membangun teknologi verifikasi untuk program Rust dan C serta memajukan AI neuro-simbolik yang menggabungkan model bahasa besar dengan penalaran otomatis. Di AWS, Rahul mendorong inisiatif sumber terbuka termasuk pemeriksa model Kani dan tantangan “Verifikasikan Keamanan Pustaka Standar Rust”. Beliau memegang gelar PhD dari Universitas Brigham Young serta sebelumnya bekerja di bidang verifikasi formal dan analisis statis di Microsoft Research, NASA JPL dan Dosen di Caltech. Beliau adalah pendukung setia untuk memberikan penalaran otomatis ke khalayak yang lebih luas, berbicara tentang bagaimana teknik pembuktian matematis dapat menghilangkan halusinasi AI serta menjamin kebenaran perangkat lunak. Beliau berdomisili di Seattle, Washington.

Stefano Buliani

Stefano Buliani

Stefano Buliani adalah Principal Product Manager di Automated Reasoning Group di AWS, tempat beliau memimpin upaya untuk memberikan kemampuan verifikasi formal ke AI generatif melalui Batas Pengaman Amazon Bedrock. Berlatar belakang sebagai rekayasawan perangkat lunak, Stefano telah bekerja di AWS selama lebih dari 12 tahun, menjabat sebagai arsitek solusi spesialis dan manajer produk di seluruh tim nirserver dan penalaran otomatis. Dalam perannya sebelumnya, beliau membantu pelanggan membangun dan menskalakan aplikasi nirserver di AWS Lambda dan Amazon API Gateway. Di luar pekerjaan, Stefano menikmati menjelajahi alam bebas di Pacific Northwest. Beliau berdomisili di Vancouver, Kanada.

Bagaimana konten ini?