Formally Specifying the Intended Behavior of the Program: LLM-Driven Neuro-Symbolic Program Specification Synthesis (2026.acl-demo)
Copied to clipboard
Cheng Wen, Hu Junjie, YiKun Hu, Jie Su, Bin Yu, Dugang Liu, Zhiwu Xu, Weidi Sun, Shengchao Qin, Cong Tian
| Challenge: | Formal verification typically requires developers to write detailed formal specifications . a formal verification system that generates candidate specifications is costly and error-prone . |
| Approach: | They propose an LLM-driven neuro-symbolic demonstration system that reframes specification writing as constrained structured synthesis. |
| Outcome: | The proposed system reduces hallucinations and produces proof-ready annotations. |
Similar Papers
AutoSpec: An Agentic Framework for Automatically Drafting Patent Specification (2025.findings-emnlp)
Copied to clipboard
| Challenge: | drafting a patent application is expensive and time-consuming, making it a prime candidate for automation. |
| Approach: | a new framework automates the process of drafting a patent application . the framework decomposes drafting into manageable subtasks . |
| Outcome: | a new framework outperforms existing baselines on drafting patent specification tasks. |
Adaptive LLM-Symbolic Reasoning via Dynamic Logical Solver Composition (2026.eacl-long)
Copied to clipboard
| Challenge: | Existing approaches to NLP are static and require manual formalization. |
| Approach: | They propose an adaptive, multi-paradigm, neuro-symbolic inference framework that automatically identifies formal reasoning strategies from problems expressed in natural language and dynamically selects and applies specialized formal logical solvers. |
| Outcome: | The proposed framework outperforms baselines on individual and multi-paradigm reasoning tasks by 17% and 6%. |
Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference (2025.acl-long)
Copied to clipboard
| Challenge: | Large Language Models (LLMs) are increasingly being used to automate programming tasks. |
| Approach: | They propose a benchmark to evaluate LLMs' reasoning abilities on program semantics. |
| Outcome: | The proposed benchmark shows that LLMs perform well with simple control flows but struggle with more complex structures, especially loops, even with advanced prompting. |
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. |
Integrating Symbolic Execution into the Fine-Tuning of Code-Generating LLMs (2025.naacl-srw)
Copied to clipboard
| Challenge: | Code-generating Large Language Models (LLMs) have become essential tools in modern software development, enhancing productivity and accelerating development. |
| Approach: | They propose to use Reinforcement Learning and Direct Preference Optimization to fine-tune code-generating Large Language Models (LLMs) by enhancing the training data with symbolic execution techniques. |
| Outcome: | The proposed model improves on the CodeRL benchmark and shows that it is more accurate and objective than the baseline model. |
PEIRCE: Unifying Material and Formal Reasoning via LLM-Driven Neuro-Symbolic Refinement (2025.acl-demo)
Copied to clipboard
| Challenge: | Large Language Models (LLMs) are capable of material inference but lack formal rigour and verifiability. |
| Approach: | They propose a framework to unify material and formal inference through an iterative conjecture–criticism process. |
| Outcome: | The proposed framework unifies material and formal inference through an iterative conjecture–criticism process. |
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%. |
ConstraintLLM: A Neuro-Symbolic Framework for Industrial-Level Constraint Programming (2025.emnlp-main)
Copied to clipboard
| Challenge: | Constraint programming (CP) is a powerful paradigm for solving constraint optimization problems. |
| Approach: | They propose to use an open-source LLM to generate formal modeling for COPs. |
| Outcome: | The proposed model outperforms the baselines on the new IndusCP benchmark by 2x. |
SynthFix: Adaptive Neuro-Symbolic Code Vulnerability Repair (2026.findings-acl)
Copied to clipboard
| Challenge: | Large Language Models (LLMs) struggle with complex semantic and structural correctness required for automated code repair. |
| Approach: | They propose a hybrid neural-symbolic framework that unifies code synthesis with compiler-informed symbolic feedback to improve LLM-based vulnerability repair. |
| Outcome: | The proposed framework improves code repair accuracy and efficiency over strong SFT and RFT training strategies on the FixJS and CodeFlaws benchmarks. |
Unifying Inference-Time Planning Language Generation (2026.findings-acl)
Copied to clipboard
Prabhu Prakash Kagitha, Bo Sun, Ishan Desai, Andrew Zhu, Cassie Huang, Manling Li, Ziyang Li, Li Zhang
| Challenge: | Large language models (LLMs) are used to generate a formal representation of a plan in a planning language. |
| Approach: | They propose a unifying organizational framework based on intermediate representations to unify the inference-time LLM-as-formalizer methodology for classical planning. |
| Outcome: | The proposed framework subsumes most existing work and proposes new ones that involve syntactically similar but high-resource intermediate languages. |