13 citations · 27 across the 16 of their papers we have counts for
17 papers
Long-Horizon AI Research for Grothendieck Constant: A Case Study in Human-AI Mathematical Collaboration
Alan Li, Rahul Saha, Anton Xue +4
AI agents are increasingly used in mathematics research, but it is often unclear how to use them effectively. Towards this, we present an extensive case study of how AI was used to…
Cost-Aware Optimization for Agentic Query Execution
Lunyiu Nie, Yilin Xia, Yiren Liu +2
Classical query optimization searches over algebraically equivalent plans that differ only in cost. This assumption breaks once LLM-backed operators enter the picture: their placem…
When Parallelism Pays Off: Cohesion-Aware Task Partitioning for Multi-Agent Coding
Xu Yang, Lunyiu Nie, Ethan Chandra +3
Multi-agent Large Language Model (LLM) systems offer a way to decompose complex tasks, such as coding, through parallelization and context isolation. However, adding agents in prac…
An Improved Last-Iterate Convergence Rate for Anchored Gradient Descent Ascent
Anja Surina, Arun Suggala, George Tsoukalas +5
We analyze the last-iterate convergence of the Anchored Gradient Descent Ascent algorithm for smooth convex-concave min-max problems. While previous work established a last-iterate…
FormulaCode: Evaluating Agentic Optimization on Large Codebases
Atharva Sehgal, James Hou, Akanksha Sarkar +4
Large language model (LLM) coding agents increasingly operate at the repository level, motivating benchmarks that evaluate their ability to optimize entire codebases under realisti…
CSLib: The Lean Computer Science Library
Clark Barrett, Swarat Chaudhuri, Fabrizio Montesi +5
We introduce CSLib, an open-source framework for proving computer-science-related theorems and writing formally verified code in the Lean proof assistant. CSLib aims to be for comp…
Learning Interestingness in Automated Mathematical Theory Formation
George Tsoukalas, Rahul Saha, Amitayush Thakur +2
We take two key steps in automating the open-ended discovery of new mathematical theories, a grand challenge in artificial intelligence. First, we introduce , a rein…
Lean Finder: Semantic Search for Mathlib That Understands User Intents
Jialin Lu, Kye Emond, Kaiyu Yang +3
We present Lean Finder, a semantic search engine for Lean and mathlib that understands and aligns with the intents of mathematicians. Progress in formal theorem proving is often hi…
AlphaEvolve: A coding agent for scientific and algorithmic discovery
Alexander Novikov, Ngân Vũ, Marvin Eisenberger +15
In this white paper, we present AlphaEvolve, an evolutionary coding agent that substantially enhances capabilities of state-of-the-art LLMs on highly challenging tasks such as tack…
CLEVER: A Curated Benchmark for Formally Verified Code Generation
Amitayush Thakur, Jasper Lee, George Tsoukalas +6
We introduce , a high-quality, curated benchmark of 161 problems for end-to-end verified code generation in Lean. Each problem consists of (1) the task of ge…
ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
Amitayush Thakur, George Tsoukalas, Greg Durrett +1
Neural approaches to theorem proving require robust infrastructure for interfacing with interactive theorem provers (ITPs), extracting structured proof data, and executing proof se…
Formal Mathematical Reasoning: A New Frontier in AI
Kaiyu Yang, Gabriel Poesia, Jingxuan He +4
AI for Mathematics (AI4Math) is not only intriguing intellectually but also crucial for AI-driven discovery in science, engineering, and beyond. Extensive efforts on AI4Math have m…
Synthesize, Partition, then Adapt: Eliciting Diverse Samples from Foundation Models
Yeming Wen, Swarat Chaudhuri
Presenting users with diverse responses from foundation models is crucial for enhancing user experience and accommodating varying preferences. However, generating multiple high-qua…
PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
George Tsoukalas, Jasper Lee, John Jennings +5
We present PutnamBench, a new multi-language benchmark for evaluating the ability of neural theorem-provers to solve competition mathematics problems. PutnamBench consists of 1692…
Grounding Data Science Code Generation with Input-Output Specifications
Yeming Wen, Pengcheng Yin, Kensen Shi +3
Large language models (LLMs) have recently demonstrated a remarkable ability to generate code from natural language (NL) prompts. However, in the real world, NL is often too ambigu…
Batched Low-Rank Adaptation of Foundation Models
Yeming Wen, Swarat Chaudhuri
Low-Rank Adaptation (LoRA) has recently gained attention for fine-tuning foundation models by incorporating trainable low-rank matrices, thereby reducing the number of trainable pa…
An In-Context Learning Agent for Formal Theorem-Proving
Amitayush Thakur, George Tsoukalas, Yeming Wen +2
We present an in-context learning agent for formal theorem-proving in environments like Lean and Coq. Current state-of-the-art models for the problem are finetuned on environment-s…