Learn how easy it is to sync an existing GitHub or Google Code repo to a SourceForge project! See Demo


Cycorp is pleased to announce the Cyc ATP Challenges at CASC


Cyc ATP Challenges at CASC
<link rel="shortcut icon" href="http://www.cyc.com/favicon.ico">


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




<a href="http://www.cyc.com">Cyc</a>

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.


<a href="http://www.opencyc.org">OpenCyc</a>

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

<a href="http://www.cs.miami.edu/~tptp/CASC/J4/">CASC-J4</a>,

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
<a href="http://www.opencyc.org/doc/tptp_challenge_problem_set">here</a>
under the section
<a href="http://www.opencyc.org/doc/tptp_challenge_problem_set#scaling">
"The Scaling Challenge Problem Set"</a>.

The problems relevant to the Cyc ATP Challenges constitute the CYC
category under the new
<a href="http://www.cs.miami.edu/~tptp/CASC/J4/Design.html#CompetitionDivisions">LTB division</a>
of the competition.


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

<h3>(1) CYC Completeness Challenge</h3>


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.


<h3>(2) CYC Efficiency Challenge</h3>


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
<sup><a href="#note1">[1]</a></sup>

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

where :

<blockquote><table cellpadding="0" cellspacing="0">
<tr valign="bottom"><td>t </td><td>&nbsp;=&nbsp;</td><td>the time taken to solve the problem

<sup><a href="#note2">[2]</a></sup></td></tr>
<tr valign="bottom"><td>Tb</td><td>&nbsp;=&nbsp;</td><td>a baseline allowed time to solve a problem</td></tr>
<tr valign="bottom"><td>CB</td><td>&nbsp;=&nbsp;</td><td>the Completeness Bonus parameter
<sup><a href="#note2">[3]</a></sup></td></tr>


For CASC-J4 the values which will be used are

<blockquote><table cellpadding="0" cellspacing="0">

<tr><td>Tb</td><td>&nbsp;=&nbsp;</td><td>10 seconds</td></tr>


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.


<!-- -------------------------------------------------------------------------------- -->

<h3>Notes :</h3>


<strong><a name="note1">[1]</a></strong>

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


<style type="text/css"> table.utility td { font-size: 8pt; } </style>
<blockquote><table cellpadding="0" cellspacing="0" class="utility">
<tr><th align="right" width="40%">t (sec)</th>
<th align="center" width="20%"></th>

<th align="left" width="40%">Utility(t)</th></tr>
<tr><td colspan="3"><hr></td></tr>
<tr><td align="right"> 0.01</td><td align="center">=</td><td align="left">3.981</td></tr>
<tr><td align="right"> 0.02</td><td align="center">=</td><td align="left">3.466</td></tr>
<tr><td align="right"> 0.05</td><td align="center">=</td><td align="left">2.885</td></tr>

<tr><td align="right"> 0.1</td><td align="center">=</td><td align="left">2.512</td></tr>
<tr><td align="right"> 0.2</td><td align="center">=</td><td align="left">2.187</td></tr>
<tr><td align="right"> 0.5</td><td align="center">=</td><td align="left">1.821</td></tr>
<tr><td align="right"> 1</td><td align="center">=</td><td align="left">1.585</td></tr>

<tr><td align="right"> 2</td><td align="center">=</td><td align="left">1.380</td></tr>
<tr><td align="right"> 5</td><td align="center">=</td><td align="left">1.149</td></tr>
<tr><td align="right"> 10</td><td align="center">=</td><td align="left">1.000</td></tr>
<tr><td align="right"> 20</td><td align="center">=</td><td align="left">0.871</td></tr>

<tr><td align="right"> 50</td><td align="center">=</td><td align="left">0.725</td></tr>
<tr><td align="right"> 100</td><td align="center">=</td><td align="left">0.631</td></tr>
<tr><td align="right"> 200</td><td align="center">=</td><td align="left">0.549</td></tr>
<tr><td align="right"> 500</td><td align="center">=</td><td align="left">0.457</td></tr>

<tr><td align="right"> 1000</td><td align="center">=</td><td align="left">0.398</td></tr>

<strong><a name="note2">[2]</a></strong>
Due to the batch nature of the CYC category, the time taken to solve a
problem must by necessity be estimated. Assume we have

<blockquote><table cellpadding="0" cellspacing="0">
<tr><td>TOTAL</td><td>&nbsp;=&nbsp;</td><td>the total number of problems in the CYC category</td></tr>
<tr><td>N </td><td>&nbsp;=&nbsp;</td><td>the number of CYC problems solved</td></tr>

<tr><td>T(0) </td><td>&nbsp;=&nbsp;</td><td>the CYC category start time</td></tr>
<tr><td>T(k) </td><td>&nbsp;=&nbsp;</td><td>the time when solution k is announced</td></tr>

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.


<strong><a name="note3">[3]</a></strong>

The Completeness Bonus (CB) parametrizes the importance of completeness versus


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.




Posted by Larry Lefkowitz 2008-08-08