TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models (2023.emnlp-main)
Copied to clipboard
Jing Xiong, Jianhao Shen, Ye Yuan, Haiming Wang, Yichun Yin, Zhengying Liu, Lin Li, Zhijiang Guo, Qingxing Cao, Yinya Huang, Chuanyang Zheng, Xiaodan Liang, Ming Zhang, Qun Liu
| Challenge: | Automated theorem proving (ATP) benchmarks focus on symbolic inference but rarely involve understanding complex number combination reasoning. |
| Approach: | They propose a benchmark that requires a model to reduce a trigonometric expression with step-by-step proof and evaluates a generative LM’s reasoning ability on formulas and ability to manipulate, group, and factor number terms. |
| Outcome: | The proposed benchmark evaluates a generative LM’s reasoning ability on formulas and ability to manipulate, group, and factor number terms. |
Similar Papers
ATG: Benchmarking Automated Theorem Generation for Generative Language Models (2024.findings-naacl)
Copied to clipboard
| Challenge: | Existing generative language models (LMs) can generate new or reusable theorems, but their ability to generate new theorels is under-explored. |
| Approach: | They propose to use Metamath library to generate new theorems that can be saved as reusable knowledge for future theoretical proving. |
| Outcome: | The proposed benchmark evaluates whether an agent can generate valuable (and possibly brand new) theorems that are applicable for downstream theoretic proving as reusable knowledge. |
From Informal to Formal – Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs (2025.acl-long)
Copied to clipboard
Jialun Cao, Yaojie Lu, Meiziniu Li, Haoyang Ma, Haokun Li, Mengda He, Cheng Wen, Le Sun, Hongyu Zhang, Shengchao Qin, Shing-Chi Cheung, Cong Tian
| Challenge: | Recent studies in formal mathematical reasoning have shown an unstoppable growth trend. |
| Approach: | They constructed 18k high-quality instruction-response pairs across five mainstream formal specification languages and evaluated them against ten open-sourced LLMs. |
| Outcome: | The proposed model compared instruction-response pairs across five formal specification languages and found that the LLMs were good at writing proof segments when given either the code, or the detailed description of proof steps. |
Neural Unification for Logic Reasoning over Natural Language (2021.findings-emnlp)
Copied to clipboard
| Challenge: | Automated Theorem Proving (ATP) is a computer program that can show that conjectures are logical consequences of a set of axioms. |
| Approach: | They propose a transformer-based architecture for deriving conjectures given axioms . they propose 'neural unifier' and relative training procedure to train the model . |
| Outcome: | The proposed architectures are able to answer queries with deep queries with a relatively low training time. |
TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts (2024.emnlp-main)
Copied to clipboard
| Challenge: | a framework for formal proof writing using formal languages like Lean4 is needed to prove mathematical theorems using formal language. |
| Approach: | They propose a framework that trains a general-purpose LLM to be a Lean4 expert. |
| Outcome: | The proposed framework achieves cumulative accuracies of 36.48% and 33.61% on MiniF2F-Valid and Test datasets. |
Theorem Prover as a Judge for Synthetic Data Generation (2025.acl-long)
Copied to clipboard
| Challenge: | Recent studies show that large language models are increasingly capable of tackling mathematical problems. |
| Approach: | They propose an approach that iteratively refines theorem prover formalisation to mitigate errors. |
| Outcome: | The proposed method increases execution rate on the Lean prover from 60% to 87%, while human annotation is replaced with theorem prover feedback. |
Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4 (2026.acl-long)
Copied to clipboard
Chengwu Liu, Yichun Yin, Ye Yuan, Jiaxuan Xie, Botao Li, Siqi Li, Jianhao Shen, Yan Xu, Lifeng Shang, Ming Zhang
| Challenge: | Existing approaches to solving mathematical problems fall into two broad categories: informal methods and formal methods. |
| Approach: | They propose to use LLM natural-language reasoning to discover answers . they introduce Discover And Prove framework that rewrites Hard Mode statements into Easy Mode ones for existing ATP provers. |
| Outcome: | The proposed framework can be used to prove hard mode statements on ATP benchmarks. |
LLM-Powered Benchmark Factory: Reliable, Generic, and Efficient (2026.acl-long)
Copied to clipboard
Peiwen Yuan, Shaoxiong Feng, Yiwei Li, Xinglin Wang, Yueqi Zhang, Jiayi Shi, Chuyi Tan, Boyuan Pan, Yao Hu, Kan Li
| Challenge: | Using generic and efficient benchmark generators, human annotators are limited by inefficiency . current benchmark generator methods rely on seed signals, leading to long cycles and high costs . |
| Approach: | They propose a framework to evaluate LLMs as generic benchmark generators and integrate them as BenchMaker. |
| Outcome: | The proposed framework achieves comparable performance to human-annotated benchmarks on most metrics. |
TritonBench: Benchmarking Large Language Model Capabilities for Generating Triton Operators (2025.findings-acl)
Copied to clipboard
Jianling Li, ShangZhan Li, Zhenye Gao, Qi Shi, Yuxuan Li, Zefan Wang, Jiacheng Huang, WangHaojie WangHaojie, Jianrong Wang, Xu Han, Zhiyuan Liu, Maosong Sun
| Challenge: | Triton is a high-level Python-like programming language for building efficient GPU kernels. |
| Approach: | They propose a TritonBench benchmark that provides a comprehensive evaluation of Tritonic operators on widely deployed GPUs. |
| Outcome: | The proposed benchmarks show that current LLMs struggle to generate efficient Triton operators on widely deployed GPUs aligned with industry applications. |
Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations (2025.acl-long)
Copied to clipboard
| Challenge: | Recent work has shown that the interaction of large language models (LLMs) with theorem provers (TPs) can help verify and improve the validity of NLI explanations. |
| Approach: | They propose to use logical expressions to guide LLMs in generating structured proof sketches and to use them to improve their accuracy. |
| Outcome: | The proposed strategies improve autoformalisation, syntactic errors and explanation refinement over the state-of-the-art model. |
LILA: A Unified Benchmark for Mathematical Reasoning (2022.emnlp-main)
Copied to clipboard
Swaroop Mishra, Matthew Finlayson, Pan Lu, Leonard Tang, Sean Welleck, Chitta Baral, Tanmay Rajpurohit, Oyvind Tafjord, Ashish Sabharwal, Peter Clark, Ashwin Kalyan
| Challenge: | Towards evaluating and improving AI systems in this domain, we propose a mathematical reasoning benchmark based on 23 diversetasks . |
| Approach: | They propose a mathematical reasoning benchmark that includes 23 diverse tasks . they extend the benchmark by collecting task instructions and solutions in the form of Python programs . |
| Outcome: | The proposed model improves on multi-tasking while the best performing model only achieves 60.40%. |