Sobre la solución automatizada de los problemas de la Olimpiada

Question

Se trata de una pregunta suave sobre el desarrollo de software para resolver problemas de exámenes/concursos.

Imagina el siguiente escenario: Usted, como usuario, tiene (digamos) una hoja de examen de la OMI. Escribe una pregunta cada vez, quizás en algún formato legible por la máquina, en una interfaz de línea de comandos como Matlab. Un minuto más tarde, su programa escupe la respuesta (y también los pasos de prueba/derivación necesarios), y tal vez en 15 minutos, ha resuelto todo el trabajo con ayuda electrónica, pero para el que su puntuación habría sido de 42/42. Además, tienes la seguridad de que tu respuesta ha sido comprobada y cotejada por tu amigo con poder de silicona. Además, suponga que le muestra el resultado a un juez de la OMI, que no dudaría en otorgarle una puntuación completa, salvo por el hecho de que le cuesta un poco de esfuerzo leer el formato "maquinal" del resultado.

Un diseño rudimentario tendría Matlab (para el cálculo) y Mizar (para el razonamiento lógico) en el back-end, y si fuera necesario un motor de procesamiento del lenguaje natural en el front-end. Tenga en cuenta que hay dos grandes obstáculos, tal y como yo lo veo:

• El motor de lenguaje natural tendría que ser muy sofisticado para entender las sutilezas de los problemas matemáticos, expresados en inglés.
• El software existente, como Matlab, es probablemente más adecuado para los problemas que se ajustan a una plantilla (por ejemplo, la inversión de matrices), pero no es muy útil para, por ejemplo, una ecuación funcional que debe resolverse mediante un truco inteligente. Un examinador siempre puede inventar un nuevo "truco inteligente" más allá de lo que los diseñadores del software han pensado.

Pregunta: ¿Existe una herramienta de este tipo? ¿Le interesaría a alguien que se desarrollara? ¿Algún comentario abierto?

Por otro lado, esta herramienta, si se desarrolla, puede aplicarse a una gran variedad de exámenes (GRE, SAT, exámenes de "acceso a la ingeniería" en la India); podemos hacer que un estudiante y un ordenador realicen el examen uno al lado del otro para determinar los puntos fuertes y débiles de dicho software.

Answer 1

La mayoría de los problemas de la OMI no son inmediatamente traducibles (por un humano) en frases en un decidible teoría. Algunos problemas de geometría y álgebra y probablemente algunos tipos de problemas de teoría de números tienen algoritmos de solución mecánica, como la eliminación de cuantificadores. Un subconjunto de esos problemas se presenta en forma interpretable por la máquina, como un sistema de ecuaciones con la palabra "resolver".

Más allá de ese subconjunto limitado de problemas, usted se pregunta si el procesamiento del lenguaje natural y la IA sin asistencia podrían construirse o serían útiles.

Answer 2

Dudo que se pueda escribir un programa así para resolver todos los problemas de la OMI. ¿Qué hace que los problemas de la OMI sean mucho más "fáciles" que las matemáticas de investigación que no podemos hacer? Muchos problemas de la OMI aluden a matemáticas muy difíciles recientemente o actualmente en la investigación. Sin embargo, para ciertos tipos de problemas de la OMI ya existen algoritmos automatizados que los resuelven de forma rutinaria. Por ejemplo, la Geometría Algebraica ha reducido los problemas de geometría euclidiana a la verificación rutinaria de ciertos enunciados algebraicos. No recuerdo el nombre de un programa que haga esto, pero ciertamente existe.

No existe ninguna máquina de Turing que pueda demostrar cualquier teorema que se le introduzca (o incluso que pueda demostrar si el teorema es verdadero o falso), y no existe ningún límite para la longitud de la demostración de un teorema que dependa de la longitud del teorema, por lo que incluso las afirmaciones más simples pueden tener demostraciones extremadamente largas e incomprensibles para los humanos. Así que esperar que alguna vez escribamos un programa de este tipo es probablemente ingenuo.

---

Ver este y sus referencias para obtener información sobre la demostración automática de teoremas en geometría.