5 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…
Measuring Psychological Depth in Language Models
Fabrice Harel-Canada, Hanyu Zhou, Sreya Muppalla +4
Evaluations of creative stories generated by large language models (LLMs) often focus on objective properties of the text, such as its style, coherence, and diversity. While these…