TacTok: Semantics-Aware Proof Synthesis
summary
Automatic proof synthesis that combines both goal semantics and prior scripts, not just one or the other. TacTok models proof state and proof script together and uses a TreeLSTM proof-state encoder plus a BiLSTM script encoder with an AST tactic decoder. Trained on CoqGym (57,719 human proofs, 10,782 test theorems), TacTok achieves a 12.9% success rate, proves 329 theorems CoqHammer misses (an 11.5% added value), and complements ASTactic by proving 20% more theorems.
AI-written summary · about
chapters (6)
- 0:00Start
- 0:23Formal Verification of Software Is Important
- 1:00Examples of Substantial Verification Efforts
- 6:48Meta-Heuristic Search
- 8:05Proof State Encoder
- 10:29Success Rates
related talks
22mTurning Catala into a Proof Platform for the Law
28mC2TACO: Lifting Tensor Code to TACO
01h 34mFormal Logic Undressed
15mTabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
30mSemantics-Guided Synthesis
18mDeveloping a Dependently Typed Language with Runtime Proof Search
14mHigher-order Automation In TLAPS
19mExtensible Metatheory Mechanization via Family Polymorphism