![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
benchmarking mathematical AI
Oct. 18th, 2006 09:56 pmTPTP is a theorem-proving competition.
I would like to see a "halting problem machine" competition, in which the task is to guess whether a given TM halts. I can think of two variants:
* Variant 1: only strict proofs count (there may be some controversy about what counts as an axiom)
* Variant 2: one can make guesses. If you're a guesser, evidence that the halting time for a machine is really long would be as useful as evidence that it never halts... although we could punishment higher for guessing "no-halt" when it halts just before the bell.
Likewise, I'd like to see a competition for proving the equivalence of Lisp programs... I'd love to stretch this to see how far I can take it. This sort of thing could be used for making smart compilers (e.g. by compiling/memoizing commonly-occurring subtrees). Going one step further, the same kind of work can help us automatically discover new program transformations that rewrite code to be more efficient. Some compilers must do this already. The further step that I want to make is automatically changing representations (i.e. rewriting data-structures in the code), and I don't know if this has been done.
A pair of theorems (respectively, the Halting problem, Rice's Theorem) mean that these two competitions can't have a definite winner.
I would like to see a "halting problem machine" competition, in which the task is to guess whether a given TM halts. I can think of two variants:
* Variant 1: only strict proofs count (there may be some controversy about what counts as an axiom)
* Variant 2: one can make guesses. If you're a guesser, evidence that the halting time for a machine is really long would be as useful as evidence that it never halts... although we could punishment higher for guessing "no-halt" when it halts just before the bell.
Likewise, I'd like to see a competition for proving the equivalence of Lisp programs... I'd love to stretch this to see how far I can take it. This sort of thing could be used for making smart compilers (e.g. by compiling/memoizing commonly-occurring subtrees). Going one step further, the same kind of work can help us automatically discover new program transformations that rewrite code to be more efficient. Some compilers must do this already. The further step that I want to make is automatically changing representations (i.e. rewriting data-structures in the code), and I don't know if this has been done.
A pair of theorems (respectively, the Halting problem, Rice's Theorem) mean that these two competitions can't have a definite winner.
