activity
20242026
most citedConsistent Autoformalization for Constructing Mathematical Libraries

2 citations · 2 across the 9 of their papers we have counts for

collaborators
Showing 2026Show all

6 papers · 1 filter

cs.CL2026

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…

cs.AI2026

SciR: A Controllable Benchmark for Scientific Reasoning in LLMs

Pierre Beckmann, Marco Valentino, Andre Freitas

Three paradigmatic forms of inference recur across scientific reasoning: deduction, induction, and causal abduction. Reliably evaluating LLMs on these in scientific settings is cur…

cs.CL2026

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…

cs.CL2026

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…

cs.CL2026

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…

cs.CL2026

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…