43 citations · 151 across the 29 of their papers we have counts for
30 papers
Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification
Joshua Ong Jun Leang, Haonan Li, Zheng Zhao +7
Most of mathematical knowledge has been communicated through so-called informal use of mathematics and natural language. With large language models (LLMs) being highly adept in usi…
FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation
Rob Cornish, Iacopo Ghinassi, Po-Hung Yeh +7
Autoformalisation (AF) systems map natural language reasoning steps into formal statements in a proof assistant such as Lean. We consider how to assess the faithfulness of these sy…
AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language
Qiyuan Xu, Joshua Ong Jun Leang, Renxi Wang +4
Interactive theorem proving (ITP) underpins program verification and formalized mathematics, but its manual effort limits scalability. LLM-based proof agents promise to ease this e…
Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation
Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian +5
Modern Lean theorem provers achieve strong performance only with substantial training and inference compute, driven in part by scarce verified proof data and the long reasoning tra…
Specialize Roles, Mix Deployments: Pushing the Cost-Accuracy Frontier of LLM Agent Teams
Yinsicheng Jiang, Liang Cheng, Yeqi Huang +6
LLM agents are increasingly deployed as multi-role teams, where tasks are divided across specialized roles such as planner, executor, and verifier. In these systems, cost and accur…
Hierarchical Alignment: Enforcing Hierarchical Instruction-Following in LLMs through Logical Consistency
Shu Yang, Zihao Zhou, Di Wang +1
Large language models increasingly operate under multiple instructions from heterogeneous sources with different authority levels, including system policies, user requests, tool ou…
Can I Have Your Order? Monte-Carlo Tree Search for Slot Filling Ordering in Diffusion Language Models
Joshua Ong Jun Leang, Yu Zhao, Mihaela Cătălina Stoian +3
While plan-and-infill decoding in Masked Diffusion Models (MDMs) shows promise for mathematical and code reasoning, performance remains highly sensitive to slot infilling order, of…
Neural Theorem Proving for Verification Conditions: A Real-World Benchmark
Qiyuan Xu, Xiaokun Luan, Renxi Wang +5
Theorem proving is fundamental to program verification, where the automated proof of Verification Conditions (VCs) remains a primary bottleneck. Real-world program verification fre…
Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
Junqi Liu, Zihao Zhou, Zekai Zhu +10
Agentic systems have recently become the dominant paradigm for formal theorem proving, achieving strong performance by coordinating multiple models and tools. However, existing app…
PiCSAR: Probabilistic Confidence Selection And Ranking for Reasoning Chains
Joshua Ong Jun Leang, Zheng Zhao, Aryo Pradipta Gema +7
Best-of-n sampling improves the accuracy of large language models (LLMs) and large reasoning models (LRMs) by generating multiple candidate solutions and selecting the one with the…
APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries
Huajian Xin, Luming Li, Xiaoran Jin +2
While frontier formal mathematics systems now routinely develop repository-scale proof engineering artifacts requiring multi-file coordination and semantic correctness beyond compi…
Theorem Prover as a Judge for Synthetic Data Generation
Joshua Ong Jun Leang, Giwon Hong, Wenda Li +1
The demand for synthetic data in mathematical reasoning has increased due to its potential to enhance the mathematical capabilities of large language models (LLMs). However, ensuri…
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…
End-to-End Ontology Learning with Large Language Models
Andy Lo, Albert Q. Jiang, Wenda Li +1
Ontologies are useful for automatic machine processing of domain knowledge as they represent it in a structured format. Yet, constructing ontologies requires substantial manual eff…
Repurposing Language Models into Embedding Models: Finding the Compute-Optimal Recipe
Alicja Ziarko, Albert Q. Jiang, Bartosz Piotrowski +3
Text embeddings are essential for many tasks, such as document retrieval, clustering, and semantic similarity assessment. In this paper, we study how to contrastively train text em…
Proving Theorems Recursively
Haiming Wang, Huajian Xin, Zhengying Liu +8
Recent advances in automated theorem proving leverages language models to explore expanded search spaces by step-by-step proof generation. However, such approaches are usually base…
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
Huajian Xin, Daya Guo, Zhihong Shao +6
Proof assistants like Lean have revolutionized mathematical proof verification, ensuring high accuracy and reliability. Although large language models (LLMs) show promise in mathem…
Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization
Jin Peng Zhou, Charles Staats, Wenda Li +3
Large language models (LLM), such as Google's Minerva and OpenAI's GPT families, are becoming increasingly capable of solving mathematical quantitative reasoning problems. However,…
Multilingual Mathematical Autoformalization
Albert Q. Jiang, Wenda Li, Mateja Jamnik
Autoformalization is the task of translating natural language materials into machine-verifiable formalisations. Progress in autoformalization research is hindered by the lack of a…
Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving
Xueliang Zhao, Wenda Li, Lingpeng Kong
Large language models~(LLMs) present an intriguing avenue of exploration in the domain of formal theorem proving. Nonetheless, the full utilization of these models, particularly in…
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
Albert Q. Jiang, Sean Welleck, Jin Peng Zhou +6
The formalization of existing mathematical proofs is a notoriously difficult process. Despite decades of research on automation and proof assistants, writing formal proofs remains…
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…
Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types
Anthony Bordg, Lawrence Paulson, Wenda Li
Church's simple type theory is often deemed too simple for elaborate mathematical constructions. In particular, doubts were raised whether schemes could be formalized in this setti…