Tag
Introduces LCS-Bench, a theory-scale benchmark for auto-formalization of logics for computer science, covering 327 textbook items over 4,076 Lean declarations. Evaluation on 14 models shows the benchmark is challenging, with SOTA models achieving only 20.1% on auto-formalization tasks.