MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics

31 August 2021

Papers citing "MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics"

50 / 110 papers shown

Title
CLEVER: A Curated Benchmark for Formally Verified Code Generation Amitayush Thakur Jasper Lee George Tsoukalas Meghana Sistla Matthew Zhao Stefan Zetzsche Greg Durrett Yisong Yue Swarat Chaudhuri ALM 7 0 0 20 May 2025
Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities Haoyu Zhao Yihan Geng Shange Tang Yong Lin Bohan Lyu Hongzhou Lin Chi Jin Sanjeev Arora 9 0 0 19 May 2025
LEXam: Benchmarking Legal Reasoning on 340 Law Exams Yu Fan Jingwei Ni Jakob Merane Etienne Salimbeni Yang Tian ... Mrinmaya Sachan Alexander Stremitzer Christoph Engel Elliott Ash Joel Niklaus AILaw ELM 26 0 0 19 May 2025
LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation Junyu Lai Jiakun Zhang Shuo Xu Taolue Chen Zihang Wang Yao Yang Jiarui Zhang Chun Cao Jingwei Xu 7 0 0 17 May 2025
MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation Zhenwen Liang Linfeng Song Yang Li Tao Yang Feng Zhang Haitao Mi Dong Yu LRM 17 0 0 16 May 2025
Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving Qi Liu Xinhao Zheng Renqiu Xia Xingzhi Qi Qinxiang Cao Junchi Yan AIMat 52 0 0 07 May 2025
CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics Jiaheng Liu Xiaohan Lin Jonas Bayer Yael Dillies Weijie Jiang ... Zhengfeng Yang J. Zhang Lihong Zhi J. Li Zhengying Liu 126 1 0 06 May 2025
FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models Zhouliang Yu Ruotian Peng Keyi Ding Y. K. Li Zhongyuan Peng ... Huajian Xin Yifan Jiang Yandong Wen Ge Zhang Weiyang Liu LRM 152 1 0 05 May 2025
APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries Huajian Xin Luming Li Xiaoran Jin Jacques Fleuriot Wenda Li AIMat 61 0 0 27 Apr 2025
Hierarchical Attention Generates Better Proofs Jianlong Chen Chao Li Yang Yuan Andrew Chi-Chih Yao AIMat LRM 33 0 0 27 Apr 2025
Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification Balaji Rao William Eiers Carlo Lipizzi 37 0 0 23 Apr 2025
Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning Haiming Wang Mert Unsal Xiaohan Lin Mantas Baksys Jiaheng Liu ... Zhouliang Yu Zihan Wang Zhilin Yang Zhengying Liu Jia-Nan Li AIMat ReLM AI4TS LRM 59 8 0 15 Apr 2025
Reasoning Models Can Be Effective Without Thinking Wenjie Ma Jingxuan He Charlie Snell Tyler Griggs Sewon Min Matei A. Zaharia ReLM LRM 52 8 1 14 Apr 2025
Leanabell-Prover: Posttraining Scaling in Formal Reasoning Jingyuan Zhang Qi Wang Xingguang Ji Yong-Jin Liu Yang Yue Fuzheng Zhang Di Zhang Guorui Zhou Kun Gai LRM 44 4 0 08 Apr 2025
Brains vs. Bytes: Evaluating LLM Proficiency in Olympiad Mathematics Hamed Mahdavi Alireza Hashemi Majid Daliri Pegah Mohammadipour Alireza Farhadi Samira Malek Yekta Yazdanifard Amir Khasahmadi V. Honavar ELM LRM 66 1 0 01 Apr 2025
Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad Ivo Petrov Jasper Dekoninck Lyuben Baltadzhiev Maria Drencheva Kristian Minchev Mislav Balunović Nikola Jovanović Martin Vechev LRM ELM 70 11 0 27 Mar 2025
Rosetta-PL: Propositional Logic as a Benchmark for Large Language Model Reasoning Shaun Baek Shaun Esua-Mensah Cyrus Tsui Sejan Vigneswaralingam Abdullah Alali Michael Lu Vasu Sharma Sean O'Brien Kevin Zhu LRM 60 0 0 25 Mar 2025
A Survey on Mathematical Reasoning and Optimization with Large Language Models Ali Forootani OffRL LRM AI4CE 45 0 0 22 Mar 2025
MA-LoT: Multi-Agent Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving Ruida Wang Rui Pan Yuxin Li Jipeng Zhang Yizhen Jia Shizhe Diao Renjie Pi Junjie Hu Tong Zhang LRM LLMAG 95 6 0 05 Mar 2025
FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4 Jiarui Yao Ruida Wang Tong Zhang LRM 65 0 0 05 Mar 2025
From Hypothesis to Publication: A Comprehensive Survey of AI-Driven Research Support Systems Zekun Zhou Xiaocheng Feng L. Huang Xiachong Feng Ziyun Song ... Baoxin Wang Dayong Wu Guoping Hu Ting Liu Bing Qin AI4TS 77 1 0 03 Mar 2025
CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization Shuming Shi Ruobing Zuo Gaolei He Jianlin Wang Chenyang Xu Zhengfeng Yang 65 0 0 25 Feb 2025
A Survey on Feedback-based Multi-step Reasoning for Large Language Models on Mathematics Ting-Ruen Wei Haowei Liu Xuyang Wu Yi Fang LRM AI4CE ReLM KELM 220 1 0 21 Feb 2025
Activation Steering in Neural Theorem Provers Shashank Kirtania LLMSV 196 0 0 21 Feb 2025
Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques Sangjun Han Taeil Hur Youngmi Hur Kathy Sangkyung Lee Myungyoon Lee Hyojae Lim 159 0 0 20 Feb 2025
Theoretical Physics Benchmark (TPBench) -- a Dataset and Study of AI Reasoning Capabilities in Theoretical Physics Daniel J.H. Chung Zhiqi Gao Yurii Kvasiuk Tianyi Li Moritz Münchmeyer Maja Rudolph Frederic Sala Sai Chaitanya Tadepalli AIMat 52 3 0 19 Feb 2025
Lean-ing on Quality: How High-Quality Data Beats Diverse Multilingual Data in AutoFormalization Willy Chan Michael Souliman Jakob Nordhagen Brando Miranda Elyas Obbad Kai Fronsdal Sanmi Koyejo 50 0 0 18 Feb 2025
Formalizing Complex Mathematical Statements with LLMs: A Study on Mathematical Definitions Lan Zhang Marco Valentino André Freitas 49 0 0 17 Feb 2025
Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs David Yin Jing Gao 44 0 0 16 Feb 2025
One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs Hai-Tao Zheng Jiayi Kuang Haojing Huang Zhikun Xu Xinnian Liang ... Xiaoyu Tan C. Qu Ying Shen Hai-Tao Zheng Philip S. Yu LRM 51 2 0 12 Feb 2025
A cross-regional review of AI safety regulations in the commercial aviation Penny A. Barr Sohel M. Imroz 49 0 0 12 Feb 2025
Examining False Positives under Inference Scaling for Mathematical Reasoning Yu Guang Wang Nan Yang Liang Wang Furu Wei LRM 67 3 0 10 Feb 2025
ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data Xiaoyang Liu Kangjie Bao Jiashuo Zhang Yunqi Liu Yu Chen Yu Chen Yang Jiao Tao Luo AIMat 55 0 0 08 Feb 2025
Advanced Weakly-Supervised Formula Exploration for Neuro-Symbolic Mathematical Reasoning Yuxuan Wu Hideki Nakayama NAI 58 0 0 02 Feb 2025
Understand, Solve and Translate: Bridging the Multilingual Mathematical Reasoning Gap Hyunwoo Ko Guijin Son Dasol Choi RALM LRM 80 7 0 05 Jan 2025
Large Language Monkeys: Scaling Inference Compute with Repeated Sampling Bradley Brown Jordan Juravsky Ryan Ehrlich Ronald Clark Quoc V. Le Christopher Ré Azalia Mirhoseini ALM LRM 95 224 0 03 Jan 2025
Mathematical Language Models: A Survey Wei Liu Hanglei Hu Jie Zhou Yuyang Ding Junsong Li ... Mengliang He Qin Chen Bo Jiang Aimin Zhou Liang He LRM 79 12 0 03 Jan 2025
Formal Mathematical Reasoning: A New Frontier in AI Kaiyu Yang Gabriel Poesia Jingxuan He Wenda Li Kristin Lauter Swarat Chaudhuri Dawn Song LRM AI4CE 82 22 0 20 Dec 2024
Can Language Models Rival Mathematics Students? Evaluating Mathematical Reasoning through Textual Manipulation and Human Experiments Andrii Nikolaiev Yiannos Stathopoulos Simone Teufel LRM 83 0 0 16 Dec 2024
Proposing and solving olympiad geometry with guided tree search Chi Zhang Jiajun Song Siyu Li Yitao Liang Yuxi Ma Wei Wang Yixin Zhu Song-Chun Zhu AIMat LRM 76 3 0 14 Dec 2024
Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically Kefan Dong Arvind V. Mahankali Tengyu Ma ReLM LRM 30 6 0 04 Nov 2024
Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency Zenan Li Yifan Wu Zhaoyu Li Xinming Wei Xian Zhang Fan Yang Xiaoxing Ma 44 4 0 28 Oct 2024
Library Learning Doesn't: The Curious Case of the Single-Use "Library" Ian Berlot-Attwell Frank Rudzicz Xujie Si 37 1 0 26 Oct 2024
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation Shaonan Wu Shuai Lu Y. Gong Nan Duan Ping Wei AIMat 45 0 0 21 Oct 2024
Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models Bofei Gao Feifan Song Zhengyuan Yang Zefan Cai Yibo Miao ... Lei Sha Yichang Zhang Xuancheng Ren Tianyu Liu Baobao Chang ELM LRM 47 39 0 10 Oct 2024
Herald: A Natural Language Annotated Lean 4 Dataset Guoxiong Gao Yutong Wang Jiedong Jiang Qi Gao Zihan Qin Tianyi Xu Bin Dong 93 3 0 09 Oct 2024
Consistent Autoformalization for Constructing Mathematical Libraries Lan Zhang Xin Quan André Freitas AI4CE 43 2 0 05 Oct 2024
Easy2Hard-Bench: Standardized Difficulty Labels for Profiling LLM Performance and Generalization Mucong Ding Chenghao Deng Jocelyn Choo Zichu Wu Aakriti Agrawal ... Dinesh Manocha Tom Goldstein John Langford Anima Anandkumar Furong Huang 64 5 0 27 Sep 2024
Proof Automation with Large Language Models Minghai Lu Benjamin Delaware Tianyi Zhang LRM 38 3 0 22 Sep 2024
SubgoalXL: Subgoal-based Expert Learning for Theorem Proving Xueliang Zhao Lin Zheng Haige Bo Changran Hu Urmish Thakker Lingpeng Kong LRM 50 2 0 20 Aug 2024