Cyc ATP Challenges at CASC-J4!

Cycorp is pleased to announce the Cyc ATP Challenges at CASC-J4!

Background

The Cyc knowledge base comprises hundreds of thousands of concepts, interrelated through millions of formal assertions representing a broad scope of common-sense knowledge. As such, Cyc provides a foundation for semantically-aware solutions in a wide range of domains. OpenCyc is an open source ontology, derived from the full Cyc knowledge base, that contains virtually all of the Cyc concepts but only a subset of the assertions about each concept.

Beginning with CASC-J4, the CASC competition will include problems derived from OpenCyc knowledge base content and answerable queries over that content relying on inference chains of interest to the domain of common-sense reasoning.

A detailed description of the problem set can be found here under the section "The Scaling Challenge Problem Set".

The problems relevant to the Cyc ATP Challenges constitute the CYC category under the new LTB division of the competition.

Prizes

A cash prize of 100 euros will be announced and awarded at the end of the competition to each winner of two related challenges:

(1) CYC Completeness Challenge

The CYC Completeness Challenge rewards pragmatic completeness over the CYC category of the LBT division. The winner will be the prover that can successfully solve the most CYC problems during the competition. Ties (if any) will be broken based on the median time spent by the prover on its answerable problems.

(2) CYC Efficiency Challenge

The CYC Efficiency Challenge rewards both processing efficiency and pragmatic completeness over the CYC category. For each successfully solved CYC problem, a utility metric will be applied to the time taken to solve the problem. The total utility for a prover is the sum of the utilities for each of the problems it successfully solves. The winner will be the prover with the highest total utility over the CYC category.

The utility metric to be used is defined as follows ^[1]

Utility(t) = (Tb/t)^(1/CB)

where :

t = the time taken to solve the problem ^[2]

Tb = a baseline allowed time to solve a problem

CB = the Completeness Bonus parameter ^[3]

For CASC-J4 the values which will be used are

Tb = 10 seconds

CB = 5

All times will be rounded to the nearest hundredth of a second, and 0.00 will be treated like 0.01 when computing the utility metric.

Notes :

[1] Here is an overview of some landmark values of the utility metric :

t (sec) Utility(t)

0.01 = 3.981

0.02 = 3.466

0.05 = 2.885

0.1 = 2.512

0.2 = 2.187

0.5 = 1.821

1 = 1.585

2 = 1.380

5 = 1.149

10 = 1.000

20 = 0.871

50 = 0.725

100 = 0.631

200 = 0.549

500 = 0.457

1000 = 0.398

[2] Due to the batch nature of the CYC category, the time taken to solve a problem must by necessity be estimated. Assume we have

TOTAL = the total number of problems in the CYC category

N = the number of CYC problems solved

T(0) = the CYC category start time

T(k) = the time when solution k is announced

The solution time t for problem k will be estimated as

t = (T(k) - T(k-1))*(N/TOTAL)

The solvability ratio (N/TOTAL) attempts to reasonably distrubute the total time spent between the N solved problems and the TOTAL-N unsolved problems.

[3] The Completeness Bonus (CB) parametrizes the importance of completeness versus efficiency.

Note that when CB = 1 there is no benefit at all for additional completeness. Utility in this case simplifies to answers / second.

Note that as CB approches infinity there is no benefit at all for additional efficiency. Utility in this case simplifies to 1.

When CB = 5 the metric results in a reasonable tradeoff that rewards efficiency while still favoring completeness.

MEDIA CONTACT: Larry Lefkowitz, larry@cyc.com (512) 342-4000