Mathematical Reasoning via Self-supervised Skip-tree Training

• URL: http://arxiv.org/abs/2006.04757v3
• Date: Wed, 12 Aug 2020 07:48:41 GMT
• Title: Mathematical Reasoning via Self-supervised Skip-tree Training
• Abstract summary: We examine whether self-supervised language modeling applied to mathematical formulas enables logical reasoning. We suggest several logical reasoning tasks that can be used to evaluate language models trained on formal mathematical statements. We find that models trained on the skip-tree task show surprisingly strong mathematical reasoning abilities.
• Score: 17.48858100144651
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We examine whether self-supervised language modeling applied to mathematical formulas enables logical reasoning. We suggest several logical reasoning tasks that can be used to evaluate language models trained on formal mathematical statements, such as type inference, suggesting missing assumptions and completing equalities. To train language models for formal mathematics, we propose a novel skip-tree task. We find that models trained on the skip-tree task show surprisingly strong mathematical reasoning abilities, and outperform models trained on standard skip-sequence tasks. We also analyze the models' ability to formulate new conjectures by measuring how often the predictions are provable and useful in other proofs.

Related papers

• Math Takes Two: A test for emergent mathematical reasoning in communication [1.2891210250935148]
  Math Takes Two is a new benchmark designed to assess the emergence of mathematical reasoning through communication.<n>Motivated by the hypothesis that mathematical cognition in humans co-evolved with the need for precise communication, our benchmark tests whether two agents, without prior mathematical knowledge, can develop a shared symbolic protocol.
  arXiv  Detail & Related papers  (2026-03-30T08:28:48Z)
• From Black-box to Causal-box: Towards Building More Interpretable Models [57.23201263629627]
  We introduce the notion of causal interpretability, which formalizes when counterfactual queries can be evaluated from a specific class of models.<n>We derive a complete graphical criterion that determines whether a given model architecture supports a given counterfactual query.
  arXiv  Detail & Related papers  (2025-10-24T20:03:18Z)
• MatheMagic: Generating Dynamic Mathematics Benchmarks Robust to Memorization [24.225957201610118]
  Current benchmarks are prone to overfitting due to having limited diversity of symbols and rules, coupled with closed-ended answers.<n>This paper proposes a method to leverage these shortcomings as useful features to a construct dynamic, counterfactual benchmark.<n>We demonstrate this via MatheMagic, which generates math test instances with the interpretations of numbers and operators altered, yet has automatically verifiable answers.
  arXiv  Detail & Related papers  (2025-10-07T14:19:21Z)
• Systematic Diagnosis of Brittle Reasoning in Large Language Models [1.14219428942199]
  A central question in artificial intelligence is the extent to which machine learning models comprehend mathematics.<n>We propose a novel framework for measuring mathematical reasoning that moves beyond standard benchmarks to diagnose specific failure points.
  arXiv  Detail & Related papers  (2025-10-05T21:40:09Z)
• LemmaHead: RAG Assisted Proof Generation Using Large Language Models [0.0]
  We develop LemmaHead, a knowledge base that supplements queries to the model with relevant mathematical context. To measure our model's performance in mathematical reasoning, our testing paradigm focuses on the task of automated theorem proving.
  arXiv  Detail & Related papers  (2025-01-27T05:46:06Z)
• Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization [29.06255449960557]
  We introduce a novel method that leverages data extracted from Mathlib to train a lightweight and effective premise retrieval model.<n>The model is learned in a contrastive learning framework, in which a fine-grained similarity calculation method and a re-ranking module are applied.<n> Experimental results demonstrate that our model outperforms existing baselines, achieving higher accuracy while maintaining a lower computational load.
  arXiv  Detail & Related papers  (2025-01-21T06:32:25Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof. Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• Is Your Model Really A Good Math Reasoner? Evaluating Mathematical Reasoning with Checklist [46.670206614087334]
  We argue that if a model really understands a problem, it should be robustly applied across a diverse array of tasks. MathCheck is a well-designed checklist for testing task generalization and reasoning. MathCheck better reflects true mathematical abilities and represents mathematical intelligence more linearly.
  arXiv  Detail & Related papers  (2024-07-11T17:58:58Z)
• From Next-Token to Mathematics: The Learning Dynamics of Mathematical Reasoning in Language Models [38.71041354422434]
  Large Language Models (LLMs) solely trained on next-token prediction learn to solve a wide range of problems involving mathematical reasoning.<n>We show the first analysis of how mathematical reasoning abilities of several open-weight LLMs develop during pre-training and post-training.
  arXiv  Detail & Related papers  (2024-07-01T01:56:28Z)
• Tree-Based Representation and Generation of Natural and Mathematical Language [77.34726150561087]
  Mathematical language in scientific communications and educational scenarios is important yet relatively understudied. Recent works on mathematical language focus either on representing stand-alone mathematical expressions, or mathematical reasoning in pre-trained natural language models. We propose a series of modifications to existing language models to jointly represent and generate text and math.
  arXiv  Detail & Related papers  (2023-02-15T22:38:34Z)
• A Survey of Deep Learning for Mathematical Reasoning [71.88150173381153]
  We review the key tasks, datasets, and methods at the intersection of mathematical reasoning and deep learning over the past decade. Recent advances in large-scale neural language models have opened up new benchmarks and opportunities to use deep learning for mathematical reasoning.
  arXiv  Detail & Related papers  (2022-12-20T18:46:16Z)
• Overcoming Barriers to Skill Injection in Language Modeling: Case Study in Arithmetic [14.618731441943847]
  We develop a novel framework that enables language models to be mathematically proficient while retaining their linguistic prowess. Specifically, we offer information-theoretic interventions to overcome the catastrophic forgetting of linguistic skills that occurs while injecting non-linguistic skills into language models.
  arXiv  Detail & Related papers  (2022-11-03T18:53:30Z)
• Learning to Reason With Relational Abstractions [65.89553417442049]
  We study how to build stronger reasoning capability in language models using the idea of relational abstractions. We find that models that are supplied with such sequences as prompts can solve tasks with a significantly higher accuracy.
  arXiv  Detail & Related papers  (2022-10-06T00:27:50Z)
• Chain of Thought Prompting Elicits Reasoning in Large Language Models [56.811278668446825]
  This paper explores the ability of language models to generate a coherent chain of thought. Experiments show that inducing a chain of thought via prompting can enable sufficiently large language models to better perform reasoning tasks.
  arXiv  Detail & Related papers  (2022-01-28T02:33:07Z)
• A Mathematical Exploration of Why Language Models Help Solve Downstream Tasks [35.046596668631615]
  Autoregressive language models, pretrained using large text corpora to do well on next word prediction, have been successful at solving many downstream tasks. This paper initiates a mathematical study of this phenomenon for the downstream task of text classification.
  arXiv  Detail & Related papers  (2020-10-07T20:56:40Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance.
  arXiv  Detail & Related papers  (2020-09-07T19:50:10Z)
• IsarStep: a Benchmark for High-level Mathematical Reasoning [20.96474618260995]
  We present a benchmark for high-level mathematical reasoning and study the reasoning capabilities of neural sequence-to-sequence models. We build a non-synthetic dataset from the largest repository of proofs written by human experts in a theorem prover.
  arXiv  Detail & Related papers  (2020-06-13T21:09:23Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.