REVIEW 13 cited by
InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
The math abilities of large language models can represent their abstract reasoning ability. In this paper, we introduce and open-source our math reasoning LLMs InternLM-Math which is continue pre-trained from InternLM2. We unify chain-of-thought reasoning, reward modeling, formal reasoning, data augmentation, and code interpreter in a unified seq2seq format and supervise our model to be a versatile math reasoner, verifier, prover, and augmenter. These abilities can be used to develop the next math LLMs or self-iteration. InternLM-Math obtains open-sourced state-of-the-art performance under the setting of in-context learning, supervised fine-tuning, and code-assisted reasoning in various informal and formal benchmarks including GSM8K, MATH, Hungary math exam, MathBench-ZH, and MiniF2F. Our pre-trained model achieves 30.3 on the MiniF2F test set without fine-tuning. We further explore how to use LEAN to solve math problems and study its performance under the setting of multi-task learning which shows the possibility of using LEAN as a unified platform for solving and proving in math. Our models, codes, and data are released at \url{https://github.com/InternLM/InternLM-Math}.
Forward citations
Cited by 13 Pith papers
-
SocietyBench: Forecasting Counterfactual Social-World Evolution
A new benchmark measures LLM social-world forecasting on anonymized real events, finding the best model reaches 75/100 and agent scaffolding does not help.
-
From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.
-
LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4
White-box proof search with factorized Lean 4 goals reaches 18.4% on MiniF2F with Llemma-7B, outperforming black-box generation at 9.6%.
-
Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization
GTED uses tree edit distance on operator trees of standardized Lean statements to evaluate autoformalization, ranking top on miniF2F and joint-top on ProofNet.
-
VRAgent-R1: Boosting Video Recommendation with MLLM-based Agents via Reinforcement Learning
VRAgent-R1 uses an MLLM agent to summarize videos and a reinforcement-learned agent to simulate user choices, improving video recommendation and user-decision simulation on MicroLens-100K.
-
Unleashing Embodied Task Planning Ability in LLMs via Reinforcement Learning
A 7B LLM trained with sparse completion rewards and a GRPO-style algorithm reaches state-of-the-art on ALFWorld and ScienceWorld.
-
Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification
Safe uses step-level formal verification in Lean 4, aggregated by a small LSTM and combined with process reward scores, to improve best-of-n accuracy for LLM mathematical reasoning.
-
Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery
An integrated survey organizing AI mathematical reasoning into informal, formal, discovery, and technique axes while cataloging benchmarks and assessing failure modes.
-
A Survey on Evaluating Quality and Trustworthiness in LLM-Generated Data
A metric-oriented survey that classifies intrinsic quality and trustworthiness metrics for LLM-generated data across six modalities and documents systematic evaluation gaps in the current literature.
-
Integrating Rules and Semantics for LLM-Based C-to-Rust Translation
IRENE combines rule-based retrieval, structured summarization, and compiler feedback to improve LLM-based C-to-Rust translation accuracy and safety.
-
LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving
LeanConjecturer automatically generates thousands of Lean 4 theorem statements from Mathlib files and uses them for reinforcement learning, with modest measured gains on held-out problems.
-
Formally Solving Answer-Construction Problems in Lean
ECP, an enumerate-conjecture-prove framework with Lean verification, improves answer-construction accuracy on ConstructiveBench and a PutnamBench subset, but its benchmark has a 17% major-error rate and its abstract r...
-
UniVG-R1: Reasoning Guided Universal Visual Grounding with Reinforcement Learning
UniVG-R1 uses CoT supervised fine-tuning plus GRPO with difficulty-aware reweighting to make Qwen2-VL substantially better at multi-image, reasoning-based visual grounding.
Discussion (0). Sign in to comment.