Proceedings 8th International Workshop on Theorem Proving Components for Educational Software

• URL: http://arxiv.org/abs/2002.11895v1
• Date: Thu, 27 Feb 2020 03:10:08 GMT
• Title: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software
• Authors: Pedro Quaresma (University of Coimbra, Portugal), Walther Neuper (Graz University of Technology, Austria), Jo\~ao Marcos (UFRN, Brazil)
• Abstract summary: This volume contains the proceedings of the ThEdu'19 workshop, promoted on August 25, 2019, as a satellite event of CADE-27, in Natal, Brazil. Representing the eighth installment of the ThEdu series, ThEdu'19 was a vibrant workshop, with an invited talk by Sarah Winkler, four contributions, and the first edition of a Geometry Automated Provers Competition. The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favoring software support for this transition by exploiting the power of theorem-proving
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This EPTCS volume contains the proceedings of the ThEdu'19 workshop, promoted on August 25, 2019, as a satellite event of CADE-27, in Natal, Brazil. Representing the eighth installment of the ThEdu series, ThEdu'19 was a vibrant workshop, with an invited talk by Sarah Winkler, four contributions, and the first edition of a Geometry Automated Provers Competition. After the workshop an open call for papers was issued and attracted seven submissions, six of which have been accepted by the reviewers, and collected in the present post-proceedings volume. The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favoring software support for this transition by exploiting the power of theorem-proving technologies. The volume editors hope that this collection of papers will further promote the development of theorem-proving-based software, and that it will collaborate on improving mutual understanding between computer mathematicians and stakeholders in education.

Related papers

• Qwen2.5-Math Technical Report: Toward Mathematical Expert Model via Self-Improvement [71.46993852662021]
  We present a series of math-specific large language models: Qwen2.5-Math and Qwen2.5-Math-Instruct-1.5B/7B/72B. Qwen2.5-Math-Instruct supports both Chinese and English, and possess advanced mathematical reasoning capabilities.
  arXiv  Detail & Related papers  (2024-09-18T16:45:37Z)
• Building Math Agents with Multi-Turn Iterative Preference Learning [56.71330214021884]
  This paper studies the complementary direct preference learning approach to further improve model performance. Existing direct preference learning algorithms are originally designed for the single-turn chat task. We introduce a multi-turn direct preference learning framework, tailored for this context.
  arXiv  Detail & Related papers  (2024-09-04T02:41:04Z)
• SciRIFF: A Resource to Enhance Language Model Instruction-Following over Scientific Literature [80.49349719239584]
  We present SciRIFF (Scientific Resource for Instruction-Following and Finetuning), a dataset of 137K instruction-following demonstrations for 54 tasks. SciRIFF is the first dataset focused on extracting and synthesizing information from research literature across a wide range of scientific fields.
  arXiv  Detail & Related papers  (2024-06-10T21:22:08Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  We introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems. We fine-tune the DeepSeekMath 7B model on this synthetic dataset, which comprises 8 million formal statements with proofs. Our model successfully proved 5 out of 148 problems in the Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4 failed to prove any.
  arXiv  Detail & Related papers  (2024-05-23T09:03:42Z)
• Proceedings 12th International Workshop on Theorem proving components for Educational software [0.0]
  ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education. ThEdu'23 was very successful, with one invited talk, by Yves Bertot (Inria, France), "The challenges of using Type Theory to teach Mathematics", and seven regular contributions. Seven submissions have been accepted by our reviewers, who jointly produced at least three careful reports on each of the contributions.
  arXiv  Detail & Related papers  (2024-04-04T11:51:26Z)
• Language Models as Science Tutors [79.73256703631492]
  We introduce TutorEval and TutorChat to measure real-life usability of LMs as scientific assistants. We show that fine-tuning base models with existing dialogue datasets leads to poor performance on TutorEval. We use TutorChat to fine-tune Llemma models with 7B and 34B parameters. These LM tutors specialized in math have a 32K-token context window, and they excel at TutorEval while performing strongly on GSM8K and MATH.
  arXiv  Detail & Related papers  (2024-02-16T22:24:13Z)
• Proceedings 11th International Workshop on Theorem Proving Components for Educational Software [0.0]
  ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education. ThEdu'22 was a vibrant workshop, with two invited talk by Thierry Dana-Picard and Yoni Zohar. The resulting revised papers are collected in the present volume.
  arXiv  Detail & Related papers  (2023-03-09T16:10:13Z)
• Proceedings End-to-End Compositional Models of Vector-Based Semantics [0.0]
  The workshop was sponsored by the research project 'A composition calculus for vector-based semantic modelling with a localization for Dutch' The present volume collects the contributed papers and the abstracts of the invited talks.
  arXiv  Detail & Related papers  (2022-08-10T12:50:12Z)
• Proceedings 10th International Workshop on Theorem Proving Components for Educational Software [0.0]
  ThEdu'21 was a vibrant workshop, with an invited talk by Gilles Dowek (ENS Paris-Saclay), eleven contributions, and one demonstration. The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education.
  arXiv  Detail & Related papers  (2022-02-02T05:48:14Z)
• What's New? Summarizing Contributions in Scientific Literature [85.95906677964815]
  We introduce a new task of disentangled paper summarization, which seeks to generate separate summaries for the paper contributions and the context of the work. We extend the S2ORC corpus of academic articles by adding disentangled "contribution" and "context" reference labels. We propose a comprehensive automatic evaluation protocol which reports the relevance, novelty, and disentanglement of generated outputs.
  arXiv  Detail & Related papers  (2020-11-06T02:23:01Z)
• Proceedings 9th International Workshop on Theorem Proving Components for Educational Software [0.0]
  The 9th International Workshop on Theorem-Proving Components for Educational Software (ThEdu'20) was scheduled to happen on June 29 as a satellite of the IJCAR-FSCD 2020 joint meeting, in Paris. The COVID-19 pandemic came by surprise, though, and the main conference was virtualised. Fearing that an online meeting would not allow our community to fully reproduce the usual face-to-face networking opportunities of the ThEdu initiative, the Steering Committee of ThEdu decided to cancel our workshop. Given that many of us had already planned and worked for that moment, we decided that
  arXiv  Detail & Related papers  (2020-10-28T00:36:08Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.