rust-djinn: Bạn Nên Định Nghĩa Mã Của Mình Một Cách Không Mơ Hồ (và Chứng Minh Điều Đó)

Tôi có một chương trình biến ước mơ thành hiện thực, miễn là tôi có thể nêu chúng một cách chính xác. Thay vì triển khai một hàm Rust, tôi mô tả những gì nó nên làm, và Djinn sẽ viết mã chứng minh rõ ràng rằng nó thực sự làm đúng như vậy. Giả sử tôi muốn sắp xếp một danh sách. Tôi viết: Djinn của tôi không phải là phép màu, nhưng nó là hiện thân của một giấc mơ. Mọi người đã mong muốn có điều gì đó giống như thế này rất lâu rồi: con người viết ra các đặc tả, sau đó dùng LLM để triển khai và chứng minh với một bộ xác minh rằng các bản triển khai của họ là chính xác. Lý thuyết thì sự kết hợp LLM-verifier này rất mạnh mẽ (nhờ LLM), nhưng vẫn an toàn và đáng tin cậy để bạn không cần phải đọc mã kết quả (nhờ bộ xác minh). Trong thực tế, nó hơi khó hơn so với nghe có vẻ. Trong khi bộ xác minh cung cấp sự chắc chắn rằng mã của LLM khớp với đặc tả của chúng ta, thì dễ dàng gây ra lỗi trong đặc tả hoặc mô tả chưa đầy đủ. Ngoài ra, bạn phải thiết lập phần mềm xác minh (và thiết lập ranh giới tin cậy), vận hành nhiều ngôn ngữ khác nhau, và trông chờ các agent. Để điều này thành công, nó cần trở nên khả thi với các SWE thông thường, và hiện tại nó vẫn là một cơn đau ngay cả đối với các chuyên gia phương pháp hình thức. Nếu chỉ có một cách dễ dàng để mọ người viết các đặc tả hình thức trong một định dạng tương đối quăm quẫn, sử dụng LLM để triển khai và tối ưu mã, và kết hợp mã kết quả với dự án thông thường của họ? Một cách mà còn hoạt động ngay cả với những người không muốn chạm vào mã Lean trực tiếp hay không tin tưởng bản thân mình viết một đặc tả hoàn hảo ngay trên lần đầu tiên?