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 logic-agnostic, explainable, and energy-efficient alternative to existing neural approaches based on large language models, which require substantial computational resources.
Recurrent Neural Networks for Guiding Proof Search in Propositional Logic
Amato G.
;Balestra N.
;Parton M.
2025-01-01
Abstract
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 logic-agnostic, explainable, and energy-efficient alternative to existing neural approaches based on large language models, which require substantial computational resources.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
