MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers
MaLeS is an automatic tuning framework for automated theorem provers. It provides solutions for both the strategy finding as well as the strategy scheduling problem. This paper describes the tool and the methods used in it, and evaluates its performance on three automated theorem provers: E, LEO-II and Satallax. An evaluation on a subset of the TPTP library problems shows that on average a MaLeS-tuned prover solves 8.67% more problems than the prover with its default settings.
Code (0)
등록된 구현이 없습니다.
Tasks
SchedulingSimilar Papers 제목 키워드 기반
Quantum automated theorem proving
Automated theorem proving, or more broadly automated reasoning, aims at using computer programs to automatically prove or disprove mathematical theorems and logical statements. It takes on an essential role across a vast…
Automated Theorem ProvingGraATP: A Graph Theoretic Approach for Automated Theorem Proving in Plane Geometry
Automated Theorem Proving (ATP) is an established branch of Artificial Intelligence. The purpose of ATP is to design a system which can automatically figure out an algorithm either to prove or disprove a mathematical cla…
Automated Theorem ProvingRocqSmith: Can Automatic Optimization Forge Better Proof Agents?
This work studies the applicability of automatic AI agent optimization methods to real-world agents in formal verification settings, focusing on automated theorem proving in Rocq as a representative and challenging domai…
Automated Theorem ProvingLearning to Prove Theorems by Learning to Generate Theorems
We consider the task of automated theorem proving, a key AI task. Deep learning has shown promise for training theorem provers, but there are limited human-written theorems and proofs available for supervised learning. T…
Automated Theorem ProvingBliStrTune: Hierarchical Invention of Theorem Proving Strategies
Inventing targeted proof search strategies for specific problem sets is a difficult task. State-of-the-art automated theorem provers (ATPs) such as E allow a large number of user-specified proof search strategies describ…
Automated Theorem Proving