Statistical Proof Pattern Recognition: Automated or Interactive?

Jónathan Heras; Ekaterina Komendantskaya

Statistical Proof Pattern Recognition: Automated or Interactive?

Software Engineering 2013-03-07 v1 Logic in Computer Science

Authors: Jónathan Heras , Ekaterina Komendantskaya

Abstract

In this paper, we compare different existing approaches employed in data mining of big proof libraries in automated and interactive theorem proving.

Keywords

theorem proving machine learning

Cite

@article{arxiv.1303.1419,
  title  = {Statistical Proof Pattern Recognition: Automated or Interactive?},
  author = {Jónathan Heras and Ekaterina Komendantskaya},
  journal= {arXiv preprint arXiv:1303.1419},
  year   = {2013}
}

Related papers

View all related →

Programming Languages · Computer Science

Proof Mining with Dependent Types

Ekaterina Komendantskaya, Jonathan Heras

2017-05-23

Logic in Computer Science · Computer Science

Mining State-Based Models from Proof Corpora

Thomas Gransden, Neil Walkinshaw, Rajeev Raman

2014-05-15

Logic in Computer Science · Computer Science

Automatic verification and interactive theorem proving

Andrea Asperti

2017-01-16

Logic in Computer Science · Computer Science

Learning Rules Explaining Interactive Theorem Proving Tactic Prediction

Liao Zhang, David M. Cerna, Cezary Kaliszyk

2024-11-05

Artificial Intelligence · Computer Science

Learning Guided Automated Reasoning: A Brief Survey

Lasse Blaauwbroek, David Cerna, Thibault Gauthier, Jan Jakubův +3

2025-06-23

Programming Languages · Computer Science

Automated Discovery of Tactic Libraries for Interactive Theorem Proving

Yutong Xin, Jimmy Xin, Gabriel Poesia, Noah Goodman +2

2025-08-26

Artificial Intelligence · Computer Science

Recycling Proof Patterns in Coq: Case Studies

Jónathan Heras, Ekaterina Komendantskaya

2014-03-10

Logic in Computer Science · Computer Science

Understanding and Improving Automated Proof Synthesis for Interactive Theorem Provers

Manqing Zhang, Yunwei Dong, Lingru Zhou, Bingxu Xiao +1

2026-04-28

Quantum Physics · Physics

Interactive Proofs with Quantum Finite Automata

Harumichi Nishimura, Tomoyuki Yamakami

2015-08-25

Artificial Intelligence · Computer Science

Interactive Benchmarks

Baoqing Yue, Zihan Zhu, Yutong Han, Brian Fan +5

2026-05-19

Artificial Intelligence · Computer Science

Neural Interactive Proofs

Lewis Hammond, Sam Adam-Day

2025-03-19

Logic in Computer Science · Computer Science

Automated Verification of Reactive and Concurrent Programs by Calculation

Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock

2021-04-19

Logic in Computer Science · Computer Science

SCTL: Towards Combining Model Checking and Proof Checking

Ying Jiang, Jian Liu, Gilles Dowek, Kailiang Ji

2017-10-03

Methodology · Statistics

Imputation procedures in surveys using nonparametric and machine learning methods: an empirical comparison

Mehdi Dagdoug, Camelia Goga, David Haziza

2022-08-23

Artificial Intelligence · Computer Science

BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving

Sean Lamont, Michael Norrish, Amir Dezfouli, Christian Walder +1

2025-02-14

Logic in Computer Science · Computer Science

AutoProof: Auto-active Functional Verification of Object-oriented Programs

Julian Tschannen, Carlo A. Furia, Martin Nordio, Nadia Polikarpova

2015-09-01

Logic in Computer Science · Computer Science

A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving

Freek Wiedijk

2015-07-01

Machine Learning · Computer Science

Towards Better Analysis of Machine Learning Models: A Visual Analytics Perspective

Shixia Liu, Xiting Wang, Mengchen Liu, Jun Zhu

2017-02-07

Machine Learning · Computer Science

An Interactive Visualization Tool for Understanding Active Learning

Zihan Wang, Jialin Lu, Oliver Snow, Martin Ester

2021-11-10

Artificial Intelligence · Computer Science

Towards Smart Proof Search for Isabelle

Yutaka Nagashima

2017-01-12

Distributed, Parallel, and Cluster Computing · Computer Science

Trade-offs in Distributed Interactive Proofs

Pierluigi Crescenzi, Pierre Fraigniaud, Ami Paz

2019-08-12

Other Computer Science · Computer Science

Reliability of Checking an Answer Given by a Mathematical Expression in Interactive Learning Systems

Vladimir G. Danilov, Ilya S. Turuntaev

2016-02-02

Computational Complexity · Computer Science

Pseudo-deterministic Proofs

Shafi Goldwasser, Ofer Grossman, Dhiraj Holden

2017-06-16

Artificial Intelligence · Computer Science

LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation

Junyu Lai, Jiakun Zhang, Shuo Xu, Taolue Chen +5

2025-05-20

Logic in Computer Science · Computer Science

Compositional pre-processing for automated reasoning in dependent type theory

Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque +3

2024-02-22