Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)

• URL: http://arxiv.org/abs/2004.10667v3
• Date: Tue, 26 May 2020 07:46:04 GMT
• Title: Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
• Authors: Yutaka Nagashima
• Abstract summary: We present a simple dataset that contains data on over 400k proof method applications along with over 100 extracted features for each. Our simple data format allows machine learning practitioners to try machine learning tools to predict proof methods in Isabelle/HOL without requiring domain expertise in logic.
• Score: 6.85316573653194
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers. However, the expressive nature of underlying logics and esoteric structures of proof documents impede machine learning practitioners, who often do not have much expertise in formal logic, let alone Isabelle/HOL, from achieving a large scale success in this field. In this data description, we present a simple dataset that contains data on over 400k proof method applications along with over 100 extracted features for each in a format that can be processed easily without any knowledge about formal logic. Our simple data format allows machine learning practitioners to try machine learning tools to predict proof methods in Isabelle/HOL without requiring domain expertise in logic.

Related papers

• Topological Methods in Machine Learning: A Tutorial for Practitioners [4.297070083645049]
  Topological Machine Learning (TML) is an emerging field that leverages techniques from algebraic topology to analyze complex data structures. This tutorial provides a comprehensive introduction to two key TML techniques, persistent homology and the Mapper algorithm. To enhance accessibility, we adopt a data-centric approach, enabling readers to gain hands-on experience applying these techniques to relevant tasks.
  arXiv  Detail & Related papers  (2024-09-04T17:44:52Z)
• Can LLMs Separate Instructions From Data? And What Do We Even Mean By That? [60.50127555651554]
  Large Language Models (LLMs) show impressive results in numerous practical applications, but they lack essential safety features. This makes them vulnerable to manipulations such as indirect prompt injections and generally unsuitable for safety-critical tasks. We introduce a formal measure for instruction-data separation and an empirical variant that is calculable from a model's outputs.
  arXiv  Detail & Related papers  (2024-03-11T15:48:56Z)
• MLFMF: Data Sets for Machine Learning for Mathematical Formalization [0.18416014644193068]
  MLFMF is a collection of data sets for benchmarking systems used to support formalization of mathematics with proof assistants. Each data set is derived from a library of formalized mathematics written in proof assistants Agda or Lean. With more than $250,000$ entries in total, this is currently the largest collection of formalized mathematical knowledge in machine learnable format.
  arXiv  Detail & Related papers  (2023-10-24T17:00:00Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. Existing methods are difficult to reproduce or build on, due to private code, data, and compute requirements. This paper introduces LeanDojo: an open-source Lean toolkit consisting of toolkits, data, models. We develop ReProver: an LLM-based prover augmented with retrieval for selecting premises from a vast math library.
  arXiv  Detail & Related papers  (2023-06-27T17:05:32Z)
• Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
  Program-Guided Fact-Checking (ProgramFC) is a novel fact-checking model that decomposes complex claims into simpler sub-tasks. We first leverage the in-context learning ability of large language models to generate reasoning programs. We execute the program by delegating each sub-task to the corresponding sub-task handler.
  arXiv  Detail & Related papers  (2023-05-22T06:11:15Z)
• Rethinking Complex Queries on Knowledge Graphs with Neural Link Predictors [58.340159346749964]
  We propose a new neural-symbolic method to support end-to-end learning using complex queries with provable reasoning capability. We develop a new dataset containing ten new types of queries with features that have never been considered. Our method outperforms previous methods significantly in the new dataset and also surpasses previous methods in the existing dataset at the same time.
  arXiv  Detail & Related papers  (2023-04-14T11:35:35Z)
• On Exams with the Isabelle Proof Assistant [0.0]
  We present an approach for testing student learning outcomes in a course on automated reasoning using the Isabelle proof assistant. The approach allows us to test both general understanding of formal proofs in various logical proof systems and understanding of proofs in the higher-order logic of Isabelle/HOL.
  arXiv  Detail & Related papers  (2023-03-10T11:37:09Z)
• Explaining Classifiers Trained on Raw Hierarchical Multiple-Instance Data [0.0]
  A number of data sources have the natural form of structured data interchange formats (e.g. Multiple security logs in/XML format) Existing methods, such as in Hierarchical Instance Learning (HMIL) allow learning from such data in their raw form. By treating these models as sub-set selections problems, we demonstrate how interpretable explanations, with favourable properties, can be generated using computationally efficient algorithms. We compare to an explanation technique adopted from graph neural networks showing an order of magnitude speed-up and higher-quality explanations.
  arXiv  Detail & Related papers  (2022-08-04T14:48:37Z)
• Questions Are All You Need to Train a Dense Passage Retriever [123.13872383489172]
  ART is a new corpus-level autoencoding approach for training dense retrieval models that does not require any labeled training data. It uses a new document-retrieval autoencoding scheme, where (1) an input question is used to retrieve a set of evidence documents, and (2) the documents are then used to compute the probability of reconstructing the original question.
  arXiv  Detail & Related papers  (2022-06-21T18:16:31Z)
• Proving Theorems using Incremental Learning and Hindsight Experience Replay [45.277067974919106]
  We propose a general incremental learning algorithm for training domain specific provers for first-order logic without equality. We adapt hindsight experience replay to theorem proving, so as to be able to learn even when no proof can be found. We show that provers trained this way can match and sometimes surpass state-of-the-art traditional provers on the TPTP dataset.
  arXiv  Detail & Related papers  (2021-12-20T16:40:26Z)
• Combining Feature and Instance Attribution to Detect Artifacts [62.63504976810927]
  We propose methods to facilitate identification of training data artifacts. We show that this proposed training-feature attribution approach can be used to uncover artifacts in training data. We execute a small user study to evaluate whether these methods are useful to NLP researchers in practice.
  arXiv  Detail & Related papers  (2021-07-01T09:26:13Z)

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.