Natural Language Reasoning using Coq: Interaction and Automation
Dans cet article, nous pr{\'e}sentons une utilisation des assistants des preuves pour traiter l{'}inf{\'e}rence en Language Naturel (NLI). D{'} abord, nous proposons d{'}utiliser les theories des types modernes comme langue dans laquelle traduire la s{\'e}mantique du langage naturel. Ensuite, nous impl{\'e}mentons cette s{\'e}mantique dans l{'}assistant de preuve Coq pour raisonner sur ceux-ci. En particulier, nous {\'e}valuons notre proposition sur un sous-ensemble de la suite de tests FraCas, et nous montrons que 95.2{\%} des exemples peuvent {\^e}tre correctement pr{\'e}dits. Nous discutons ensuite la question de l{'}automatisation et il est d{\'e}montr{\'e} que le langage de tactiques de Coq permet de construire des tactiques qui peuvent automatiser enti{\`e}rement les preuves, au moins pour les cas qui nous int{\'e}ressent.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Steward: Natural Language Web Automation
Recently, large language models (LLMs) have demonstrated exceptional capabilities in serving as the foundation for AI assistants. One emerging application of LLMs, navigating through websites and interacting with UI elem…
AutoEDA: Enabling EDA Flow Automation through Microservice-Based LLM Agents
Electronic Design Automation (EDA) remains heavily reliant on tool command language (Tcl) scripting to drive complex RTL-to-GDSII flows. This scripting-based paradigm is labor-intensive, error-prone, and difficult to sca…
InfiGUIAgent: A Multimodal Generalist GUI Agent with Native Reasoning and Reflection
Graphical User Interface (GUI) Agents, powered by multimodal large language models (MLLMs), have shown great potential for task automation on computing devices such as computers and mobile phones. However, existing agent…
History-Aware Reasoning for GUI Agents
Advances in Multimodal Large Language Models have significantly enhanced Graphical User Interface (GUI) automation. Equipping GUI agents with reliable episodic reasoning capabilities is essential for bridging the gap bet…
Reinforcement LearningBuildArena: A Physics-Aligned Interactive Benchmark of LLMs for Engineering Construction
Engineering construction automation aims to transform natural language specifications into physically viable structures, requiring complex integrated reasoning under strict physical constraints. While modern LLMs possess…