Towards United Reasoning for Automatic Induction in Isabelle/HOL
CIIRC, Czech Technical University in Prague（捷克布拉格技术大学捷克信息学、机器人学与控制论研究所）；University of Innsbruck（因斯布鲁克大学）
Yutaka Nagashima
备注：
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)
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, inductive reasoning, and inductive reasoning, to prove difficult inductive problems automatically.
Freie Universität Berlin（柏林自由大学）；Cambridge University（剑桥大学）
We present an automated verification of the well-known modal logic cube in Isabelle/HOL, in which we prove the inclusion relations between the cube's logics using automated reasoning tools. Prior work addresses this problem but without restriction to the modal logic cube, and using encodings in first-order logic in combination with first-order automated theorem provers. In contrast, our solution is more elegant, transparent and effective. It employs an embedding of quantified modal logic in classical higher-order logic. Automated reasoning tools, such as Sledgehammer with LEO-II, Satallax and …
University of Innsbruck（因斯布鲁克大学）；Czech Technical University（捷克技术大学）
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, such existing proof corpora present only one way of proving conjectures, while there are often multiple equivalently effective ways to prove one conjecture. In this abstract, we identify challenges in d…
Czech Technical University in Prague（布拉格捷克理工大学）；University of Innsbruck（因斯布鲁克大学）；University of Sydney（悉尼大学）
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 existing hand-written proof corpora, thus transferring experienced users' expertise to new users. Our evaluation shows that PaMpeR correctly predicts experienced users' proof methods invocation especi…
HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
College of Computer Science and Technology Zhejiang University（浙江大学计算机科学与技术学院）；Siebel Center for Computer Science University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校计算机科学中心）
Czech Technical University in Prague（布拉格捷克理工大学）；University of Innsbruck（因斯布鲁克大学）
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.
Artificial Intelligence and its Applications Institute (AIAI), School of Informatics, University of Edinburgh（爱丁堡大学信息学院人工智能及其应用研究所）
We present a formalisation of finite Markov decision processes with rewards in the Isabelle theorem prover. We focus on the foundations required for dynamic programming and the use of reinforcement learning agents over such processes. In particular, we derive the Bellman equation from first principles (in both scalar and vector form), derive a vector calculation that produces the expected value of any policy p, and go on to prove the existence of a universally optimal policy where there is a discounting factor less than one. Lastly, we prove that the value iteration and the policy iteration al…
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 in particular. The use of Isabelle enables almost automatic grading of large parts of the exam. We explain our approach through a number of example problems, and explain why we believe that each of the kinds of problems we have selected are adequate measures of our intended learning outcom…
Czech Technical University in Prague（布拉格捷克理工大学）；University of Innsbruck（因斯布鲁克大学）
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 kno…
Munkres' General Topology Autoformalized in Isabelle/HOL
Independent（独立研究者）；Aalborg University（奥尔堡大学）；University of Melbourne（墨尔本大学）；AI4REASON and University of Gothenburg / Chalmers University（AI4REASON 和哥德堡大学 / 查尔姆斯理工大学）
Techniche Universität München（慕尼黑工业大学）；King’s College London（伦敦国王学院）
We present a simple and concise semantics for temporal planning. Our semantics are developed and formalised in the logic of the interactive theorem prover Isabelle/HOL. We derive from those semantics a validation algorithm for temporal planning and show, using a formal proof in Isabelle/HOL, that this validation algorithm implements our semantics. We experimentally evaluate our verified validation algorithm and show that it is practical.
Yale-NUS College, National University of Singapore（耶鲁-新加坡国立大学学院，新加坡国立大学）；University of Innsbruck（因斯布鲁克大学）；Czech Institute of Informatics, Robotics, and Cybernetics, Czech Technical University in Prague（布拉格捷克理工大学信息学、机器人与控制论研究所）
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 kind of quantifiers that allow us to investigate not only the syntactic structures of inductive problems but also the definitions of relevant constants in a domain-agnostic style. Our evaluation shows…
Computer Science and Communications, University of Luxembourg（卢森堡大学计算机科学与通信学院）
A flexible infrastructure for normative reasoning is outlined. A small-scale demonstrator version of the envisioned system has been implemented in the proof assistant Isabelle/HOL by utilising the first authors universal logical reasoning approach based on shallow semantical embeddings in meta-logic HOL. The need for such a flexible reasoning infrastructure is motivated and illustrated with a contrary-to-duty example scenario selected from the General Data Protection Regulation.
University of Luxemburg（卢森堡大学）；Freie Universität Berlin（柏林自由大学）
Starting from a generalization of the standard axioms for a monoid we present a stepwise development of various, mutually equivalent foundational axiom systems for category theory. Our axiom sets have been formalized in the Isabelle/HOL interactive proof assistant, and this formalization utilizes a semantically correct embedding of free logic in classical higher-order logic. The modeling and formal analysis of our axiom sets has been significantly supported by series of experiments with automated reasoning tools integrated with Isabelle/HOL. We also address the relation of our axiom systems to…
Learning-assisted automated reasoning has recently gained popularity among the users of Isabelle/HOL, HOL Light, and Mizar. In this paper, we present an add-on to the HOL4 proof assistant and an adaptation of the HOLyHammer system that provides machine learning-based premise selection and automated reasoning also for HOL4. We efficiently record the HOL4 dependencies and extract features from the theorem statements, which form a basis for premise selection. HOLyHammer transforms the HOL4 statements in the various TPTP-ATP proof formats, which are then processed by the ATPs. We discuss the diffe…
