---
title: "LEANGUARD: Araç Kullanan Ajanlar İçin Lean ile Doğrulanmış Güvenlik Korkulukları"
url: https://blog.edumints.com/leanguard-arac-kullanan-ajanlar-icin-lean-ile-dogrulanmis-guvenlik
category: "LLM"
date: 2026-11-03T15:05:36.112Z
publisher: Edumints Blog
lang: tr-TR
source_name: "Hugging Face Papers"
source_url: https://huggingface.co/papers/2611.02332
---

# LEANGUARD: Araç Kullanan Ajanlar İçin Lean ile Doğrulanmış Güvenlik Korkulukları

## Araç Kullanan Ajanlarda Politika İhlali Sorunu ve LeanGuard Mimarisi

Araç kullanan (tool-using) dil modeli ajanları, çalışma sırasında sıklıkla alan politikalarının (domain policies) açıkça yasakladığı eylemleri yürütebilmektedir. Bu güvenlik ve güvenilirlik açığını kapatmak için geliştirilen **LeanGuard**, önerilen her araç çağrısını (tool call) henüz hedef ortama ulaşmadan önce **Lean4** dilinde yazılmış bir politikaya karşı denetleyen bir çalışma zamanı (runtime) katmanı sunar.

LeanGuard mimarisinin temel çalışma prensipleri şunlardır:

- **Zamansal Mantık ve Durum Önermeleri:** Politikalar, mevcut durum önermelerini (state predicates) yürütme geçmişi üzerindeki kapsamlı geçmiş zamanlı zamansal operatörlerle (scoped past-time temporal operators) birleştirir.
- **Güvenli Kapanma (Fail-Closed) ve Matematiksel Kanıt:** Değerlendirme süreci **fail-closed** (hata durumunda işlemi reddetme) prensibiyle çalışır ve karar prosedürünün **LeanLTL** semantiği ile eşdeğer olduğu matematiksel olarak kanıtlanmıştır.

## Reddedilen Çağrıları Düzeltme Mekanizmaları

LeanGuard tarafından engellenen bir araç çağrısı iki farklı yaklaşımla düzeltilebilir:

- **Geri Bildirim (Feedback) Yöntemi:** Ajana ihlal edilen kural ve bir ipucu (hint) geri gönderilerek modelin kendi çağrısını düzeltmesi sağlanır.
- **Kanıt Güdümlü Onarım (Proof-Guided Repair):** Modele tekrar başvurmaya gerek kalmaksızın, Lean metaprogramlama yetenekleri kullanılarak kullanıcının niyetini koruyan yakın bir alternatif çağrı aranır ve politikanın bu yeni çağrıya izin verdiği matematiksel olarak kanıtlanır.

## Deneysel Sonuçlar ve Performans Bulguları

Makaledeki test sonuçları, biçimsel doğrulama (formal verification) tabanlı korkulukların üretim ortamındaki etkisini net biçimde ortaya koymaktadır:

- **Tau-Bench Testleri:** Beş farklı Qwen modeli (0.8B ile 27B arası) üzerinde yapılan testlerde, korumasız ajanlar Lean politikasının yasakladığı en az **33 çağrıyı** yürütürken, **LeanGuard** hiçbir yasaklı çağrıya izin vermemiştir. Üstelik geri bildirim mekanizması kullanıldığında görev başarı oranında anlamlı bir düşüş yaşanmamıştır.
- **DTap ve Prompt Injection Koruması:** LeanGuard, doğrudan **prompt-injection** saldırılarının başarı oranını **%57,9'dan %5,9'a** düşürmüştür. İyi niyetli (benign) görevlerin yazma işlemi gerektirmediği telekom senaryolarında ise normal görev başarısı hiç değişmemiştir.
- **Geri Bildirim ve Hızlı Onarım Verimliliği:** Geri bildirim mekanizması, salt reddetmeye (bare denial) kıyasla tekrarlanan engellenmiş çağrıları azaltmış ve beş modelin dördünde görev başarısını artırmıştır. Yeniden oynatılan reddedilmelerde ise kanıt güdümlü onarım, argüman değerlerinden kaynaklanan **252 reddin 88'i** için kabul edilebilir bir düzenlemeyi medyan **2 ms** gibi çok düşük bir sürede kanıtlamıştır.

## Yazılım Geliştirme ve Mühendislik Çıkarımları

Modern yazılım mühendisliğinde **Tool Calling ve Multi-Step Agent'lar** geliştirirken ve **Production'da Agent Güvenilirliği** sağlarken yalnızca prompt tabanlı kısıtlamalara güvenmek yetersizdir:

- **Deterministik Çalışma Zamanı Katmanı:** LLM çıktıları olasılıksal olduğu için kritik API çağrılarının önüne deterministik ve **fail-closed** çalışan bir doğrulama katmanı eklenmelidir.
- **Yapılandırılmış Hata Dönüşleri:** Bir araç çağrısı engellendiğinde ajana sadece "reddedildi" demek yerine hangi kuralın ihlal edildiğini açıklayan geri bildirimler dönmek, döngüsel hataları önler ve görev başarısını korur.
- **Düşük Gecikmeli Otomatik Onarım:** Parametre kaynaklı hataları LLM'e yeniden sormak yerine kural tabanlı veya biçimsel doğrulama yöntemleriyle milisaniyeler içinde (örneğin 2 ms) onarmak, hem token maliyetini hem de sistem gecikmesini ciddi ölçüde azaltır.

---

**Kaynak:** Hugging Face Papers (https://huggingface.co/papers/2611.02332)
**Yayıncı:** [Edumints Blog](https://blog.edumints.com) · Alıntılarken bu URL'ye bağlantı verin: https://blog.edumints.com/leanguard-arac-kullanan-ajanlar-icin-lean-ile-dogrulanmis-guvenlik