FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean (2026.acl-long)
Copied to clipboard
| Challenge: | Formalising informal mathematical reasoning into formally verifiable code is a significant challenge for large language models. |
| Approach: | They propose a domain-agnostic human-in-the-loop agentic pipeline to aid autoformalisation in scientific domains. |
| Outcome: | The proposed system produces syntactically correct and semantically aligned proofs for low cost. |
Similar Papers
Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions (2025.emnlp-main)
Copied to clipboard
| Challenge: | Large Language Models (LLMs) have demonstrated remarkable potential in assisting with mathematical reasoning on different downstream tasks. |
| Approach: | They propose two new tools for autoformalizing real-world mathematical definitions from Wikipedia and arXiv papers. |
| Outcome: | The proposed methods improve definitions by up to 16% and undefined errors by 43%. |
Consistent Autoformalization for Constructing Mathematical Libraries (2024.emnlp-main)
Copied to clipboard
| Challenge: | Autoformalization is the task of automatically translating mathematical content written in natural language to a formal language expression. |
| Approach: | They propose to use three mechanisms to improve autoformalization quality . they propose to combine most-similar retrieval augmented generation, denoising steps and auto-correction with syntax error feedback to improve syntactic, terminological and semantic control. |
| Outcome: | The proposed mechanisms can deliver syntactically, terminologically and semantically more consistent results across different models. |
From Informal to Formal – Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs (2025.acl-long)
Copied to clipboard
Jialun Cao, Yaojie Lu, Meiziniu Li, Haoyang Ma, Haokun Li, Mengda He, Cheng Wen, Le Sun, Hongyu Zhang, Shengchao Qin, Shing-Chi Cheung, Cong Tian
| Challenge: | Recent studies in formal mathematical reasoning have shown an unstoppable growth trend. |
| Approach: | They constructed 18k high-quality instruction-response pairs across five mainstream formal specification languages and evaluated them against ten open-sourced LLMs. |
| Outcome: | The proposed model compared instruction-response pairs across five formal specification languages and found that the LLMs were good at writing proof segments when given either the code, or the detailed description of proof steps. |
DataSciBench: An LLM Agent Benchmark for Data Science (2026.findings-acl)
Copied to clipboard
Dan Zhang, Sining Zhoubian, Min Cai, Fengzu Li, Lekang Yang, Wei Wang, Tianjiao Dong, Ziniu Hu, Jie Tang, Yisong Yue
| Challenge: | Existing benchmarks focus on single task, simple evaluation metrics, and readily available ground truth (GT) DataSciBench is built on curated, natural, and challenging prompts with complex evaluation criteria and uncertain GT. |
| Approach: | They propose a benchmark for evaluating Large Language Models in data science that integrates LLM-based self-consistency and human verification to ensure accuracy. |
| Outcome: | The proposed framework outperforms open-source models in all metrics and offers rigorous insights into LLM strengths and weaknesses. |
MASA: LLM-Driven Multi-Agent Systems for Autoformalization (2025.emnlp-demos)
Copied to clipboard
| Challenge: | This paper presents a framework for building multi-agent systems for autoformalization driven by Large Language Models. |
| Approach: | They propose a framework for building multi-agent systems for autoformalization driven by Large Language Models. |
| Outcome: | The proposed framework leverages collaborative agents to convert natural language statements into formal representations. |
AutoSDT: Scaling Data-Driven Discovery Tasks Toward Open Co-Scientists (2025.emnlp-main)
Copied to clipboard
Yifei Li, Hanane Nour Moussa, Ziru Chen, Shijie Chen, Botao Yu, Mingyi Xue, Benjamin Burns, Tzu-Yao Chiu, Vishal Dey, Zitong Lu, Chen Wei, Qianheng Zhang, Tianyu Zhang, Song Gao, Xuhui Huang, Xia Ning, Nesreen K. Ahmed, Ali Payani, Huan Sun
| Challenge: | AutoSDT-5K is the only automatically collected and the largest open dataset for data-driven scientific discovery. |
| Approach: | They propose an automatic pipeline that collects high-quality coding tasks in real-world data-driven discovery workflows. |
| Outcome: | The proposed pipeline synthesizes accurate tasks and tasks from a dataset of 5,404 tasks covering four scientific disciplines and 756 Python packages. |
TinyScientist: An Interactive, Extensible, and Controllable Framework for Building Research Agents (2025.emnlp-demos)
Copied to clipboard
Haofei Yu, Keyang Xuan, Fenghai Li, Kunlun Zhu, Zijie Lei, Jiaxun Zhang, Ziheng Qi, Kyle Richardson, Jiaxuan You
| Challenge: | Existing research systems often design and use agentic workflows to perform research tasks such as ideation, scientific coding, review writing, and tree-based search. |
| Approach: | They propose an open-source codebase, an interactive web demonstration, and a PyPI Python package to make state-of-the-art auto-research pipelines broadly accessible to every researcher and developer. |
| Outcome: | The proposed framework adapts easily to new tools and supports iterative growth. |
CodeScientist: End-to-End Semi-Automated Scientific Discovery with Code-based Experimentation (2025.findings-acl)
Copied to clipboard
Peter Jansen, Oyvind Tafjord, Marissa Radensky, Pao Siangliulue, Tom Hope, Bhavana Dalvi Mishra, Bodhisattwa Prasad Majumder, Daniel S Weld, Peter Clark
| Challenge: | Automated scientific discovery (ASD) systems are limited in their evaluation of software artifacts and large volumes of research artifs are typically evaluated using conference-style paper review with limited evaluation of code. |
| Approach: | They propose a novel ASD system that frames ideation and experiment construction as a form of genetic search jointly over combinations of research articles and codeblocks defining common actions in a domain. |
| Outcome: | The proposed system returns 19 discoveries on machine-generated ideas in the domain of agents and virtual environments. |
Data-Centric Perspectives on Agentic Retrieval-Augmented Generation: A Survey (2026.findings-acl)
Copied to clipboard
| Challenge: | Large Language Models (LLMs) excel at natural language understanding and generation, yet rely on static pre-training data. |
| Approach: | They propose to augment Large Language Models with external retrieval to ground model outputs . traditional RAG is constrained by a fixed retrieve-then-generate routine . authors aim to guide creation of high-quality datasets for next generation of adaptive LLM agents . |
| Outcome: | The proposed model can decompose tasks, issue exploratory queries, and refine evidence through iterative retrieval. |
AdaptFlow: Adaptive Workflow Optimization via Meta-Learning (2025.findings-emnlp)
Copied to clipboard
Runchuan Zhu, Bowen Jiang, Lingrui Mei, Fangkai Yang, Lu Wang, Haoxiang Gao, Fengshuo Bai, Pu Zhao, Qingwei Lin, Saravan Rajmohan, Dongmei Zhang
| Challenge: | Existing approaches to large language models rely on static templates or manual workflows. |
| Approach: | AdaptFlow is a language-based meta-learning framework inspired by model-agnostic meta- learning. |
| Outcome: | AdaptFlow outperforms manual and automated workflows on question answering, code generation and mathematical reasoning benchmarks. |