TrojanSpec-Bench: An Adversarial Benchmark for LLM-Based Formal Specification Elicitation
收藏官方服务：
资源简介：
TrojanSpec-Bench is an adversarial benchmark for LLM-based formal specification elicitation. It contains 1,024 admitted triples across three verification languages (Dafny, Lean 4, Verus) and defines four attack patterns that inject subtle faults into elicited specifications. The atomic_monitor detector (K=2) reaches F1 0.967, a false positive rate of 0.068, outperforming a consensus baseline (F1 0.871) and MutDafny (F1 0.530). This record contains the benchmark dataset.
提供机构：
Zenodo创建时间：
2026-08-11
