A Benchmark and Test Environment for the Theorem Prover E

The theorem prover E is a high-performance deduction system for many-sorted first-order logic with equality. As a saturating theorem prover, E searches for a proof by contradiction by systematically exploring the space of derivable first-order clauses (modulo redundancy). Performance of the theorem prover depends on the one hand on efficient algorithms and data structures, and on the other hand on search heuristics controlled by sets of parameters.

The prover is under continuous development. Currently, evaluation and testing of the system is a manual process, utilizing either small scale ad-hoc tests on the developer workstation, or systematic large-scale automation on the StarExec community cluster. Ad-hoc tests are manual and undocumented, while StarExec tests are complex, require manual set-up, and are only efficient (in terms of developer time and elapsed time) for tests requiring thousands of CPU hours. In particular, it is very hard to achieve fully automated tests with short feedback times.

The aim of this project is to develop a portable, drop-in test and benchmark environment that fills the gap between manual tests and large-scale evaluation enables systematic and automated testing, evaluation and tuning of the system.

The benchmark system should fulfill the following requirements:

• It must be available as a simple archive (e.g. .tgz) and be installable on any modern Linux/OS-X/Unix computer with minimal user interaction. During installation it should automatically recognize relevant system parameters (e.g. number of cores, memory) and should configure itself accordingly during installation.
• It must maintain a processing queue efficiently using local resources to execute theorem proving jobs.
• It must support the scheduling of complex test runs (theorem prover version, search parameters, set of input files), and report the summarized results in a standard way. This mode must be available via a simple-to-use API, preferably to multiple users.
• It should support priorities and ensure fair access, with manually scheduled jobs taking precedence over automatically recurring jobs. No job should be delayed for ever, but for automatically recurring jobs, outdated instances may be cancelled.
• It should offer a regression test mode that pulls the prover sources from a git repository, builds the system, and runs a predefined test schedule and test to results for regressions in run time and correctness. The results should be archived and published in HTML to a defined folder accessible to the local web server.
• It should rely only on widely deployed Open Source technology (e.g. make, bash, Python) and it must itself be licensed under an Open Source license compatible with the license used by E (currently GPL2).
• Bonus: The system should be able to integrate other TPTP/SZS compatible theorem provers and evaluate them as well.

In this context, there are (up to) three topics for Bachelor Theses/Student Projects available.

Shared responsibilities: Data Formats, APIs, packaging

All students should work together to define the API and data types for the system: How should jobs be described? How can jobs be submitted? How are results collected? The system should at least support StarExec-packages and StarExec runscripts for theorem prover configuration, but also needs ways to specify test examples, expected results, and both summarized and full actual results.

Preliminary work has identified a number of concepts that the system probably should supportL

• A library of test problems that holds the actual input for each problem. This should probably support sub-libraries, e.g. different TPTP versions.
• A library of test sets, where each test set is a list of problems from problem library.
• A library of different versions of the theorem prover.
• A library of theorem prover configurations (each comprising a prover and a set of options for search control)
• A database of jobs, where each job is a combination of a prover configuration and a test set, possibly with partial or complete results.
• A single pair - a prover configuration and a problem - as the smallest unit of execution.

The second shared responsibility is the design and development of the packaging and installation process.

Subproject: Multi-core Job Scheduling and Execution

This subproject concerns the efficient scheduling and execution of sets of theorem prover runs on the local hardware. It should ensure that all cores are fully utilized, but also that no more threads than cores are running to avoid unnecessary and expensive context switches. This subproject is the core of the environment.

Prerequisites

• Skill in Python (as the suggested implementation language)
• Basic understanding of Linux/Unix systems
• Basic data structures and algorithms
• Process control and basic interprocess communication (e.g. pipes or sockets)
• Basic database skills

Subproject: Automatic Testing and Reporting

This subproject should automatically maintain a configurable list of remote git branches of the theorem prover, check them for updates, and if an update has been detected, should automatically fetch the new version, build the prover in both debug and performance configurations and perform tests with a predefined set of configurations and test problems. The results should be compared against expected values, and should be summarized and published via a web interface, with problems, errors, and regressions highlighted.

Prerequisites

• Skill in Python (as the suggested implementation language)
• Skill in HTML and CSS
• Knowledge of version control systems, in particular git
• Basic understanding of interprocess communication
• Basic database skills

Subproject: StarExec Backend

StarExec (described above) offers an API via the Java program StarExecCommand. This subproject should enable configuration of the benchmark environment to transparently use StarExec as the backend to execute (large) jobs.

Prerequisites

• Skill in Python (as the suggested implementation language)
• Skill in Java
• Basic understanding of interprocess communication and http

Literature