LEANGUARD: Đường dây bảo vệ được kiểm tra mỏng cho các agent sử dụng công cụ

Đoạn trích bài viết

Các agent mô hình ngôn ngữ sử dụng công cụ thường thực hiện các hành động mà chính sách miền của họ cấm. Chúng tôi giới thiệu LeanGuard, một runtime kiểm tra mọi cuộc gọi công cụ được đề xuất so với một chính sách được viết trong Lean4 trước khi cuộc gọi đạt đến môi trường. Các chính sách kết hợp các dự đoán trạng thái với phạm vi thời gian quá khứ o.