ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics

24 February 2023

Papers citing "ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics"

24 / 24 papers shown

Title
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 12 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 106 0 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 128 1 0 05 May 2025
Hierarchical Attention Generates Better Proofs Jianlong Chen Chao Li Yang Yuan Andrew Chi-Chih Yao AIMat LRM 33 0 0 27 Apr 2025
ShadowCoT: Cognitive Hijacking for Stealthy Reasoning Backdoors in LLMs Gejian Zhao Hanzhou Wu Xinpeng Zhang Athanasios V. Vasilakos LRM 38 1 0 08 Apr 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 202 1 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 129 0 0 20 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
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
Large Language Models as an Indirect Reasoner: Contrapositive and Contradiction for Automated Reasoning Yanfang Zhang Yiliu Sun Yibing Zhan Dapeng Tao Dacheng Tao Chen Gong LRM AI4CE LLMAG 97 2 0 28 Jan 2025
Mathematical Language Models: A Survey Wen 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
MIND: Math Informed syNthetic Dialogues for Pretraining LLMs Syeda Nahida Akter Shrimai Prabhumoye John Kamalu S. Satheesh Eric Nyberg M. Patwary M. Shoeybi Bryan Catanzaro LRM SyDa ReLM 103 1 0 15 Oct 2024
Autonomous Evaluation of LLMs for Truth Maintenance and Reasoning Tasks Rushang Karia Daniel Bramblett D. Dobhal Siddharth Srivastava ELM LRM 35 0 0 11 Oct 2024
Herald: A Natural Language Annotated Lean 4 Dataset Guoxiong Gao Yutong Wang Jiedong Jiang Qi Gao Zihan Qin Tianyi Xu Bin Dong 88 3 0 09 Oct 2024
miniCTX: Neural Theorem Proving with (Long-)Contexts Jiewen Hu Thomas Zhu Sean Welleck AIMat 71 6 0 05 Aug 2024
Lean-STaR: Learning to Interleave Thinking and Proving Haohan Lin Zhiqing Sun Yiming Yang Sean Welleck ReLM LRM 72 23 0 14 Jul 2024
Improving Autoformalization using Type Checking Auguste Poiroux Gail Weiss Viktor Kunčak Antoine Bosselut 47 2 0 11 Jun 2024
Can I understand what I create? Self-Knowledge Evaluation of Large Language Models Zhiquan Tan Lai Wei Jindong Wang Xing Xie Weiran Huang ELM LRM 35 5 0 10 Jun 2024
Using Large Language Models for (De-)Formalization and Natural Argumentation Exercises for Beginner's Students M. Carl LRM 16 1 0 12 Apr 2023
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs Albert Q. Jiang Sean Welleck Jin Peng Zhou Wenda Li Jiacheng Liu M. Jamnik Timothée Lacroix Yuhuai Wu Guillaume Lample AIMat 73 158 0 21 Oct 2022
Autoformalization with Large Language Models Yuhuai Wu Albert Q. Jiang Wenda Li M. Rabe Charles Staats M. Jamnik Christian Szegedy AI4CE 110 157 0 25 May 2022
Large Language Models are Zero-Shot Reasoners Takeshi Kojima S. Gu Machel Reid Yutaka Matsuo Yusuke Iwasawa ReLM LRM 328 4,077 0 24 May 2022