Blockchain-based Algorithmic Problem Solving Competitions

Efstathios Aliprantis, MSc in Computer Science* October 2021
Asst. Prof. Eugenie Foustoucos*
Asst. Prof. Spyridon Voulgaris*
Assoc. Prof. Vangelis Markakis*
* Dept. of Informatics, Athens University of Economics and Business


This thesis presents a blockchain-based platform where algorithmic problems can be posed as competitions, potentially, with a financial reward. A competition is won by the first individual to submit an algorithm that is both correct and bounded on time and space complexity, in accordance with the specification of the corresponding problem. Submitted algorithms must be accompanied by a formal proof of correctness which is mechanically validated by the platform. The platform is based on blockchain technology, specifically Ethereum, which ensures transparency on solution validation and allows for the automatic payment of competition rewards.

A complete system design is proposed and experimentally evaluated. The system consists of a web-based front end and a blockain-based backend. The blockain-based backend conducts competitions transparently and validates submitted algorithms and proofs mechanically. The proposed system design is evaluated by an experimental proof-of-concept implementation.

Furthermore, a theoretical setup is established in order to develop the methods and tools required to make the platform a reality. This theoretical setup includes a method for the formal specification of computational problems where problem specifications are formatted as special problem-definition algorithms. A method for proving algorithm correctness against such problem specifications is proposed based on formal program verification. A new programming language with a fully working compiler is developed for the representation of algorithms. A proof composer for proofs of algorithm correctness is developed based on a custom configuration of Hoare logic.

1.1.2 Concept and Actors

Competitions have two actors roles:

The individual who poses a problem and initiates a competition
The individual who proposes a solution accompanied by a proof

There is no role of “reviewer” as solutions are validated by the platform.

We focus on algorithmic problems, thus petitioners provide definitions of algorithmicproblems while creators provide algorithms. A definition for an algorithmic problem consist of the following:

  • A definition for the underlying computational problem which will serve as a specification for the correctness of proposed algorithms
  • A set of complexity constraints that must be satisfied by proposed algorithms

Creators submit algorithms in the form of a procedural program and accompany them with a proof for their correctness and their worst case asymptotic complexity. Proofs are composed with the utilization of formal program verification methods.

3.1.2 Competition flow

The main flow of a completion is as follows:

  1. The petitioner submits the question q, initiating the competition
  2. A creator submits an answer a accompanied by a proof p
  3. The system invokes the proof validator* v on (q, a, p) and
    1. if v responds positively the competition concludes successfully
    2. otherwise, the system allows the re-execution of step 2

This flow is depicted in figure 3.1.

Figure 3.1: Flow of a competition
Figure 3.1:Flow of a competition

* See Definition 3.2 of the full text for proof validators

3.2.2 Solver algorithms/Answer objects (simplified)

Solver algorithms/Answer objects are represented as procedural programs having the solve function.

Here is an example of a solver for the natural square root of natural numbers. The result will be -1 if there is no natural square root.

Program 3.1: Natural square root solver
Program 3.1:Natural square root solver

3.2.3 Problem definitions/Question objects (simplified)

To define an algorithmic problem* we create a program necessarily containing the following funcions:

Determines whether instance i is a valid instance of the problem
negatedVerify(i, s, h)
Determines whether solution s is not correct for instance iwith the help of hint h

The negatedVerify function must behave as follows:

  • If s is correct for i then it must return false for every h
  • If s is not correct for i then there must exist an h for which it returns true

Example: Here is a definition for the natural square root problem.

Program 3.5: Natural square root problem definition with no complexity constraints
Program 3.5:Natural square root problem definition with no complexity constraints

This example behaves as follows:

  • If s is -1, meaning there is no square root, the hint should provide the actual square root to prove the mistake
  • Otherwise, it compares s with the square of i to check if s is not the actual square root of i

Negating the verifier seems counter-intuitive, however, it serves for creating proofs of correctness as described in the next section.

* This page focuses on correctness, refer to the full text for details about asymptotic complexity constraints. Correctness (simplified)

To examine the correctness of a given solver against a certain problem definition, we compose the program correctness.

Program 3.7: Format of program <code>correctness</code>
Program 3.7:Format of program correctness

It is proved (Proposition 3.2 and section in the full text) that a candidate solver is correct if and only if

  • program correctness terminates for every i and h
  • and variable verdict is always true at program termination.

4 System Design and Implementation (overview)

A petitioner must provide two inputs to create a competition:

  1. The problem definition
  2. The reward amount in eth currency
Figure 4.1: Competition starting process
Figure 4.1:Competition starting process

A creator needs to perform two steps to submit a solution:

  1. Write the solver algorithm
  2. Make the formal proof for the correctness of the solver algorithm against the problem definition
Figure 4.2: Answer submission process
Figure 4.2:Answer submission process

5 Evaluation (a few words)

The proof of concept system is evaluated in terms of the observed length of the proofs and the gas cost (Ethereum computational fees) required to validate them.

6.1 Conclusions

We have proposed a blockchain-based platform design for conducting algorithmic problem solving competitions where proposed algorithms can be mechanically validated. The feasibility of this design has been demonstrated by a proof-of-concept implementation. As part of the design, we proposed a method for representing algorithmic problem definitions as procedural computer programs and showed that these representations can be effectively used to validate the correctness and complexity bounds of proposed algorithms.

The evaluation process revealed two main issues regarding the use of the platform, though none of them is irrecoverable. The first issue arises from the length of the proofs of correctness. The relatively large number of low level deduction steps makes it cumbersome for human users to compose proofs. The second issue arises from the relatively large number of axioms needed for a proof that only relies on simple arithmetic truths. This signals that more complex proofs would require a very large number of axioms or otherwise, they would have to prove many trivial facts thus making the proofs immensely lengthy.