3 citations · 5 across the 4 of their papers we have counts for
4 papers
Vero: Can AI Agents Build Formally Verified Software Repositories?
Zhe Ye, Hantao Lou, Yuechun Sun +8
AI agents are increasingly used for programming, but do not provide any guarantee on the correctness of generated code. Verified code generation, in which an agent produces both an…
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…
VERINA: Benchmarking Verifiable Code Generation
Zhe Ye, Zhengxu Yan, Jingxuan He +3
Large language models (LLMs) are increasingly integrated in software development, but ensuring correctness in LLM-generated code remains challenging and often requires costly manua…
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…