Smart Induction for Isabelle/HOL (System Description)
- URL: http://arxiv.org/abs/2001.10834v1
- Date: Mon, 27 Jan 2020 15:29:34 GMT
- Title: Smart Induction for Isabelle/HOL (System Description)
- Authors: Yutaka Nagashima
- Abstract summary: smart_induct lists promising arguments for the induct tactic without relying on a search.
Our evaluation demonstrated smart_induct produces valuable recommendations across problem domains.
- Score: 6.85316573653194
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Proof assistants offer tactics to facilitate inductive proofs. However, it
still requires human ingenuity to decide what arguments to pass to those
induction tactics. To automate this process, we present smart_induct for
Isabelle/HOL. Given an inductive problem in any problem domain, smart_induct
lists promising arguments for the induct tactic without relying on a search.
Our evaluation demonstrated smart_induct produces valuable recommendations
across problem domains.
Related papers
- An Incomplete Loop: Deductive, Inductive, and Abductive Learning in Large Language Models [99.31449616860291]
Modern language models (LMs) can learn to perform new tasks in different ways.
In instruction following, the target task is described explicitly in natural language; in few-shot prompting, the task is specified implicitly.
In instruction inference, LMs are presented with in-context examples and are then prompted to generate a natural language task description.
arXiv Detail & Related papers (2024-04-03T19:31:56Z) - Phenomenal Yet Puzzling: Testing Inductive Reasoning Capabilities of Language Models with Hypothesis Refinement [92.61557711360652]
Language models (LMs) often fall short on inductive reasoning, despite achieving impressive success on research benchmarks.
We conduct a systematic study of the inductive reasoning capabilities of LMs through iterative hypothesis refinement.
We reveal several discrepancies between the inductive reasoning processes of LMs and humans, shedding light on both the potentials and limitations of using LMs in inductive reasoning tasks.
arXiv Detail & Related papers (2023-10-12T17:51:10Z) - Self-Polish: Enhance Reasoning in Large Language Models via Problem Refinement [50.62461749446111]
Self-Polish (SP) is a novel method that facilitates the model's reasoning by guiding it to progressively refine the given problems to be more comprehensible and solvable.
SP is to all other prompting methods of answer/reasoning side like CoT, allowing for seamless integration with state-of-the-art techniques for further improvement.
arXiv Detail & Related papers (2023-05-23T19:58:30Z) - Enhancing Large Language Models Against Inductive Instructions with
Dual-critique Prompting [55.15697111170836]
This paper reveals the behaviors of large language models (LLMs) towards textitinductive instructions and enhance their truthfulness and helpfulness accordingly.
After extensive human and automatic evaluations, we uncovered a universal vulnerability among LLMs in processing inductive instructions.
We identify that different inductive styles affect the models' ability to identify the same underlying errors, and the complexity of the underlying assumptions also influences the model's performance.
arXiv Detail & Related papers (2023-05-23T06:38:20Z) - User Guided Abductive Proof Generation for Answer Set Programming
Queries (Extended Version) [0.0]
We present a method for generating possible proofs of a query with respect to a given Answer Set Programming (ASP) rule set.
Given a (possibly empty) set of user provided facts, our method infers any additional facts that may be needed for the entailment of a query.
We also present a method to generate a set of directed edges corresponding to the justification graph for the query.
arXiv Detail & Related papers (2022-09-16T14:06:12Z) - Who Finds the Short Proof? An Exploration of variants of Boolos' Curious
Inference using Higher-order Automated Theorem Provers [62.997667081978825]
We report on an exploration of variants of Boolos' curious inference using higher-order automated theorem provers.
Surprisingly, only a single shorthand notation still had to be provided by hand.
All higher-order lemmas required for obtaining short proof are automatically discovered by the computer.
arXiv Detail & Related papers (2022-08-14T16:31:04Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
We present a novel stepwise method NLProofS (Natural Language Proof Search)
NLProofS learns to generate relevant steps conditioning on the hypothesis.
It achieves state-of-the-art performance on EntailmentBank and RuleTaker.
arXiv Detail & Related papers (2022-05-25T02:22:30Z) - Impossibility Results in AI: A Survey [3.198144010381572]
An impossibility theorem demonstrates that a particular problem or set of problems cannot be solved as described in the claim.
We have categorized impossibility theorems applicable to the domain of AI into five categories: deduction, indistinguishability, induction, tradeoffs, and intractability.
We conclude that deductive impossibilities deny 100%-guarantees for security.
arXiv Detail & Related papers (2021-09-01T16:52:13Z) - Definitional Quantifiers Realise Semantic Reasoning for Proof by
Induction [6.85316573653194]
SeLFiE is a query language to represent users' knowledge on how to apply the induct tactic in Isabelle/HOL.
For evaluation we build an automatic induction prover using SeLFiE.
Our new prover achieves 1.4 x 103% improvement over the corresponding baseline prover for 1.0 second timeout and the median value of speedup is 4.48x.
arXiv Detail & Related papers (2020-10-19T09:05:09Z) - Faster Smarter Induction in Isabelle/HOL [6.85316573653194]
sem_ind recommends what arguments to pass to the induct method.
definitional quantifiers allow us to investigate not only the syntactic structures of inductive problems but also the definitions of relevant constants in a domain-agnostic style.
arXiv Detail & Related papers (2020-09-19T11:51:54Z) - Towards United Reasoning for Automatic Induction in Isabelle/HOL [6.85316573653194]
We propose united reasoning, a novel approach to further automating inductive theorem proving.
After success, united reasoning takes the best of three schools of reasoning: deductive reasoning, inductive reasoning, and inductive reasoning.
arXiv Detail & Related papers (2020-05-25T08:30:05Z)
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.