Improving QED-Tutrix by Automating the Generation of Proofs
The idea of assisting teachers with technological tools is not new. Mathematics in general, and geometry in particular, provide interesting challenges when developing educative softwares, both in the education and computer science aspects. QED-Tutrix is an intelligent tutor for geometry offering an interface to help high school students in the resolution of demonstration problems. It focuses on specific goals: 1) to allow the student to freely explore the problem and its figure, 2) to accept proofs elements in any order, 3) to handle a variety of proofs, which can be customized by the teacher, and 4) to be able to help the student at any step of the resolution of the problem, if the need arises. The software is also independent from the intervention of the teacher. QED-Tutrix offers an interesting approach to geometry education, but is currently crippled by the lengthiness of the process of implementing new problems, a task that must still be done manually. Therefore, one of the main focuses of the QED-Tutrix' research team is to ease the implementation of new problems, by automating the tedious step of finding all possible proofs for a given problem. This automation must follow fundamental constraints in order to create problems compatible with QED-Tutrix: 1) readability of the proofs, 2) accessibility at a high school level, and 3) possibility for the teacher to modify the parameters defining the "acceptability" of a proof. We present in this paper the result of our preliminary exploration of possible avenues for this task. Automated theorem proving in geometry is a widely studied subject, and various provers exist. However, our constraints are quite specific and some adaptation would be required to use an existing prover. We have therefore implemented a prototype of automated prover to suit our needs. The future goal is to compare performances and usability in our specific use-case between the existing provers and our implementation.
Code (0)
등록된 구현이 없습니다.
Tasks
Automated Theorem ProvingSimilar Papers 제목 키워드 기반
A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
Large language models (LLMs) can potentially help with verification using proof assistants by automating proofs. However, it is unclear how effective LLMs are in this task. In this paper, we perform a case study based on…
Automating the Generation of High School Geometry Proofs using Prolog in an Educational Context
When working on intelligent tutor systems designed for mathematics education and its specificities, an interesting objective is to provide relevant help to the students by anticipating their next steps. This can only be …
Automating Mathematical Proof Generation Using Large Language Model Agents and Knowledge Graphs
Large Language Models have demonstrated remarkable capabilities in natural language processing tasks, including mathematical problem-solving that requires multi-step logical reasoning. However, challenges persist in auto…
Formal LogicKnowledge GraphsLanguage ModelingLanguage Modelling+5Baldur: Whole-Proof Generation and Repair with Large Language Models
Formally verifying software properties is a highly desirable but labor-intensive task. Recent work has developed methods to automate formal verification using proof assistants, such as Coq and Isabelle/HOL, e.g., by trai…
From Scientific Texts to Verifiable Code: Automating the Process with Transformers
Despite the vast body of research literature proposing algorithms with formal guarantees, the amount of verifiable code in today's systems remains minimal. This discrepancy stems from the inherent difficulty of verifying…