-
Template-Based Conjecturing for Automated Induction in Isabelle/HOL
Abstract: Proof by induction plays a central role in formal verification. However, its automation remains as a formidable challenge in Computer Science. To solve inductive problems, human engineers often have to provide auxiliary lemmas manually. We automate this laborious process with template-based conjecturing, a novel approach to generate auxiliary lemmas and use them to prove final goals. Our evaluatio… ▽ More
Submitted 19 January, 2023; v1 submitted 20 November, 2022; originally announced December 2022.
Comments: To appear at Fundamentals of Software engineering 2023 (http://fsen.ir/2023/)
-
Genetic Algorithm for Program Synthesis
Abstract: A deductive program synthesis tool takes a specification as input and derives a program that satisfies the specification. The drawback of this approach is that search spaces for such correct programs tend to be enormous, making it difficult to derive correct programs within a realistic timeout. To speed up such program derivation, we improve the search strategy of a deductive program synthesis too… ▽ More
Submitted 19 January, 2023; v1 submitted 21 November, 2022; originally announced November 2022.
-
Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
Abstract: Proof assistants offer tactics to apply proof by induction, but these tactics rely on inputs given by human engineers. To automate this laborious process, we developed SeLFiE, a boolean query language to represent experienced users' knowledge on how to apply the induct tactic in Isabelle/HOL: when we apply an induction heuristic written in SeLFiE to an inductive problem and arguments to the induct… ▽ More
Submitted 20 May, 2022; v1 submitted 19 October, 2020; originally announced October 2020.
Comments: This is the preprint of our paper accepted at Tests and Proofs 2022. arXiv admin note: substantial text overlap with arXiv:2009.09215
-
Faster Smarter Induction in Isabelle/HOL
Abstract: Proof by induction plays a critical role in formal verification and mathematics at large. However, its automation remains as one of the long-standing challenges in Computer Science. To address this problem, we developed sem_ind. Given inductive problem, sem_ind recommends what arguments to pass to the induct method. To improve the accuracy of sem_ind, we introduced definitional quantifiers, a new… ▽ More
Submitted 9 May, 2021; v1 submitted 19 September, 2020; originally announced September 2020.
Comments: This is the preprint of our paper of the same title, which is accepted to IJCAI2021. For the formal proceeding, please refer to the IJCAI2021 website
-
Towards United Reasoning for Automatic Induction in Isabelle/HOL
Abstract: Inductive theorem proving is an important long-standing challenge in computer science. In this extended abstract, we first summarize the recent developments of proof by induction for Isabelle/HOL. Then, we propose united reasoning, a novel approach to further automating inductive theorem proving. Upon success, united reasoning takes the best of three schools of reasoning: deductive reasoning, indu… ▽ More
Submitted 25 May, 2020; originally announced May 2020.
Comments: This is the pre-print of our short-paper accepted at the 34th Annual Conference of the Japanese Society for Artificial Intelligence, 2020 (https://www.ai-gakkai.or.jp/jsai2020/en)
-
arXiv:2004.10667 [pdf, ps, other]
Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
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 des… ▽ More
Submitted 26 May, 2020; v1 submitted 21 April, 2020; originally announced April 2020.
Comments: This is the preprint of our short paper accepted at the 13th Conference on Intelligent Computer Mathematics (CICM 2020)
-
Smart Induction for Isabelle/HOL (System Description)
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 demonstrat… ▽ More
Submitted 27 January, 2020; originally announced January 2020.
Comments: Under submission at IJCAR2020 as a System Description
-
arXiv:1907.02594 [pdf, ps, other]
Domain-Specific Language to Encode Induction Heuristics
Abstract: Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however, they did not have a systematic way to encode their expertise. To address this problem, we present our domain-specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heuristics in a style independent of… ▽ More
Submitted 29 June, 2019; originally announced July 2019.
Comments: Accepted at ICFP2019-SRC (International Conference on Functional Programming Student Research Competition). Our draft, "LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL" (arXiv:1906.08084), gives further details of this domain specific language. arXiv admin note: substantial text overlap with arXiv:1906.08084
-
arXiv:1906.08549 [pdf, ps, other]
Designing Game of Theorems
Abstract: "Theorem proving is similar to the game of Go. So, we can probably improve our provers using deep learning, like DeepMind built the super-human computer Go program, AlphaGo." Such optimism has been observed among participants of AITP2017. But is theorem proving really similar to Go? In this paper, we first identify the similarities and differences between them and then propose a system in which va… ▽ More
Submitted 20 June, 2019; originally announced June 2019.
Comments: Presented at the third Conference on Artificial Intelligence and Theorem Proving (AITP 2018)
-
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
Abstract: Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however, there is a little tool support for transferring this expert knowledge to a wider user audience. To address this problem, we present our domain-specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heu… ▽ More
Submitted 24 May, 2020; v1 submitted 19 June, 2019; originally announced June 2019.
Comments: This is the pre-print of our paper of the same title accepted at APLAS2019 (https://doi.org/10.1007/978-3-030-34175-6_14). We updated the draft after fixing the errata found by Kenji Miyamoto
-
arXiv:1904.08468 [pdf, ps, other]
Towards Evolutionary Theorem Proving for Isabelle/HOL
Abstract: Mechanized theorem proving is becoming the basis of reliable systems programming and rigorous mathematics. Despite decades of progress in proof automation, writing mechanized proofs still requires engineers' expertise and remains labor intensive. Recently, researchers have extracted heuristics of interactive proof development from existing large proof corpora using supervised learning. However, su… ▽ More
Submitted 17 April, 2019; originally announced April 2019.
Comments: 2 pages, This is a pre-print of our poster-only paper accepted at GECCO'19. For the final version, please visit the corresponding ACM website
-
Towards Machine Learning Induction
Abstract: Induction lies at the heart of mathematics and computer science. However, automated theorem proving of inductive problems is still limited in its power. In this abstract, we first summarize our progress in automating inductive theorem proving for Isabelle/HOL. Then, we present MeLoId, our approach to suggesting promising applications of induction without completing a proof search.
Submitted 26 March, 2019; v1 submitted 4 December, 2018; originally announced December 2018.
Comments: This abstract is submitted to the fourth Conference on Artificial Intelligence (AITP2019) and Theorem Proving and to the third Workshop on Learning in Verification (LiVE2019)
-
PaMpeR: Proof Method Recommendation System for Isabelle/HOL
Abstract: Deciding which sub-tool to use for a given proof state requires expertise specific to each ITP. To mitigate this problem, we present PaMpeR, a Proof Method Recommendation system for Isabelle/HOL. Given a proof state, PaMpeR recommends proof methods to discharge the proof goal and provides qualitative explanations as to why it suggests these methods. PaMpeR generates these recommendations based on… ▽ More
Submitted 19 June, 2018; originally announced June 2018.
Comments: An anonymized version of this paper has been submitted to a Computer Science conference in April 2018
-
Goal-Oriented Conjecturing for Isabelle/HOL
Abstract: We present PGT, a Proof Goal Transformer for Isabelle/HOL. Given a proof goal and its background context, PGT attempts to generate conjectures from the original goal by transforming the original proof goal. These conjectures should be weak enough to be provable by automation but sufficiently strong to prove the original goal. By incorporating PGT into the pre-existing PSL framework, we exploit Isa… ▽ More
Submitted 25 July, 2018; v1 submitted 12 June, 2018; originally announced June 2018.
Comments: This paper has been accepted at 11th Conference on Intelligent Computer Mathematics. An error in Abstract has been fixed
-
arXiv:1701.03037 [pdf, ps, other]
Towards Smart Proof Search for Isabelle
Abstract: Despite the recent progress in automatic theorem provers, proof engineers are still suffering from the lack of powerful proof automation. In this position paper we first report our proof strategy language based on a meta-tool approach. Then, we propose an AI-based approach to drastically improve proof automation for Isabelle, while identifying three major challenges we plan to address for this obj… ▽ More
Submitted 10 January, 2017; originally announced January 2017.
Comments: Accepted at AITP2017
-
arXiv:1608.03350 [pdf, ps, other]
Close Encounters of the Higher Kind Emulating Constructor Classes in Standard ML
Abstract: We implement a library for encoding constructor classes in Standard ML, including elaboration from minimal definitions, and automatic instantiation of superclasses.
Submitted 10 August, 2016; originally announced August 2016.
Comments: Accepted by ACM SIGPLAN Workshop on ML, September 2016
-
A Proof Strategy Language and Proof Script Generation for Isabelle/HOL
Abstract: We introduce a language, PSL, designed to capture high level proof strategies in Isabelle/HOL. Given a strategy and a proof obligation, PSL's runtime system generates and combines various tactics to explore a large search space with low memory usage. Upon success, PSL generates an efficient proof script, which bypasses a large part of the proof search. We also present PSL's monadic interpreter to… ▽ More
Submitted 1 March, 2017; v1 submitted 9 June, 2016; originally announced June 2016.
Comments: This paper has been submitted to CADE26
-
COGENT: Certified Compilation for a Functional Systems Language
Abstract: We present a self-certifying compiler for the COGENT systems language. COGENT is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. It compiles to efficient C code that is designed to interoperate with existing C functions. The language is suited for layered systems code with minimal sharing suc… ▽ More
Submitted 21 January, 2016; originally announced January 2016.