gym-saturation: Gymnasium environments for saturation provers (System description)

• URL: http://arxiv.org/abs/2309.09022v1
• Date: Sat, 16 Sep 2023 15:25:39 GMT
• Title: gym-saturation: Gymnasium environments for saturation provers (System description)
• Authors: Boris Shminke
• Abstract summary: We contribute usage examples with two different provers: Vampire and iProver. We demonstrate how environment wrappers can transform a prover into a problem similar to a multi-armed bandit.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This work describes a new version of a previously published Python package - gym-saturation: a collection of OpenAI Gym environments for guiding saturation-style provers based on the given clause algorithm with reinforcement learning. We contribute usage examples with two different provers: Vampire and iProver. We also have decoupled the proof state representation from reinforcement learning per se and provided examples of using a known ast2vec Python code embedding model as a first-order logic representation. In addition, we demonstrate how environment wrappers can transform a prover into a problem similar to a multi-armed bandit. We applied two reinforcement learning algorithms (Thompson sampling and Proximal policy optimisation) implemented in Ray RLlib to show the ease of experimentation with the new release of our package.

Related papers

• Spanning the Visual Analogy Space with a Weight Basis of LoRAs [84.16188433935494]
  Visual analogy learning enables image manipulation through demonstration rather than textual description.<n>LoRWeB specializes the model for each analogy task at inference time through dynamic composition of learned transformation primitives.<n>We introduce two key components: (1) a learnable basis of LoRA modules, to span the space of different visual transformations, and (2) a lightweight encoder that dynamically selects and weighs these basis LoRAs.
  arXiv  Detail & Related papers  (2026-02-17T17:02:38Z)
• Make Prompts Adaptable: Bayesian Modeling for Vision-Language Prompt Learning with Data-Dependent Prior [14.232144691524528]
  Recent Vision-Language Pretrained models have become the backbone for many downstream tasks. MLE training can lead the context vector to over-fit dominant image features in the training data. This paper presents a Bayesian-based framework of prompt learning, which could alleviate the overfitting issues on few-shot learning application.
  arXiv  Detail & Related papers  (2024-01-09T10:15:59Z)
• Boot and Switch: Alternating Distillation for Zero-Shot Dense Retrieval [50.47192086219752]
  $texttABEL$ is a simple but effective unsupervised method to enhance passage retrieval in zero-shot settings. By either fine-tuning $texttABEL$ on labelled data or integrating it with existing supervised dense retrievers, we achieve state-of-the-art results.
  arXiv  Detail & Related papers  (2023-11-27T06:22:57Z)
• Co-training $2^L$ Submodels for Visual Recognition [67.02999567435626]
  Submodel co-training is a regularization method related to co-training, self-distillation and depth. We show that submodel co-training is effective to train backbones for recognition tasks such as image classification and semantic segmentation.
  arXiv  Detail & Related papers  (2022-12-09T14:38:09Z)
• Speech Sequence Embeddings using Nearest Neighbors Contrastive Learning [15.729812221628382]
  We introduce a simple neural encoder architecture that can be trained using an unsupervised contrastive learning objective. We show that when built on top of recent self-supervised audio representations, this method can be applied iteratively and yield competitive SSE.
  arXiv  Detail & Related papers  (2022-04-11T14:28:01Z)
• An audiovisual and contextual approach for categorical and continuous emotion recognition in-the-wild [27.943550651941166]
  We tackle the task of video-based audio-visual emotion recognition, within the premises of the 2nd Workshop and Competition on Affective Behavior Analysis in-the-wild (ABAW) Standard methodologies that rely solely on the extraction of facial features often fall short of accurate emotion prediction in cases where the aforementioned source of affective information is inaccessible due to head/body orientation, low resolution and poor illumination. We aspire to alleviate this problem by leveraging bodily as well as contextual features, as part of a broader emotion recognition framework.
  arXiv  Detail & Related papers  (2021-07-07T20:13:17Z)
• Visual Transformer for Task-aware Active Learning [49.903358393660724]
  We present a novel pipeline for pool-based Active Learning. Our method exploits accessible unlabelled examples during training to estimate their co-relation with the labelled examples. Visual Transformer models non-local visual concept dependency between labelled and unlabelled examples.
  arXiv  Detail & Related papers  (2021-06-07T17:13:59Z)
• Composable Learning with Sparse Kernel Representations [110.19179439773578]
  We present a reinforcement learning algorithm for learning sparse non-parametric controllers in a Reproducing Kernel Hilbert Space. We improve the sample complexity of this approach by imposing a structure of the state-action function through a normalized advantage function. We demonstrate the performance of this algorithm on learning obstacle-avoidance policies in multiple simulations of a robot equipped with a laser scanner while navigating in a 2D environment.
  arXiv  Detail & Related papers  (2021-03-26T13:58:23Z)
• Contrastive Prototype Learning with Augmented Embeddings for Few-Shot Learning [58.2091760793799]
  We propose a novel contrastive prototype learning with augmented embeddings (CPLAE) model. With a class prototype as an anchor, CPL aims to pull the query samples of the same class closer and those of different classes further away. Extensive experiments on several benchmarks demonstrate that our proposed CPLAE achieves new state-of-the-art.
  arXiv  Detail & Related papers  (2021-01-23T13:22:44Z)
• Self-supervised Pre-training with Hard Examples Improves Visual Representations [110.23337264762512]
  Self-supervised pre-training (SSP) employs random image transformations to generate training data for visual representation learning. We first present a modeling framework that unifies existing SSP methods as learning to predict pseudo-labels. Then, we propose new data augmentation methods of generating training examples whose pseudo-labels are harder to predict than those generated via random image transformations.
  arXiv  Detail & Related papers  (2020-12-25T02:44:22Z)
• Landscape of R packages for eXplainable Artificial Intelligence [4.91155110560629]
  The article is primarily devoted to the tools available in R, but since it is easy to integrate the Python code, we will also show examples for the most popular libraries from Python.
  arXiv  Detail & Related papers  (2020-09-24T16:54:57Z)

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.