Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving

• URL: http://arxiv.org/abs/2305.16366v1
• Date: Thu, 25 May 2023 11:35:52 GMT
• Title: Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving
• Authors: Xueliang Zhao, Wenda Li, Lingpeng Kong
• Abstract summary: Large language models(LLMs) present an intriguing avenue of exploration in the domain of formal theorem proving. We introduce a subgoal-based demonstration learning framework, consisting of two primary elements. We have successfully increased the prevailing proof accuracy from 38.9% to 44.3% on the miniF2F benchmark.
• Score: 15.624453757710798
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large language models~(LLMs) present an intriguing avenue of exploration in the domain of formal theorem proving. Nonetheless, the full utilization of these models, particularly in terms of demonstration formatting and organization, remains an underexplored area. In an endeavor to enhance the efficacy of LLMs, we introduce a subgoal-based demonstration learning framework, consisting of two primary elements: Firstly, drawing upon the insights of subgoal learning from the domains of reinforcement learning and robotics, we propose the construction of distinct subgoals for each demonstration example and refine these subgoals in accordance with the pertinent theories of subgoal learning. Secondly, we build upon recent advances in diffusion models to predict the optimal organization, simultaneously addressing two intricate issues that persist within the domain of demonstration organization: subset selection and order determination. Through the integration of subgoal-based learning methodologies, we have successfully increased the prevailing proof accuracy from 38.9\% to 44.3\% on the miniF2F benchmark. Furthermore, the adoption of diffusion models for demonstration organization can lead to an additional enhancement in accuracy to 45.5\%, or a $5\times$ improvement in sampling efficiency compared with the long-standing state-of-the-art method. Our code is available at \url{https://github.com/HKUNLP/subgoal-theorem-prover}.

Related papers

• Proof Flow: Preliminary Study on Generative Flow Network Language Model Tuning for Formal Reasoning [11.268313729426627]
  We present a proof of concept in the domain of formal reasoning, specifically in the Neural Theorem Proving setting. Unlike classical reward-maximization reinforcement learning, GFlowNets have emerged as a promising approach for sampling compositional objects. Our early results demonstrate GFlowNet fine-tuning's potential for enhancing model performance in a search setting.
  arXiv  Detail & Related papers  (2024-10-17T05:10:12Z)
• Unleashing the Potential of the Diffusion Model in Few-shot Semantic Segmentation [56.87049651707208]
  Few-shot Semantic has evolved into In-context tasks, morphing into a crucial element in assessing generalist segmentation models. Our initial focus lies in understanding how to facilitate interaction between the query image and the support image, resulting in the proposal of a KV fusion method within the self-attention framework. Based on our analysis, we establish a simple and effective framework named DiffewS, maximally retaining the original Latent Diffusion Model's generative framework.
  arXiv  Detail & Related papers  (2024-10-03T10:33:49Z)
• SubgoalXL: Subgoal-based Expert Learning for Theorem Proving [37.115856591703974]
  SubgoalXL is a novel approach that synergizes subgoal-based proofs with expert learning to enhance formal theorem proving. SubgoalXL achieves a new state-of-the-art performance of 56.1% in Isabelle on the standard miniF2F dataset.
  arXiv  Detail & Related papers  (2024-08-20T20:10:53Z)
• Self-Refine Instruction-Tuning for Aligning Reasoning in Language Models [0.8133739801185272]
  The alignments of reasoning abilities between smaller and larger Language Models are largely conducted via Supervised Fine-Tuning (SFT) We propose the Self-refine Instruction-tuning method that elicits Smaller Language Models to self-refine their abilities. Results obtained on commonsense and math reasoning tasks show that this approach significantly outperforms Instruction-tuning in both in-domain and out-domain scenarios.
  arXiv  Detail & Related papers  (2024-05-01T09:10:27Z)
• Co-guiding for Multi-intent Spoken Language Understanding [53.30511968323911]
  We propose a novel model termed Co-guiding Net, which implements a two-stage framework achieving the mutual guidances between the two tasks. For the first stage, we propose single-task supervised contrastive learning, and for the second stage, we propose co-guiding supervised contrastive learning. Experiment results on multi-intent SLU show that our model outperforms existing models by a large margin.
  arXiv  Detail & Related papers  (2023-11-22T08:06:22Z)
• Knowledge Transfer-Driven Few-Shot Class-Incremental Learning [23.163459923345556]
  Few-shot class-incremental learning (FSCIL) aims to continually learn new classes using a few samples while not forgetting the old classes. Despite the advance of existing FSCIL methods, the proposed knowledge transfer learning schemes are sub-optimal due to the insufficient optimization for the model's plasticity. We propose a Random Episode Sampling and Augmentation (RESA) strategy that relies on diverse pseudo incremental tasks as agents to achieve the knowledge transfer.
  arXiv  Detail & Related papers  (2023-06-19T14:02:45Z)
• Variance-Preserving-Based Interpolation Diffusion Models for Speech Enhancement [53.2171981279647]
  We present a framework that encapsulates both the VP- and variance-exploding (VE)-based diffusion methods. To improve performance and ease model training, we analyze the common difficulties encountered in diffusion models. We evaluate our model against several methods using a public benchmark to showcase the effectiveness of our approach.
  arXiv  Detail & Related papers  (2023-06-14T14:22:22Z)
• Hierarchical Optimization-Derived Learning [58.69200830655009]
  We establish a new framework, named Hierarchical ODL (HODL), to simultaneously investigate the intrinsic behaviors of optimization-derived model construction and its corresponding learning process. This is the first theoretical guarantee for these two coupled ODL components: optimization and learning.
  arXiv  Detail & Related papers  (2023-02-11T03:35:13Z)
• USER: Unified Semantic Enhancement with Momentum Contrast for Image-Text Retrieval [115.28586222748478]
  Image-Text Retrieval (ITR) aims at searching for the target instances that are semantically relevant to the given query from the other modality. Existing approaches typically suffer from two major limitations.
  arXiv  Detail & Related papers  (2023-01-17T12:42:58Z)
• Learning to Augment via Implicit Differentiation for Domain Generalization [107.9666735637355]
  Domain generalization (DG) aims to overcome the problem by leveraging multiple source domains to learn a domain-generalizable model. In this paper, we propose a novel augmentation-based DG approach, dubbed AugLearn. AugLearn shows effectiveness on three standard DG benchmarks, PACS, Office-Home and Digits-DG.
  arXiv  Detail & Related papers  (2022-10-25T18:51:51Z)
• Let us Build Bridges: Understanding and Extending Diffusion Generative Models [19.517597928769042]
  Diffusion-based generative models have achieved promising results recently, but raise an array of open questions. This work tries to re-exam the overall framework in order to gain better theoretical understandings. We present 1) a first theoretical error analysis for learning diffusion generation models, and 2) a simple and unified approach to learning on data from different discrete and constrained domains.
  arXiv  Detail & Related papers  (2022-08-31T08:58:10Z)

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.