6
$\begingroup$

This is a soft question on developing software to solve exam/contest problems.

Imagine the following scenario: You, as user, have (say) an IMO exam paper. You type one question at a time, perhaps in some machine-readable format, into a command-line interface like Matlab. A minute of thinking later, your program spits out the answer (and also the needed proof/derivation steps), and perhaps in 15 minutes, you have solved the entire paper with electronic assistance, but for which your score would have been 42/42. You also have the confidence that your answer has been checked and cross checked by your Silicon-powered friend. Further, suppose you were to show the output to an IMO judge, (s)he would have no hesitation in awarding a full score, except for the fact that it takes a little effort to read the "machine-like" format of the output.

A crude design would have Matlab (for computation) and Mizar (for logical reasoning) at the back-end, and if needed a natural language processing engine at the front end. Note that there are 2 big hurdles as I see it:

  • The natural language engine would have to be very sophisticated to understand the subtleties of maths problems, expressed in English.
  • Existing software like Matlab is probably better suited for problems fitting a template (say matrix inversion), but not much use for say, a functional equation to be solved by a clever trick. An examiner can always come up with a new "clever trick" beyond what the software designers have thought of.

Question: Is there one such tool in existence? Would anyone be interested if it's developed ? Any open-ended comments?

As an aside,this tool if developed may be applied to a wide variety of exams ( GRE, SAT, "Engineering entrance" exams in India) ; we may have a student and a computer taking the exam side by side to determine the strengths and weaknesses of such software.

$\endgroup$
4
  • 2
    $\begingroup$ Why restrict only to olympiad questions? Why not do research with this automated friends? The main difference I can think of between olympiad problems and research problems is that we know apriori that the problems from the former category are solvable. Are you proposing to exploit this explicitly or implicitly somewhere? $\endgroup$
    – Srivatsan
    Commented Oct 5, 2011 at 2:05
  • 1
    $\begingroup$ @Srivatsan: yes, I am making use of the fact that olympiad problems are solvable, albeit implicitly - my software has only to learn a large number of separate tricks. I said "olympiad" just to set a bar for the software. And I would like a mathematician's answer to this, hence this query here. $\endgroup$
    – Ganesh
    Commented Oct 5, 2011 at 2:07
  • 2
    $\begingroup$ I think you just identified the difficulty in automated theorem proving: all mathematical research is devoted to solving problems in a definitive manner. And this is ostensibly automatable, except research papers are difficult to formalize, and even informal everyday -word- problems are difficult to translate to symbolism, at least automatically. $\endgroup$
    – Mitch
    Commented Oct 5, 2011 at 2:27
  • $\begingroup$ I would say, it probably takes more skill to even translate a problem to a format a computer understands, than to actually solve the problem, (if the problem i IMO level). $\endgroup$
    – Per Alexandersson
    Commented Oct 5, 2011 at 13:11

2 Answers 2

Reset to default
4
$\begingroup$

Most IMO problems are not immediately translatable (by a human) into sentences in a decidable theory. Some geometry and algebra problems and probably a few types of number theory problems have mechanical solution algorithms, such as quantifier elimination. A subset of those problems are presented in machine-interpretable form such as a system of equations with the word "solve".

Beyond that limited subset of problems, you are asking whether unassisted natural language processing and AI could be built or would be useful.

$\endgroup$
3
$\begingroup$

I doubt one could ever write such a program to solve all IMO problems. What really makes IMO problems so much "easier" than research maths that we can't do? Many IMO problems allude to very difficult mathematics recently or currently in research. However, for certain types of IMO problems, automated algorithims already exist which solve them in a routine fashion. For example, Algebraic Geometry has reduced Euclidean geometry problems into rountinely verifying certain algebraic statements. I can't remember a programs name that does this, but it certainly exists.

There is no Turing machine which will output a proof of any input theorem (or even output whether the theorem is true or false), and there is no bound to the length of the proof of a theorem dependent on the length of the theorem, so even simple statements can have extremely long proofs incomprehensible to humans. So to expect we will ever write such a program is probably naïve.

See this and the references therein for information on automated theorem proving in geometry.

$\endgroup$
2

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .