3 papers
cs.CL2026
Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean
Kári Rögnvaldsson, Chenhao Sun, Jasper Dekoninck +1
Large language models (LLMs) are increasingly used in workflows for generating formal proofs in Lean. These workflows often decompose problems into smaller lemmas, sample many proo…
cs.LG2025
Dual Randomized Smoothing: Beyond Global Noise Variance
Chenhao Sun, Yuhao Mao, Martin Vechev
Randomized Smoothing (RS) is a prominent technique for certifying the robustness of neural networks against adversarial perturbations. With RS, achieving high accuracy at small rad…
cs.LG2024
Average Certified Radius is a Poor Metric for Randomized Smoothing
Chenhao Sun, Yuhao Mao, Mark Niklas Müller +1
Randomized smoothing (RS) is popular for providing certified robustness guarantees against adversarial attacks. The average certified radius (ACR) has emerged as a widely used metr…