2 citations · 2 across the 9 of their papers we have counts for
9 papers · 1 filter
Autoformalizing Argumentative Material Inferences
Xin Quan, Reto Gubelmann, André Freitas
Natural language arguments are compelling before they are formally explicit. A premise supports a claim through defeasible warrants, background commitments, and exception condition…
AbstRAG: Learning to Abstract for Retrieval Problems
Lei Xu, Xin Quan, Daniel Pedronette +1
Retrieval-augmented generation often fails when the query, the document evidence, and the user's intent are expressed at different levels of abstraction. A query may ask about a cl…
Reasoning without Gold Standards: A Proxy-Judge Theory of Autoformalization
Lei Xu, Xin Quan, André Freitas
Autoformalization (AF) requires both prover acceptance and fidelity to an informal source, but prover acceptance alone cannot establish fidelity, and expert-validated reference for…
Decompose-and-Formalise: Recursively Verifiable Natural Language Inference
Xin Quan, Marco Valentino, Louise A. Dennis +1
Recent work has shown that integrating large language models (LLMs) with theorem provers (TPs) in neuro-symbolic pipelines helps with entailment verification and proof-guided refin…
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…