DeepSAT is an ongoing research project investigating the use of deep reinforcement learning for automated theorem proving in propositional logic. In contrast to traditional SAT solvers, which focus on satisfiability checking, our aim is to construct formal proofs of validity within the sequent calculus framework. As a preliminary step toward this goal, we have focused on training recurrent neural networks to predict whether a given propositional formula is a tautology. These models will form the basis of the value function in the planned reinforcement learning architecture. Although in its early stages, DeepSAT lays the groundwork for a logicagnostic, explainable, and energy-eficient alternative to existing neural approaches based on large language models, which require substantial computational resources.
Automated theorem proving is a longstanding challenge at the intersection of logic, artificial intelligence,
and symbolic reasoning. In propositional logic, the state of the art is dominated by SAT solvers [
In contrast, neural approaches to reasoning have gained increasing attention for their ability to
learn inference patterns directly from data [
Our aim is to develop a system for automated proof search in propositional logic. This paper presents
a hybrid system that combines a neural model with a symbolic proof engine based on the sequent
calculus. As a first step, we train a Tree Long Short-Term Memory (Tree-LSTM) [
The architecture of the Tree-LSTM classifier leverages the hierarchical structure of logic syntax: formulas are represented as trees, enabling this model to learn compositional embeddings aligned with their syntactic structure. The symbolic component, in turn, applies inference rules over sequents to construct formal derivations. We evaluate this model both as a standalone classifier and as a heuristic guide within the MCTS agent.
The Python code, the dataset used for the experiments and the trained models can all be found on our git repository at the URL https://github.com/CLAI-UdA/deepsat-experiments/tree/ictcs2025.
DeepSAT is a broader research initiative in which the present work is situated. Its central idea is to frame theorem proving as a sequential decision process, where each state corresponds to a collection of sequents, and each action applies an inference rule to advance the proof. Neural networks provide heuristics in the form of a policy — guiding the choice of inference steps — and a value function — estimating the provability of a sequent. These components are integrated into a tree search procedure such as Monte Carlo Tree Search.
While we acknowledge that this approach is unlikely to compete with SAT solvers in terms of raw performance, DeepSAT ofers several potential advantages in comparison to subsymbolic neural approaches, particularly large-scale language models: Logic-agnosticism. The architecture is not tied to classical propositional logic and can, in principle, be adapted to non-classical logics such as intuitionistic or linear logic without major structural changes.
Extensibility. The system can be extended to support first-order logic, potentially serving as an intelligent assistant in interactive proof development.
Transparency and accessibility. Unlike solutions developed within large-scale industrial research frameworks (e.g., by OpenAI or DeepMind), DeepSAT is designed around principles of openness and explainability.
These features are not intended to outperform traditional symbolic solvers, which remain the most eficient and reliable tools for large-scale automated reasoning. Rather, DeepSAT is conceived as a structured and interpretable alternative to purely neural approaches, particularly those based on large language models. The goal is not to replace symbolic reasoning, but to complement it with learned guidance that remains transparent, adaptable, and logically grounded.
Specifically, the project embraces the following key principles: Open-source. All software components, trained models, and data will be made publicly available. Energy eficiency. The system is designed to operate with a fraction of the computational resources typically required for training and inference in larger models.
Explainability. Although human-readability of the produced proofs is not our primary goal, we aim to design architectures whose internal functioning is more interpretable, owing to the need to operate under constrained computational budgets. This will require novel strategies for the representation and manipulation of formulas and sequents, tailored to the structure of logical reasoning tasks.
This paper represents a first step towards the broader goal of the DeepSAT project. We focus in particular on the implementation of the value function.
We present a method for classifying propositional formulas as tautologies or non-tautologies using a neural network architecture. This approach is based on a Tree-LSTM model, which is specifically designed to operate on tree-structured data, making it well-suited for the recursive and compositional nature of logical formulas.
The central idea is to represent each formula as a binary syntax tree that captures its hierarchical
structure, and to process this tree using a recursive neural network that can learn to recognize various
logical patterns. The Tree-LSTM model, following the architecture proposed by Tai et al. [
To train and evaluate the model, we construct a synthetic dataset of well-formed propositional formulas labeled as tautologies or non-tautologies by means of exhaustive truth table evaluation. To address class imbalance and ensure that well-known tautologies are well represented during training, we perform targeted data augmentation using instantiated tautology schemata.
In our framework, each formula is recursively defined in terms of atomic components (propositional variables and logical constants) and logical connectives, according to the formal syntax of propositional logic.
Atomic formulas correspond to individual propositional variables, each assigned a unique numerical identifier. Compound formulas are constructed recursively by applying logical connectives — such as negation (¬) and binary connectives (∧, ∨, →) — to one or more subformulas.
To train and evaluate the model, we constructed a synthetic dataset of normalized propositional formulas, generated through a controlled recursive process, with bounded depth and a limited set of propositional variables.
The generation follows a recursive pattern: at each level, the formula may be the Boolean constant false (⊥), a propositional variable (), or a compound formula.
Once generated, a normalization procedure is applied to each formula, renaming propositional variables in order of first appearance with sequential indices starting from 0. This step reduces superficial syntactic redundancy, allowing the model to focus on logical structure rather than on arbitrary variable names.
Each formula is labeled either as a tautology or non-tautology by exhaustively evaluating all possible truth assignments. A formula is labeled as a tautology if it is evaluated true under every possible assignment of truth values. Given the limited number of propositional variables, this method is computationally feasible. For future extensions involving a larger variable space, we plan to adopt SAT solvers for more scalable and eficient labeling. The final dataset consists of 10, 000 distinct formulas, each paired with its corresponding Boolean label.
However, the initial distribution of tautologies was highly imbalanced: only 4.18% of the generated formulas were tautologies. This imbalance stems from the random generation process itself: since tautologies constitute only a small fraction of the space of well-formed formulas, they are rarely produced by chance. Such imbalance risks biasing the model during training, potentially leading it to ignore the minority class and underperform on tautological instances. Furthermore, an analysis of the dataset revealed the absence of canonical tautologies such as the Law of the Excluded Middle and Law of Non-Contradiction.
To make the dataset more representative, we introduced a data augmentation phase based on the generation of new examples from known tautological schemata. For this purpose, we defined a collection of tautological schemata containing metavariables. These schemata include the following examples from classical logic: Reflexivity ( → ), Law of the Excluded Middle, Law of Non-Contradiction, De Morgan’s Law for Conjunction, De Morgan’s Law for Disjunction, De Morgan’s Law for Disjunction, Distribution of Conjunction over Disjunction, Distribution of Disjunction over Conjunction.
To generate concrete instances, each metavariable in the schemata is replaced with a randomly generated formula, and the result is finally normalized. The generation process produced formulas with structural properties consistent with those of randomly generated examples in the dataset. This ensures structural consistency between instantiated and randomly generated formulas.
In total 3, 000 new tautological formulas were generated and included as independent examples in the dataset, increasing the proportion of tautologies to 26.29%. Even with the additions of these formulas, the dataset was still unbalanced. To address this challenge, we adopted an asymmetric loss function, described in Section 3.4.
After dataset generation, each propositional formula is converted into a binary syntax tree that reflects its compositional logic structure. In this representation, each node corresponds to a subformula ∈ ℱ , where ℱ is the set of well-formed formulas. The children of each node represent the arguments of the main connective in . This tree structure is required by the Tree-LSTM model, which processes formulas recursively from leaves to root.
To enable numerical processing by the model, to each node is associated an index () ∈ N, which depends on the main connective of the subformula it contains, via a tokenization function : • For each propositional letter , assign the token • For each logical connective □ ∈ {¬, ∧, ∨, →}, assign a token () = + 1,
with ≥ 0 (□ ) = ⎧⎪100, if □ is ¬ ⎪ ⎪ ⎪⎨101, if □ is ∧ ⎪102, if □ is ∨ ⎪ ⎪ ⎪⎩103, if □ is → (⊥) = 105 • For the Boolean constant ⊥, assign the token
The index () is stored in the embedding_index field of the node , and subsequently passed to a learnable embedding layer that maps symbolic identifiers to dense vector representations. Specifically, the embedding layer is parameterized by a matrix E ∈ R × , where denotes the vocabulary size (i.e., the number of distinct tokens) and is the embedding dimension. Given an index = (), the model retrieves the corresponding embedding vector by selecting the -th row of E, denoted = E[] ∈ R . This vector is then used as input to the subsequent Tree-LSMT cell at node .
The embedding matrix E is composed of learnable parameters and participates in gradient-based optimization. At each training step, only the rows corresponding to input symbols are updated.
An example of an embedding-annotated tree is shown in Figure 1.
[Implication] A0 ∧ (A0 → A1) → A1 (embedding_index=103) [Conjunction] A0 ∧ (A0 → A1) (embedding_index=100) [Letter] A0 (embedding_index=1) [Implication] A0 → A1 (embedding_index=103) [Letter] A0 (embedding_index=1) [Letter] A1 (embedding_index=2) [Letter] A1 (embedding_index=2)
For model training, each data example consists of a binary syntax tree whose nodes are annotated with embedding indices, encoding the logical structure of the corresponding formula. Each tree is paired with a Boolean label indicating whether the formula is a tautology or not.
× left child
ℎ
× + tanh tanh ×
ℎ ×
ℎ right child and ℎ vectors. These outputs are then passed to the Tree-LSTM unit corresponding to a higher-level (outer) node in the tree structure. Elliptic pink nodes represent simple pointwise operations, while rectangular yellow nodes represent perceptron layers.
vector ∈ R.
Tree-LSTM networks generalize standard recurrent architectures to hierarchical structures such as syntax tree. In our setting, each formula is represented as a binary tree, and the model computes hidden representation for each node by recursively combining information from its children. This enables the model to capture long-range dependencies and structural relationships that arise in propositional logic formulas.
In the binary Tree-LSTM variant, each internal node receives an input vector ∈ R and two pairs of hidden and cell states, (ℎ, ) and (ℎ, ), from its left and right children, respectively. At each node in the formula tree, the Tree-LSTM performs a local computation — referred to as a Tree-LSTM unit — which outputs a hidden state vector ℎ ∈ R and a memory cell vector ∈ R, where is the hidden dimension. These two vectors encode the entire subtree rooted at that node and are recursively propagated upward to the parent node.
To compute these vectors, the Tree-LSTM unit maintains five internal components: an input gate ∈ R, two forget gates , ∈ R for the left and right children, an output gate ∈ R, and an update The Tree-LSTM transition equations, depicted in Figure 2, are the following: ℎcat = [ℎ, ℎ] = ( () + ()ℎcat + ()) = ( () + ()ℎcat + ()) = ( () + ()ℎcat + ()) = ( () + ()ℎcat + ()) = tanh( () + ()ℎcat + ()) = ⊗ + ⊗ + ⊗ ℎ = ⊗ tanh()
Here, is the input embedding of the current node, denotes the logistic sigmoid activation function, and ⊗ denotes elementwise multiplication. The hidden state vector ℎ can be interpreted as a distributed representation of the subformula rooted at the node, integrating structural and semantic information from its subtree.
Conceptually, the input gate controls the incorporation of new information into the memory cell; the forget gates , regulate the contribution of information from the left and right child children, respectively; and the output gate determines which parts of the memory cell are exposed to the hidden state. As in standard LSTMs, the gating mechanism enables the model to learn multiscale representations and retain relevant information over long-range structural contexts.
In our implementation, leaf nodes (e.g., propositional letters or constants) are initialized with zerovalued hidden and cell states. Unary nodes (e.g., negations) replicate the same child’s state as both left and right inputs, in order to maintain a consistent binary interface.
The output of the Tree-LSTM — that is, the hidden state ℎ at the root of the tree — is passed through a small multi-layer perceptron (MLP) consisting of a fully connected layer with ReLU activation, and a ifnal single-neuron output layer for binary classification.
To address class imbalance in the dataset, we adopt a variant of Focal Loss known as Asymmetric Focal
Loss [
This formulation represents one possible instantiation within a broader class of methods designed to address class imbalance during training. By dynamically modulating the contribution of individual training examples based on their dificulty, it mitigates the dominance of the majority class and places increased emphasis on correctly classifying underrepresented tautologies. In doing so, it aims to enhance recall on the minority class without significantly compromising overall performance.
The Tree-LSTM classifier, described in the previous section, provides a value estimate for propositional formulas in the form of a predicted probability of being a tautology. We integrate this trained model into a Monte Carlo Tree Search (MCTS) agent for automated proof search. The goal is to replace pure pattern-based classification with an agent capable of actively constructing proofs within the sequent calculus framework, guided by a learned probability distribution over inference rules and an estimated value of provability for each sequent.
Proof construction is framed as search over a dynamically growing tree. Each node represents a sequent to be proved, and inference rules decompose it into child sequents. Diferent inference rules may be applied to the same sequent. Therefore, we have two diferent kinds of branch, which have to be dealt with diferently in checking provability and in cost aggregation: all sequents coming from the same inference rule must be proved in order to prove the original sequent, while the success of a single inference rule is enough. Therefore, what we will call proof tree is actually an hyper-tree in which every edge has a source node and a finite set of target nodes. Alternatively, we can view proof-trees as and-or trees.
We implement a variant of Monte Carlo Tree Search that combines the symbolic structure of sequent
calculus with a learned neural policy and value. The MCTS agent performs a series of simulations, each
involving four phases:
• Selection: Starting from the root sequent, the agent recursively selects child nodes based on
a polynomial Upper Confidence Bound for Tree (PUCT) [
This architecture implements a hybrid approach in which symbolic rule applications are guided by probabilities. The neural model steers the exploration toward plausible proof paths, while the MCTS framework ensures that all constructed proofs adhere to the formal semantics of the Sequent Salculus. The next section presents the results of our experiments with this architecture.
In this section we present the result of our experiments on both the Tree-LTSM model and the MCTS agent. In particular, Sections 5.1 to 5.6 present the tuning process and the final results of the Tree-LTSM model, while Section 5.7 deal with the MCTS agent, with either a random policy or a policy derived from the Tree-LTSM model.
All experiments were conducted on the synthetic dataset described in Section 3, generated using a controlled recursive procedure with a maximum syntax tree depth of 5 and up to 7 distinct propositional variables. This limit was chosen as a trade-of between the expressive richness of the generated formulas and their interpretability, both for training analysis and for proof traceability. As discussed, the final dataset includes 13,000 formulas labeled as either tautologies or non-tautologies, with the proportion of tautologies equal to 26.29%. The dataset was randomly split into 80% for training and 20% for testing.
All models were trained in an environment running on a virtualized Ubuntu 22.04.5 LTS server equipped with an 8-core AMD EPYC processor, 31GB of RAM, and NVIDIA Tesla T4 GPU with 15GB of memory. The system uses CUDA 12.6 and NVIDIA driver version 560.35.05.
Training time for each Tree-LSTM variant was approximately 3 hours, while the GRU baseline — trained with half the epochs — completed in approximately 1.5 hours.
Before introducing the tree-based architecture, we first established a baseline for experiments, using
a sequential model based on stacked bidirectional GRU [
The architecture consists of an embedding layer of dimension 32, followed by two bidirectional GRU layers: the first with 128 hidden units, and the second with 64 hidden units. The final hidden states of the second GRU layer are concatenated and passed through a fully connected layer of size 32 with ReLU activation, followed by an output layer with a single neuron for binary classification .
The model was trained using the Adam optimizer [
Although it lacks explicit access to the compositional tree structure of formulas, the GRU model achieved promising results. Table 1 reports the metrics over 10 training epochs.
These results indicate that even a sequential model can learn relevant regularities in propositional formulas. However, we hypothesized that a model explicitly designed to exploit the tree structure of formulas would be more efective at capturing logical composition and semantic abstractions. This motivated the transition to the Tree-LSTM architecture.
In the next section, we introduce a Tree-LSTM model that leverages the hierarchical syntax of logical formulas to improve classification accuracy and generalization.
To determine the best configuration for the Tree-LSTM classifier, we conducted a structured three-stage grid search over a reduced subset of 1,000 formulas sampled from the full dataset, preserving the original class distribution to ensure representativeness.
In the first stage, we varied the hidden state size of the Tree-LSTM unit and the dimension of the fully connected layer. The embedding dimension was fixed at 32, and each trial was run for 5 epochs to control computational cost.
The parameters of the Asymmetric Focal Loss were initially set based on the same heuristic used for the bidirectional GRU baseline: pos = 0.3, neg = 0.7, pos = 3.0, and neg = 1.5. We used the Adam optimizer with a learning rate of 5 × 10− 4.
The Tree-LSTM configuration with 128 hidden units and a fully connected layer of size 32 achieved the best performance in this phase, reaching 92% test accuracy and a test loss of 0.0248.
In the second stage, we fixed the architecture based on the results from the previous phase and varied the class weights ( pos, neg) and focusing parameters ( pos, neg). The goal was to improve the model’s ability to detect tautologies by refining the sensitivity of the loss function to class imbalance. The best results were obtained with pos = 0.25, neg = 0.7, pos = 3.0, neg = 2.5. This configuration achieved a test accuracy of 93% and a test loss of 0.0154.
In the final stage, we optimized the learning rate, testing values from 1 × 10− 4 to 1 × 10− 3 using the best model and loss parameters from the previous steps. The best performance was achieved with a learning rate of 9 × 10− 4, which yielded a test accuracy of 93% and a test loss of 0.0112.
This final configuration — combining architectural tuning, improved loss weighting, and learning rate optimization — was adopted as the default setup for all experiments on the full dataset, discussed in the next section.
Hidden Size & FC Layer (128, 32) Focal Loss Params ( = 0.25, = 3.0) Learning Rate (9 × 10− 4)
After selecting the optimal hyperparameters through grid search, we trained two Tree-LSTM variants on the full dataset of 13,000 examples.
The first model corresponds to the final architecture determined in the previous sections and does not include any dropout regularization. It was trained for 20 epochs and exhibited a stable and consistent learning trajectory. The highest test accuracy was obtained at epoch 17, reaching 99.31%, with a corresponding test loss of 0.0026. While training accuracy converged to 100% in the later epochs, test accuracy remained consistently high across the training process. The test loss also stayed low and stable, indicating that the model was able to generalize well despite the absence of explicit regularization.
These results suggest that overfitting had minimal impact on overall performance.
To assess the impact of regularization, we trained a second variant that includes a dropout layer, with dropout rate of 30%, after the first fully connected layer. The training configuration and number of epochs were kept identical. This model also achieved high performance, with a peak test accuracy of 99.08% at epoch 17. In the final epochs, test accuracy fluctuated between 98.35% and 99.08%, and test loss varied in a narrow range between 0.0017 and 0.0066. Although these variations are not large in absolute terms, they indicate a slightly less stable generalization behavior compared to the model without dropout.
Overall, both models performed strongly, but the version without dropout slightly outperformed the regularized variant in terms of both peak accuracy and consistency. Based on these results, the model without dropout was selected as the final version for evaluation and integration into the MCTS agent.
To better assess the classification performances of the final model, we computed a confusion matrix and standard evaluation metrics focused on the tautology class. The confusion matrix obtained in the test set is the following: Based on this matrix, we derived the following metrics for the tautology class:
Precision =
Recall = F1-score =
TP 666
= TP + FP 666 + 4
TP 666
= TP + FN 666 + 14 2 · Precision · Recall Precision + Recall
These results confirm that the model achieves strong performance not only in overall accuracy, but also in terms of recall and precision on the tautology class — the more challenging and less frequent class in the dataset.
Despite the model’s strong overall performance, a detailed inspection of the misclassifications reveals certain limitations in generalization and abstraction capabilities. Table 5 reports the list of misclassified formulas, grouped by type — false positives and false negatives — and accompanied by their predicted confidence scores.
These misclassifications reveal that the model struggles with recognizing tautologies that lack syntactic regularity or that require a deeper level of semantic abstraction. Even structurally trivial tautologies involving contradictions or logical identities may be missed if expressed in unusual forms.
These residual errors illustrate the limitations of purely statistical generalization. While the model performs well on structurally familiar inputs, it remains sensitive to syntactic variations — confirming the absence of true deductive reasoning and the reliance on learned syntactic heuristics.
The previous evaluation revealed that the Tree-LSTM classifier exhibits limitations in abstraction and generalization — particularly when confronted with tautologies expressed in uncommon syntactic forms.
To test whether the learned value predictions could support structured inference, we embedded the Tree-LSTM classifier within a symbolic agent based on Monte Carlo Tree Search (MCTS). This agent navigates the proof space of the sequent calculus by applying inference rules to decompose sequents into subgoals. The aim was to evaluate the model not in isolation, but as a guide within a search process governed by logical constrains.
Experiments were conducted on the subset of 680 tautological formulas extracted from the test set, each encoded as a sequent with an empty set of premises and the formula as the conclusion. The agent’s task was to find a proof for each tautology using a limited number of inference steps.
Two diferent policy-value functions were tested:
False Positives Formula (((0 → 1) ∨ ((¬2) → 3)) ∨ ((((4 ∨ 5) ∧ (6 → 7)) → (0 → (1 ∨ 2))) ∨ 3)) ((0 ∨ 1) ∨ ((((2 → 3) ∧ 4) ∧ ((¬5) ∧ (6 → 7))) → (0 ∨ (1 ∧ (2 ∧ 3))))) (((0 → 1) → (2 → 3)) ∨ (((4 ∧ (¬⊥)) → (¬(5 ∧ 6))) ∨ (¬0))) ((((0 → (1 ∨ 2)) ∨ (3 ∨ (4 ∧ 5))) ∨ 6) ∨ (((¬(¬7)) ∧ (0 ∧ (1 → 2))) ∨ 3))
False Negatives
• Uniform policy assigns equal prior to all applicable moves ad uses a constant value estimate of 0.5. • Tree-LSTM model policy uses the Tree-LSTM classifier to estimate the probability of success for each subgoal generated by legal inference moves, and assigns move priors accordingly.
We conducted a parameter sweep over two key settings: the number of MCTS simulations per step playout ∈ {2, 3, 4, 5, 10} and the maximum number of proof steps allowed max_steps ∈ {3, 4, 5}. The best performance achieved with the uniform policy was 63.24% accuracy at playout = 10 and max_steps = 5, as shown in Table 6.
We then evaluated the MCTS agent guided by the Tree-LSTM classifier using the same configuration values explored for the uniform policy. In this setup, the model assigns prior probabilities to inference rules based on the predicted provability of the resulting subgoals.
As shown in Table 6, the Tree-LSTM guided agent consistently outperformed the uniform baseline across all tested configurations. With playout = 5 and max_steps = 5, the model-guided agent reached a peak accuracy of 91.42%, compared to 56.76% for the uniform policy under the same conditions. Strong performance was achieved even with minimal simulations per step, suggesting that the classifier provides meaningful guidance that helps focus the search toward promising inference paths.
Numerous studies have explored using machine-learning techniques to partially or fully assist in
constructing proofs for logical systems. A survey can be found in [
Tree-LSTM Policy
• Kusumoto et al. [
In this paper, we have shown that it is possible to train a recurrent neural network to predict the validity of propositional formulas. Furthermore, we have shown that a network trained in this manner can efectively guide the exploration of a Monte Carlo Tree Search (MCTS) agent in the task of finding proofs for sequents in propositional logic. This represents an initial step in the DeepSAT project, which ultimately aims to develop a system capable of automatically proving theorems in type theory.
One might wonder why formulas of the form 1 → 2 → . . . → which frequently arise when translating sequents into single formulas, are not well represented in the training data. This is a consequence of the fact that, in this initial phase, the dataset was constructed independently of the proof tasks. However, this limitation is expected to be naturally overcome in the next phase of the project: by switching to reinforcement learning, the network will be trained directly on formulas encountered during proof search episodes, which include precisely those implicative structures typical of sequents. In this way, the training distribution will become progressively aligned with the actual inference tasks the model is meant to solve.
In the next phase of our project, we aim to address this and other limitations by transitioning from supervised to reinforcement learning. The dataset of formulas currently used to train the neural network in a supervised fashion will instead serve as a foundation for training, via reinforcement learning, a neural network that computes the external policy of the MCTS agent. In parallel, we will continue to train the network responsible for the external value estimate using supervised learning, with the training data drawn from the formulas that appear in the intermediate nodes of the proof trees.
Additionally, we plan to explore alternative neural network architectures, potentially incorporating
attention mechanisms as in [
This work was partially supported by the PNRR project FAIR – Future AI Research (PE00000013), Spoke 9 - Green-aware AI, under the NRRP MUR program funded by the NextGenerationEU; Istituto Nazionale di Alta Matematica – INdAM groups GNCS and GNSAGA.
During the preparation of this work, the authors used X-GPT-4 to: Drafting content, Paraphrase and reword, Improve writing style. After using these tools, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content. IEEE Winter Conference on Applications of Computer Vision, 2024, p. 2798 – 2807. doi:10.1109/ WACV57701.2024.00279. [16] C. Metta, M. Fantozzi, A. Papini, G. Amato, M. Bergamaschi, A. Fois, S. G. Galfrè, A. Marchetti, M. Vegliò, M. Parton, F. Morandin, Increasing biases can be more eficient than increasing weights, Advances in Data Analysis and Classification (2025). doi: 10.1007/s11634-025-00649-2. [17] T. M. Moerland, J. Broekens, A. Plaat, C. M. Jonker, Monte carlo tree search for asymmetric trees, 2018. doi:10.48550/arXiv.1805.09218. [18] E. Doe, M. H. M. Winands, D. J. N. J. Soemers, C. Browne, Combining Monte-Carlo tree search with proof-number search, in: 2022 IEEE Conference on Games (CoG), IEEE Press, 2022, p. 206–212. doi:10.1109/CoG51982.2022.9893635. [19] G. Amato, M. Rubino, F. Scozzari, Inferring linear invariants with parallelotopes, Sci. Comput.
Program. 148 (2017) 161–188. doi:10.1016/j.scico.2017.05.011.