In the realm of formal theorem proving, the Coq proof assistant stands out for its rigorous approach to verifying mathematical assertions and software correctness. Despite the advances in artificial intelligence and machine learning, the specialized nature of Coq syntax and semantics poses unique challenges for Large Language Models (LLMs). Addressing this gap, we present a comprehensive dataset specifically designed to enhance LLMs' proficiency in interpreting and generating Coq code. This dataset, derived from a collection of over 10,000 Coq source files, encompasses a wide array of propositions, proofs, and definitions, enriched with metadata including source references and licensing information. Our primary aim is to facilitate the development of LLMs capable of generating syntactically correct and semantically meaningful Coq constructs, thereby advancing the frontier of automated theorem proving. Initial experiments with this dataset have showcased its significant potential; models trained on this data exhibited enhanced accuracy in Coq code generation. Notably, a particular experiment revealed that a fine-tuned LLM was capable of generating 141 valid proofs for a basic lemma, highlighting the dataset's utility in facilitating the discovery of diverse and valid proof strategies. This paper discusses the dataset's composition, the methodology behind its creation, and the implications of our findings for the future of machine learning in formal verification. The dataset is accessible for further research and exploration: https://huggingface.co/datasets/florath/coq-facts-props-proofs-gen0-v1

Abstract-- This paper presents a Simple and effIcient Motion Prediction baseLine (SIMPL) for autonomous vehicles. Unlike conventional agent-centric methods with high accuracy but repetitive computations and scene-centric methods with compromised accuracy and generalizability, SIMPL delivers realtime, accurate motion predictions for all relevant traffic participants. To achieve improvements in both accuracy and inference speed, we propose a compact and efficient global feature fusion module that performs directed message passing in a symmetric manner, enabling the network to forecast future motion for all road users in a single feed-forward pass and mitigating accuracy loss caused by viewpoint shifting. Please refer to the attached video for more examples. To achieve better accuracy and robustness, a common solution is normalizing the scene context w.r.t. Motion forecasting for the surrounding traffic participants It means the normalization process and feature is essential in autonomous vehicles, especially for the encoding have to be executed repeatedly for each target downstream decision-making and planning modules, since agent, leading to better performance but at the cost of accurate and timely intention and trajectory prediction will redundant computation.

This paper summarizes our line of research about the introduction of function symbols (functions) in Answer Set Programming (ASP) – a powerful language for knowledge representation and reasoning. The undecidability of reasoning on ASP with functions, implied that functions were subject to severe restrictions or disallowed at all, drastically limiting ASP applicability. We overcame most of the technical difficulties preventing this introduction, and we singled out a highly expressive class of programs with functions (FG-programs), allowing the (possibly recursive) use of function terms in the full ASP language with disjunction and negation. Reasoning on FG-programs is decidable, and they can express any computable function (causing membership in this class to be semi-decidable). We singled out also FD-programs, a subset of FG-programs which are effectively recognizable, while keeping the computability of reasoning. We implemented all results into the DLV system, thus obtaining an ASP system allowing to encode any computable function in a rich and fully declarative KRR language, ensuring termination on every FG program. Finally, we singled out the class of DFRP programs, where decidability of reasoning is guaranteed and Prolog-like functions are allowed.