Papers with ATP
Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4 (2026.acl-long)
Copied to clipboard
Chengwu Liu, Yichun Yin, Ye Yuan, Jiaxuan Xie, Botao Li, Siqi Li, Jianhao Shen, Yan Xu, Lifeng Shang, Ming Zhang
| Challenge: | Existing approaches to solving mathematical problems fall into two broad categories: informal methods and formal methods. |
| Approach: | They propose to use LLM natural-language reasoning to discover answers . they introduce Discover And Prove framework that rewrites Hard Mode statements into Easy Mode ones for existing ATP provers. |
| Outcome: | The proposed framework can be used to prove hard mode statements on ATP benchmarks. |
Towards Robustness of Text-to-SQL Models Against Natural and Realistic Adversarial Table Perturbation (2022.acl-long)
Copied to clipboard
| Challenge: | Existing Text-to-SQL parsers are vulnerable to perturbations in NL questions . we propose the Adversarial Table Perturbation (ATP) as a new attacking paradigm . |
| Approach: | They propose to use the Adversarial Table Perturbation to measure robustness of Text-to-SQL parsers against adversarial perturbations. |
| Outcome: | The proposed approach outperforms baseline methods in robustness evaluations on ADVETA and can be used in future projects. |
Neural Unification for Logic Reasoning over Natural Language (2021.findings-emnlp)
Copied to clipboard
| Challenge: | Automated Theorem Proving (ATP) is a computer program that can show that conjectures are logical consequences of a set of axioms. |
| Approach: | They propose a transformer-based architecture for deriving conjectures given axioms . they propose 'neural unifier' and relative training procedure to train the model . |
| Outcome: | The proposed architectures are able to answer queries with deep queries with a relatively low training time. |
TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models (2023.emnlp-main)
Copied to clipboard
Jing Xiong, Jianhao Shen, Ye Yuan, Haiming Wang, Yichun Yin, Zhengying Liu, Lin Li, Zhijiang Guo, Qingxing Cao, Yinya Huang, Chuanyang Zheng, Xiaodan Liang, Ming Zhang, Qun Liu
| Challenge: | Automated theorem proving (ATP) benchmarks focus on symbolic inference but rarely involve understanding complex number combination reasoning. |
| Approach: | They propose a benchmark that requires a model to reduce a trigonometric expression with step-by-step proof and evaluates a generative LM’s reasoning ability on formulas and ability to manipulate, group, and factor number terms. |
| Outcome: | The proposed benchmark evaluates a generative LM’s reasoning ability on formulas and ability to manipulate, group, and factor number terms. |
Virtual Personas for Language Models via an Anthology of Backstories (2024.emnlp-main)
Copied to clipboard
| Challenge: | Large language models (LLMs) are trained from vast repositories of text authored by millions of distinct authors, reflecting an enormous diversity of human traits. |
| Approach: | They propose a method for conditioning LLMs to particular virtual personas by harnessing open-ended life narratives, which they refer to as backstories, and demonstrate that it improves consistency and reliability of experimental outcomes. |
| Outcome: | The proposed method improves consistency and reliability of experimental outcomes while ensuring better representation of diverse sub-populations. |
EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Proving (2026.acl-long)
Copied to clipboard
| Challenge: | Large Language Models (LLMs) have recently advanced the field of Automated Theorem Proving (ATP) Existing cost analyses regulate only the number of sampling passes, ignoring the substantial disparities in sampling costs. |
| Approach: | They propose to integrate two complementary methods into a unified EconRL pipeline to increase pass rates under constrained sampling passes. |
| Outcome: | The proposed method reduces token usage and sample passes while maintaining the original performance. |