Sat 13 Jan 2018 15:00 - 15:30 at Crocker - Session 2 Chair(s): William E. Byrd

Inspired by the recent evolution of deep neural networks (DNNs) in machine learning, we explore their application to the problems that often appear in the research of programming languages (PL problems), such as program synthesis and automated theorem proving. As a first step towards this goal, we report the result of our preliminary experimental result of the application of DNNs to proof synthesis of the intuitionistic propositional logic. The idea is to view the proof-synthesis problem as a translation from a proposition to its proof. We train a seq2seq model, which is a popular model in neural machine translation, so that it generates a proof term from a given proposition. We empirically observe that, although the generated proof is correct only for approximately half of the propositions in the test data, a generated proof term is close to a correct one in terms of the tree edit distance of AST. Based on this observation, we implemented a proof-search procedure that uses the generated proof term as a hint, which outperforms a brute-force one. We discuss future research directions and the gaps to be filled between DNN and PL problems.

Abstract (obt18-paper8.pdf)546KiB

Conference Day
Sat 13 Jan

Displayed time zone: Tijuana, Baja California change

13:30 - 15:30
Session 2Off the Beaten Track at Crocker
Chair(s): William E. ByrdUniversity of Alabama at Birmingham, USA
13:30
30m
Lunch
Lunch (12pm-2pm)
Off the Beaten Track

14:00
30m
Talk
SweetPea: A Language for Designing Experiments
Off the Beaten Track
Annie CherkaevUniversity of Utah, Sebastian MusslickPrinceton University, Jonathan CohenPrinceton University, Vivek SrikumarUniversity of Utah, Matthew FlattUniversity of Utah
File Attached
14:30
30m
Talk
Extensible Semantics for Fluidics
Off the Beaten Track
Max WillseyUniversity of Washington, Jared RoeschUniversity of Washington, USA
File Attached
15:00
30m
Talk
Towards Proof Synthesis by Neural Machine Translation
Off the Beaten Track
Taro SekiyamaIBM Research, Japan, Akifumi ImanishiKyoto University, Kohei SuenagaGraduate School of Informatics, Kyoto University
File Attached