9 posts
Verifikasi Cleanroom memerlukan pembuatan dan pelunasan kewajiban pembuktian. Berikut cara LLM mengotomatisasi anotasi dan pembuatan VC sehingga Anda bisa fokus pada pembuktian yang sebenarnya sulit.
Cleanroom software engineering menuntut agar Anda membuktikan kode Anda benar sebelum Anda mengompilasinya. Kedengarannya mulia sampai Anda menghabiskan tiga…
Saya menghabiskan 30 hari menulis penjelasan desain sebelum meminta kode ke LLM. Hasilnya mengubah cara saya berpikir tentang rubber-ducking.
Kebanyakan developer menggunakan LLM secara terbalik. Kita mendeskripsikan keinginan dalam lima kata, mendapatkan 200 baris kode, dan menghabiskan satu jam…
Percakapan LLM berisi niat, alternatif yang ditolak, dan kode yang berfungsi. Itulah sebenarnya yang seharusnya menjadi dokumentasi. Berikut cara mengubah obrolan yang fana menjadi dokumen yang tahan lama dan dapat dicari tanpa kehilangan narasi.
Anda menghabiskan empat puluh lima menit dengan Claude merancang sebuah retry circuit. Anda menjelaskan mode kegagalannya, menolak exponential backoff karena…
Inspeksi Fagan membutuhkan empat hingga enam orang dan dua jam untuk meninjau 250 baris. LLM dapat mengurangi biaya tersebut dengan menangani persiapan dan penegakan checklist, namun tidak dapat menggantikan peran manusia yang menemukan defect paling mahal.
Inspeksi Fagan penuh membutuhkan seorang moderator, seorang reader, dua hingga empat inspector, dan author. Tim menghabiskan dua jam untuk meninjau sekitar 250…
Model bahasa besar menulis kode Rust yang menakjubkan baiknya, tetapi ketika Anda meminta pembuktian formal, mereka menghasilkan invarian yang tidak ada dan menciptakan sintaks yang tidak diterima oleh verifikator apa pun. Berikut ini yang benar-benar mereka lakukan dengan benar, di mana mereka gagal, dan bagaimana menggunakannya meskipun begitu.
LLM dapat menulis Rust yang dikompilasi dan bahkan lulus . Apa yang tidak dapat mereka lakukan secara andal adalah menulis pembuktian formal bahwa kode…
LLM menghasilkan sintaks yang salah karena mereka melakukan sampling token secara probabilistik. Grammar-constrained decoding menyaring kosakata di setiap langkah sehingga hanya token yang mempertahankan validitas sintaksis yang dikeluarkan.
Minta LLM untuk menghasilkan objek JSON dan pada akhirnya ia akan mengeluarkan trailing comma, newline yang tidak di-escape di dalam string, atau bare word di…
Anda dapat menghasilkan design token dari deskripsi Bahasa Inggris sederhana, tetapi hanya jika Anda memperlakukan deskripsi tersebut sebagai DSL konteks terbatas dengan kontrak schema dan snapshot test.
Ya, Anda dapat mendeskripsikan sebuah tema dalam Bahasa Inggris dan mendapatkan design system yang berfungsi. Masalahnya adalah deskripsi dalam Bahasa Inggris…
Menjalankan beberapa LLM secara paralel menangkap kesalahan yang akan dengan percaya diri dikirim oleh model tunggal. Berikut cara membangun sistem resolusi ketidaksetujuan yang benar-benar berfungsi.
Anda mengirim prompt ke GPT-4o. Ia mengembalikan blob JSON dengan confidence 0,97. Anda mengirim prompt yang sama ke Claude 3.5 Sonnet. Ia mengembalikan blob…
N-version programming dengan LLM tidak memerlukan banyak model. Anda bisa mengekstrak implementasi yang beragam dan benar dari satu model dengan memvariasikan prompt, persona, dan constraint reasoning.
N-version programming berasumsi bahwa keragaman berasal dari penulis yang berbeda. Dengan LLM, itu berarti model yang berbeda, provider yang berbeda, mungkin…