43 citations · 63 across the 2 of their papers we have counts for
5 papers
Autoformalization with Large Language Models
Yuhuai Wu, Albert Q. Jiang, Wenda Li +4
Autoformalization is the process of automatically translating from natural language mathematics to formal specifications and proofs. A successful autoformalization system could adv…
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
Albert Q. Jiang, Wenda Li, Szymon Tworkowski +5
In theorem proving, the task of selecting useful premises from a large library to unlock the proof of a given conjecture is crucially important. This presents a challenge for all t…
IsarStep: a Benchmark for High-level Mathematical Reasoning
Wenda Li, Lei Yu, Yuhuai Wu +1
A well-defined benchmark is essential for measuring and accelerating research progress of machine learning models. In this paper, we present a benchmark for high-level mathematical…
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem
Wenda Li, Lawrence C. Paulson
Many problems in computer algebra and numerical analysis can be reduced to counting or approximating the real roots of a polynomial within an interval. Existing verified root-count…
Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL
Wenda Li, Lawrence C. Paulson
In complex analysis, the winding number measures the number of times a path (counter-clockwise) winds around a point, while the Cauchy index can approximate how the path winds. We…