Efficient Neural Clause-Selection Reinforcement

• URL: http://arxiv.org/abs/2503.07792v1
• Date: Mon, 10 Mar 2025 19:14:48 GMT
• Title: Efficient Neural Clause-Selection Reinforcement
• Authors: Martin Suda,
• Abstract summary: We present a neural network architecture for scoring clauses for clause selection.<n>We integrate the network into the Vampire theorem prover and train it from successful proof attempts.<n>An experiment on the diverse TPTP benchmark finds the neurally guided prover improve over a baseline strategy.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Clause selection is arguably the most important choice point in saturation-based theorem proving. Framing it as a reinforcement learning (RL) task is a way to challenge the human-designed heuristics of state-of-the-art provers and to instead automatically evolve -- just from prover experiences -- their potentially optimal replacement. In this work, we present a neural network architecture for scoring clauses for clause selection that is powerful yet efficient to evaluate. Following RL principles to make design decisions, we integrate the network into the Vampire theorem prover and train it from successful proof attempts. An experiment on the diverse TPTP benchmark finds the neurally guided prover improve over a baseline strategy, from which it initially learns--in terms of the number of in-training-unseen problems solved under a practically relevant, short CPU instruction limit--by 20%.

Related papers

• Can RLHF be More Efficient with Imperfect Reward Models? A Policy Coverage Perspective [31.956232187102465]
  This paper studies how to transfer knowledge from imperfect reward models in online RLHF.<n>We propose a theoretical transfer learning algorithm with provable benefits compared to standard online learning.
  arXiv  Detail & Related papers  (2025-02-26T16:03:06Z)
• Preventing Local Pitfalls in Vector Quantization via Optimal Transport [77.15924044466976]
  We introduce OptVQ, a novel vector quantization method that employs the Sinkhorn algorithm to optimize the optimal transport problem. Our experiments on image reconstruction tasks demonstrate that OptVQ achieves 100% codebook utilization and surpasses current state-of-the-art VQNs in reconstruction quality.
  arXiv  Detail & Related papers  (2024-12-19T18:58:14Z)
• Model-Based Transfer Learning for Contextual Reinforcement Learning [5.5597941107270215]
  We introduce Model-Based Transfer Learning to solve contextual RL problems.<n>We show theoretically that the method exhibits sublinear regret in the number of training tasks.<n>We experimentally validate our methods using urban traffic and standard continuous control benchmarks.
  arXiv  Detail & Related papers  (2024-08-08T14:46:01Z)
• An Efficient Learning-based Solver Comparable to Metaheuristics for the Capacitated Arc Routing Problem [67.92544792239086]
  We introduce an NN-based solver to significantly narrow the gap with advanced metaheuristics. First, we propose direction-aware facilitating attention model (DaAM) to incorporate directionality into the embedding process. Second, we design a supervised reinforcement learning scheme that involves supervised pre-training to establish a robust initial policy.
  arXiv  Detail & Related papers  (2024-03-11T02:17:42Z)
• On-Device Learning with Binary Neural Networks [2.7040098749051635]
  We propose a CL solution that embraces the recent advancements in CL field and the efficiency of the Binary Neural Networks (BNN) The choice of a binary network as backbone is essential to meet the constraints of low power devices.
  arXiv  Detail & Related papers  (2023-08-29T13:48:35Z)
• Deep Active Learning with Structured Neural Depth Search [18.180995603975422]
  Active-iNAS trains several models and selects the model with the best generalization performance for querying the subsequent samples after each active learning cycle. We propose a novel active strategy with the method called structured variational inference (SVI) or structured neural depth search (SNDS) At the same time, we theoretically demonstrate that the current VI-based methods based on the mean-field assumption could lead to poor performance.
  arXiv  Detail & Related papers  (2023-06-05T12:00:12Z)
• Provable Reward-Agnostic Preference-Based Reinforcement Learning [61.39541986848391]
  Preference-based Reinforcement Learning (PbRL) is a paradigm in which an RL agent learns to optimize a task using pair-wise preference-based feedback over trajectories. We propose a theoretical reward-agnostic PbRL framework where exploratory trajectories that enable accurate learning of hidden reward functions are acquired.
  arXiv  Detail & Related papers  (2023-05-29T15:00:09Z)
• Learning to Optimize for Reinforcement Learning [58.01132862590378]
  Reinforcement learning (RL) is essentially different from supervised learning, and in practice, these learneds do not work well even in simple RL tasks. Agent-gradient distribution is non-independent and identically distributed, leading to inefficient meta-training. We show that, although only trained in toy tasks, our learned can generalize unseen complex tasks in Brax.
  arXiv  Detail & Related papers  (2023-02-03T00:11:02Z)
• Learning To Cut By Looking Ahead: Cutting Plane Selection via Imitation Learning [80.45697245527019]
  We show that a greedy selection rule explicitly looking ahead to select cuts that yield the best bound improvement delivers strong decisions for cut selection. We propose a new neural architecture (NeuralCut) for imitation learning on the lookahead expert.
  arXiv  Detail & Related papers  (2022-06-27T16:07:27Z)
• A Simple Fine-tuning Is All You Need: Towards Robust Deep Learning Via Adversarial Fine-tuning [90.44219200633286]
  We propose a simple yet very effective adversarial fine-tuning approach based on a $textitslow start, fast decay$ learning rate scheduling strategy. Experimental results show that the proposed adversarial fine-tuning approach outperforms the state-of-the-art methods on CIFAR-10, CIFAR-100 and ImageNet datasets.
  arXiv  Detail & Related papers  (2020-12-25T20:50:15Z)
• Learning to Prune Deep Neural Networks via Reinforcement Learning [64.85939668308966]
  PuRL is a deep reinforcement learning based algorithm for pruning neural networks. It achieves sparsity and accuracy comparable to current state-of-the-art methods.
  arXiv  Detail & Related papers  (2020-07-09T13:06:07Z)

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.