LeanGuard: kiểm tra từng lệnh gọi công cụ của agent LLM bằng chính sách viết trong Lean 4
Nhóm tác giả (Sankar, Ganguly, Singh và cộng sự) đề xuất LeanGuard, một runtime kiểm tra mọi lệnh gọi công cụ mà agent đề xuất theo chính sách viết bằng Lean 4 trước khi lệnh tới môi trường; hệ thống từ chối mặc định (fail-closed). Trên Tau-Bench với năm mô hình Qwen (0,8B–27B), các agent không có bảo vệ thực thi ít nhất 33 lệnh mà chính sách cấm, còn LeanGuard thực thi 0 lệnh; trên DTap, tỉ lệ prompt-injection trực tiếp thành công giảm từ 57,9% xuống 5,9%. Với các lệnh bị từ chối do giá trị tham số, cơ chế sửa có chứng minh tìm được bản chỉnh hợp lệ cho 88 trên 252 trường hợp.
Nguồn: arXiv
Cần chatbot hoặc agent LLM cho doanh nghiệp?
Mô tả ngắn yêu cầu của bạn; bạn sẽ nhận câu hỏi làm rõ và đề xuất phạm vi trước khi bắt đầu.
Tin liên quan
AI & LLM · 2026-11-04
Tencent ra mắt Hy4: lần đầu có thị giác và điều khiển máy tính, nhắm tới nhóm mô hình mở mạnh nhất
AI & LLM · 2026-11-03
Strategist: meta-agent tự tiến hoá chiến lược suy luận dưới dạng mã, giảm 39% chi phí suy luận
AI & LLM · 2026-11-03