4 papers
From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
Eric Jiang, Xiao Liang, Yikai Zhang +16
Recent developments in AI for Mathematics (AI4Math), especially Large Language Model (LLM)-driven theorem provers, has achieved remarkable success in formal proof generation for we…
SLAM: Structural Linguistic Activation Marking for Language Models
Fabrice Harel-Canada, Amit Sahai
LLM watermarks must be detectable without compromising text quality, yet most existing schemes bias the next-token distribution and pay for detection with measurable quality loss.…
TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?
Alexander K Taylor, Junyi Zhang, Ethan Ji +10
Automated theorem proving (ATP) benchmarks largely consist of problems formalized in MathLib, so current ATP training and evaluation are heavily biased toward MathLib's definitiona…
Sandcastles in the Storm: Revisiting the (Im)possibility of Strong Watermarking
Fabrice Y Harel-Canada, Boran Erol, Connor Choi +4
Watermarking AI-generated text is critical for combating misuse. Yet recent theoretical work argues that any watermark can be erased via random walk attacks that perturb text while…