Papers with autoformalisation
Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving (2024.emnlp-main)
Copied to clipboard
| Challenge: | Existing methods for assessing the validity of explanations for NLI are time-consuming and prone to logical errors. |
| Approach: | They propose a framework that integrates Large Language Models and Theorem Provers to verify and refine natural language explanations through crowd-sourcing . they propose to use TPs to generate and formalise explanatory sentences and suggest potential inference strategies for NLI. |
| Outcome: | The proposed framework generates and formalises explanatory sentences and suggests potential inference strategies for NLI. |
Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations (2025.acl-long)
Copied to clipboard
| Challenge: | Recent work has shown that the interaction of large language models (LLMs) with theorem provers (TPs) can help verify and improve the validity of NLI explanations. |
| Approach: | They propose to use logical expressions to guide LLMs in generating structured proof sketches and to use them to improve their accuracy. |
| Outcome: | The proposed strategies improve autoformalisation, syntactic errors and explanation refinement over the state-of-the-art model. |
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. |