2 citations · 3 across the 9 of their papers we have counts for
9 papers
FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean
Jordan Meadows, Lan Zhang, Andre Freitas
Formalising informal mathematical reasoning into formally verifiable code is a significant challenge for large language models. In scientific fields such as physics, domain-specifi…
Monotonic Reference-Free Refinement for Autoformalization
Lan Zhang, Marco Valentino, André Freitas
While statement autoformalization has advanced rapidly, full-theorem autoformalization remains largely unexplored. Existing iterative refinement methods in statement autoformalizat…
MASA: LLM-Driven Multi-Agent Systems for Autoformalization
Lan Zhang, Marco Valentino, André Freitas
Autoformalization serves a crucial role in connecting natural language and formal reasoning. This paper presents MASA, a novel framework for building multi-agent systems for autofo…
Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning
Lan Zhang, Marco Valentino, Jordan Meadows +1
Statement autoformalization plays a crucial role in formal mathematical reasoning by enabling the automatic translation of natural language statements into formal languages. While…
Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions
Lan Zhang, Marco Valentino, Andre Freitas
Thanks to their linguistic capabilities, LLMs offer an opportunity to bridge the gap between informal mathematics and formal languages through autoformalization. However, it is sti…
Consistent Autoformalization for Constructing Mathematical Libraries
Lan Zhang, Xin Quan, Andre Freitas
Autoformalization is the task of automatically translating mathematical content written in natural language to a formal language expression. The growing language interpretation cap…
Multi-Operational Mathematical Derivations in Latent Space
Marco Valentino, Jordan Meadows, Lan Zhang +1
This paper investigates the possibility of approximating multiple mathematical operations in latent space for expression derivation. To this end, we introduce different multi-opera…
The Neglected Sibling: Isotropic Gaussian Posterior for VAE
Lan Zhang, Wray Buntine, Ehsan Shareghi
Deep generative models have been widely used in several areas of NLP, and various techniques have been proposed to augment them or address their training challenges. In this paper,…
Unsupervised Representation Disentanglement of Text: An Evaluation on Synthetic Datasets
Lan Zhang, Victor Prokhorov, Ehsan Shareghi
To highlight the challenges of achieving representation disentanglement for text domain in an unsupervised setting, in this paper we select a representative set of successfully app…