3 citations · 4 across the 9 of their papers we have counts for
9 papers
The Problem Is the Problem: Towards Scalable Mathematical Discovery
Zeyu Zheng, Shengtong Zhang, Jeremy Avigad +2
AI systems are increasingly capable of contributing to mathematical research. In research practice, frontier-model reasoning is a limited resource, and expert mathematical review i…
Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization
Anmol Agarwal, Natalie Neamtu, Pranjal Aggarwal +6
AI coding agents are increasingly used to write real-world software, but ensuring that their outputs are correct remains a fundamental challenge. Formal verification offers a promi…
Explorable Proofs: Making Written Proofs Explorable by Grounding Them in Formal Representations
Hita Kambhamettu, Will Crichton, Sean Welleck +2
LLM-generated explanations can make technical content more accessible, but there is a ceiling on what they can support interactively. Because LLM outputs are static text, they cann…
AdaExplore: Failure-Driven Adaptation and Diversity-Preserving Search for Efficient Kernel Generation
Weihua Du, Jingming Zhuo, Yixin Dong +9
Recent large language model (LLM) agents have shown promise in using execution feedback for test-time adaptation. However, robust self-improvement remains far from solved: most app…
DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
Tate Rowney, Riyaz Ahuja, Jeremy Avigad +1
Domain-specific languages (DSLs) mediate interactions between interactive proof assistants and external automation, but translating between the prover's internal representation and…
LeanArchitect: Automating Blueprint Generation for Humans and AI
Thomas Zhu, Pietro Monticone, Jeremy Avigad +1
Large-scale formalization projects in Lean rely on blueprints: structured dependency graphs linking informal mathematical exposition to formal declarations. While blueprints are ce…
Premise Selection for a Lean Hammer
Thomas Zhu, Joshua Clune, Jeremy Avigad +2
Neural methods are transforming automated reasoning for proof assistants, yet integrating these advances into practical verification workflows remains challenging. A hammer is a to…
ImProver: Agent-Based Automated Proof Optimization
Riyaz Ahuja, Jeremy Avigad, Prasad Tetali +1
Large language models (LLMs) have been used to generate formal proofs of mathematical theorems in proofs assistants such as Lean. However, we often want to optimize a formal proof…
Efficient AUC Optimization for Information Ranking Applications
Sean J. Welleck
Adequate evaluation of an information retrieval system to estimate future performance is a crucial task. Area under the ROC curve (AUC) is widely used to evaluate the generalizatio…