Core Insights - The article discusses the challenges and innovations in formalizing mathematical proofs, particularly focusing on inequality problems and the limitations of current large language models (LLMs) in providing rigorous reasoning [1][27][38]. Group 1: Inequality Proofs and Formalization - Inequality problems serve as ideal subjects for testing the rigor of mathematical reasoning due to their clear structure and logical simplicity [1]. - Current formal systems like Lean and Coq require high precision in expression, making them difficult to apply at scale, especially for middle and high school level problems [1][5]. - A new approach proposed by research teams from Stanford, UC Berkeley, and MIT involves breaking down inequality proof tasks into two non-formal but verifiable sub-tasks: Bound Estimation and Relation Prediction [2][7]. Group 2: IneqMath Dataset - The IneqMath dataset is the first benchmark for Olympic-level inequality proofs, consisting of 1,252 training problems, 200 test problems, and 100 validation problems [12]. - The training set includes 83 theorem types and 29 theorem categories, allowing for model fine-tuning [12][13]. - Each problem in the dataset has a unique correct answer, facilitating the verification of results [10]. Group 3: Evaluation Framework - The research team developed a framework called LLM-as-Judge, which includes five automated reviewers to assess the logical rigor of the reasoning process in LLMs [20][23]. - The framework evaluates whether models merely guessed the correct answer or followed a logical reasoning chain at each step [23][24]. - The evaluation system has shown high alignment with human annotations, achieving an F1 score of 0.93, indicating its reliability and scalability [24]. Group 4: Findings on LLM Performance - The study found that while LLMs like GPT-4 and others can guess answers accurately, they often fail to maintain logical rigor in their reasoning processes [27][30]. - The accuracy of final answers can be high, but the overall reasoning correctness remains low, with some models dropping from 71.5% to 6% when evaluated for logical rigor [29]. - Increasing model size or reasoning time does not significantly improve the quality of reasoning, suggesting that simply scaling models is insufficient for enhancing logical closure [30][32]. Group 5: Improvement Strategies - The research identified effective strategies for improving LLM performance, such as self-improvement via critic and theorem augmentation, which have shown to enhance accuracy by approximately 5% and 10% respectively [42]. - The IneqMath leaderboard encourages community participation, allowing researchers to submit their models for evaluation based on both final answer accuracy and reasoning rigor [36][37].