Papers by Sorin Lerner
Learn from Failure: Fine-tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving (2024.acl-long)
Copied to clipboard
Chenyang An, Zhibo Chen, Qihao Ye, Emily First, Letian Peng, Jiayun Zhang, Zihan Wang, Sorin Lerner, Jingbo Shang
| Challenge: | Recent advances in Automated Theorem Proving have shown the effectiveness of leveraging a (large) language model that generates tactics (i.e. proof steps) to search through proof states. |
| Approach: | They propose to use a large language model that generates tactics to search through proof states. |
| Outcome: | The proposed model solves more unseen theorems with lower trial searches than the current model, which only learns from failed attempts. |