Maurizio Parton

DeepSAT is a research project investigating deep reinforcement learning for automated theorem proving in propositional logic. In contrast to traditional SAT solvers, which check satisfiability, our aim is to construct formal proofs of validity within the sequent calculus, working in intuitionistic propositional logic. We first train a Tree-LSTM classifier to predict whether a formula is an intuitionistic tautology, and then use it to warm-start a dual-head policy–value network that guides a Monte Carlo Tree Search prover. Closing the reinforcement learning loop, the network is refined by expert iteration on the proof traces generated by the search it guides: the proofs MCTS finds become the training signal for the next round. On a held-out test set, expert iteration improves low-budget proving substantially over the warm-started prover, and a diagnostic analysis attributes the residual ceiling primarily to proof depth rather than to guidance failure. DeepSAT aims at a logic-agnostic, explainable, and energy-efficient alternative to neural approaches based on large language models, which require substantially greater computational resources.

Portfolio allocation represents a significant challenge within financial markets, traditionally relying on correlation or covariance matrices to delineate relationships among stocks. However, these methodologies assume time stationarity and only capture linear relationships among stocks. In this study, we propose to substitute the conventional Pearson's correlation or covariance matrix in portfolio optimization with a similarity matrix derived from the signature. The signature, a concept from path theory, provides a unique representation of time series data, encoding their geometric patterns and inherent properties. Furthermore, we undertake a comparative analysis of network structures derived from the correlation matrix versus those obtained from the signature-based similarity matrix. Through numerical evaluation on the Standard & Poor's 500, we assess that portfolio allocation utilizing the signature-based similarity matrix yielded superior results in terms of cumulative log-returns and Sharpe ratio compared to the baseline network approach based on Pearson's correlation. This assessment was conducted across various portfolio optimization strategies. This research contributes to portfolio allocation and financial network representation by proposing the use of signature-based similarity matrices over traditional correlation or covariance matrices.