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.

这项工作描述了之前发布的 Python 软件包 gym-saturation 的新版本：这是一个基于给定子句算法和强化学习的 OpenAI Gym 环境集合。我们提供了两种不同求解器（Vampire 和 iProver）的使用示例，并将证明状态表示与强化学习分离，并提供了使用已知的 ast2vec Python 代码嵌入模型作为一阶逻辑表示的示例。此外，我们还展示了环境包装器如何将求解器转化为类似多臂赌博机问题的问题。我们使用 Ray RLlib 实现了两种强化学习算法（Thompson 抽样和 Proximal Policy Optimization），以展示我们软件包新版本的实验易用性。

gym - 饱和：用于饱和证明器的体育馆环境（系统描述）

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

Reusing previously trained models is critical in deep reinforcement learning
to speed up training of new agents. However, it is unclear how to acquire new
skills when objectives and constraints are in conflict with previously learned
skills. Moreover, when retraining, there is an intrinsic conflict between
exploiting what has already been learned and exploring new skills. In soft
actor-critic (SAC) methods, a temperature parameter can be dynamically adjusted
to weight the action entropy and balance the explore $\times$ exploit
trade-off. However, controlling a single coefficient can be challenging within
the context of retraining, even more so when goals are contradictory. In this
work, inspired by neuroscience research, we propose a novel approach using
inhibitory networks to allow separate and adaptive state value evaluations, as
well as distinct automatic entropy tuning. Ultimately, our approach allows for
controlling inhibition to handle conflict between exploiting less risky,
acquired behaviors and exploring novel ones to overcome more challenging tasks.
We validate our method through experiments in OpenAI Gym environments.

本文提出了一种受神经科学研究启发的新方法，使用抑制性网络，以允许分离和自适应状态值评估，以及不同的自动熵调整，最终我们的方法允许控制抑制来处理利用较少风险获取的行为和探索新行为之间的冲突，以克服更具挑战性的任务，并通过在 OpenAI Gym 环境中进行实验验证。