arXiv subjects

Vincent Martin

Publications and source records attributed to Vincent Martin.

17 recordsLinked to original sources

arXiv2026

A Rocq Formalization of Simplicial Lagrange Finite Elements

Formalization of mathematics is a major topic, that includes in particular numerical analysis, towards proofs of scientific computing programs. The present study is about the finite element method, a popular method to numerically solve partial differential equations. In the long-term goal of proving its correctness, we focus here on the formal definition of what is a finite element. Mathematically, a finite element describes what happens in a cell of a mesh. It notably includes the geometry of the cell, the polynomial approximation space, and a finite set of linear forms that computationally characterizes the polynomials. Formally, we design a finite element as a record in the Rocq proof assistant with both values (such as the vertices of the cell) and proofs of validity (such as the dimension of the approximation space). The decisive validity proof is unisolvence, that makes the previous characterization unique. We then instantiate this record with the most popular and useful, the simplicial Lagrange finite elements for evenly distributed nodes, for any dimension and any polynomial degree, including the difficult unisolvence proof. These proofs require many results (definitions, lemmas, canonical structures) about finite families, affine spaces, multivariate polynomials, in the context of finite or infinite-dimensional spaces.

cs.LO↗

arXiv2025

A Rocq Formalization of Monomial and Graded Orders

Even if binary relations and orders are a common formalization topic, we need to formalize specific orders (namely monomial and graded) in the process of formalizing in Rocq the finite element method. This article is therefore definitions, operators, and proofs of properties about relations and orders, thus providing a comprehensive Rocq library. We especially focus on monomial orders, that are total orders compatible with the monoid operation. More than its definition and proved properties, we define several of them, among them the lexicographic and grevlex orders. For the sake of genericity, we formalize the grading of an order, a high-level operator that transforms a binary relation into another one, and we prove that grading an order preserves many of its properties, such as the monomial order property. This leads us to the definition and properties of four different graded orders, with very factorized proofs. We therefore provide a comprehensive and user-friendly library in Rocq about orders, including monomial and graded orders, that contains more than 700 lemmas.

cs.LO↗

arXiv2025

A Flexible Multi-Agent LLM-Human Framework for Fast Human Validated Tool Building

We introduce CollabToolBuilder, a flexible multiagent LLM framework with expert-in-the-loop (HITL) guidance that iteratively learns to create tools for a target goal, aligning with human intent and process, while minimizing time for task/domain adaptation effort and human feedback capture. The architecture generates and validates tools via four specialized agents (Coach, Coder, Critic, Capitalizer) using a reinforced dynamic prompt and systematic human feedback integration to reinforce each agent's role toward goals and constraints. This work is best viewed as a system-level integration and methodology combining multi-agent in-context learning, HITL controls, and reusable tool capitalization for complex iterative problems such as scientific document generation. We illustrate it with preliminary experiments (e.g., generating state-of-the-art research papers or patents given an abstract) and discuss its applicability to other iterative problem-solving.

cs.AI↗

arXiv2025

Impact of HRTF individualisation and head movements in a real/virtual localisation task

The objective of Audio Augmented Reality (AAR) applications are to seamlessly integrate virtual sound sources within a real environment. It is critical for these applications that virtual sources are localised precisely at the intended position, and that the acoustic environments are accurately matched. One effective method for spatialising sound on headphones is through Head-Related Transfer Functions (HRTFs). These characterise how the physical features of a listener modify sound waves before they reach the eardrum. This study examines the influence of using individualised HRTFs on the localisation and the perceived realism of virtual sound sources associated with a real visual object. Participants were tasked with localising virtual and real speech sources presented via headphones and through a spherical loudspeaker array, respectively. The assessment focussed on perceived realism and sources location. All sources were associated with one of thirty real visual sources (loudspeakers) arranged in a semi-anechoic room. Various sound source renderings were compared, including single loudspeaker rendering and binaural rendering with individualised or non-individualised HRTFs. Additionally, the impact of head movements was explored: ten participants completed the same task with and without the possibility to move their head. The results showed that using individual HRTFs improved perceived realism but not localisation performance in the static scenario. Surprisingly, the opposite was observed when head movements were possible and encouraged.

eess.AS↗

arXiv2025

The Extended SONICOM HRTF Dataset and Spatial Audio Metrics Toolbox

Headphone-based spatial audio uses head-related transfer functions (HRTFs) to simulate real-world acoustic environments. HRTFs are unique to everyone, due to personal morphology, shaping how sound waves interact with the body before reaching the eardrums. Here we present the extended SONICOM HRTF dataset which expands on the previous version released in 2023. The total number of measured subjects has now been increased to 300, with demographic information for a subset of the participants, providing context for the dataset's population and relevance. The dataset incorporates synthesised HRTFs for 200 of the 300 subjects, generated using Mesh2HRTF, alongside pre-processed 3D scans of the head and ears, optimised for HRTF synthesis. This rich dataset facilitates rapid and iterative optimisation of HRTF synthesis algorithms, allowing the automatic generation of large data. The optimised scans enable seamless morphological modifications, providing insights into how anatomical changes impact HRTFs, and the larger sample size enhances the effectiveness of machine learning approaches. To support analysis, we also introduce the Spatial Audio Metrics (SAM) Toolbox, a Python package designed for efficient analysis and visualisation of HRTF data, offering customisable tools for advanced research. Together, the extended dataset and toolbox offer a comprehensive resource for advancing personalised spatial audio research and development.

eess.AS↗

arXiv2024

Perceptual implications of simplifying geometrical acoustics models for Ambisonics-based binaural reverberation

Different methods can be employed to render virtual reverberation, often requiring substantial information about the room's geometry and the acoustic characteristics of the surfaces. However, fully comprehensive approaches that account for all aspects of a given environment may be computationally costly and redundant from a perceptual standpoint. For these methods, achieving a trade-off between perceptual authenticity and model's complexity becomes a relevant challenge. This study investigates this compromise through the use of geometrical acoustics to render Ambisonics-based binaural reverberation. Its precision is determined, among other factors, by its fidelity to the room's geometry and to the acoustic properties of its materials. The purpose of this study is to investigate the impact of simplifying the room geometry and the frequency resolution of absorption coefficients on the perception of reverberation within a virtual sound scene. Several decimated models based on a single room were perceptually evaluated using the a multi-stimulus comparison method. Additionally, these differences were numerically assessed through the calculation of acoustic parameters of the reverberation. According to numerical and perceptual evaluations, lowering the frequency resolution of absorption coefficients can have a significant impact on the perception of reverberation, while a less notable impact was observed when decimating the geometry of the model.

eess.AS↗

arXiv2024

Finite element method. Detailed proofs to be formalized in Coq

To obtain the highest confidence on the correction of numerical simulation programs for the resolution of Partial Differential Equations (PDEs), one has to formalize the mathematical notions and results that allow to establish the soundness of the approach. The finite element method is one of the popular tools for the numerical resolution of a wide range of PDEs. The purpose of this document is to provide the formal proof community with very detailed pen-and-paper proofs for the construction of the Lagrange finite elements of any degree on simplices in positive dimension.

cs.LO↗

arXiv2023

Neuromuscular and Metabolic Responses during Repeated Bouts of Loaded Downhill Walking

The aim of this study was to compare vastus lateralis (VL) and rectus femoris (RF) muscles for their nervous and mechanical adaptations during two bouts of downhill walking (DW) with load carriage performed two weeks apart. Moreover, we investigated cardio-metabolic and perceived exertion responses during both DW bouts. Methods Seventeen participants performed two 45-min sessions of loaded DW (30% of body mass; slope: -25 %; speed: 4.5 km$\times$h -1 ) separated by two weeks. Rating of perceived exertion (RPE), cost of walking (C w ), heart rate (HR), and EMG activity of thigh muscles were assessed during the DW. Muscle shear elastic modulus ($\mu$) of RF and VL were assessed before each exercise bout. Maximal voluntary contraction (MVC) torque was assessed before (PRE), immediately after (POST), 24 and 48 h after the two exercise bouts. Results MVC torque decreased from POST (-23.7 $\pm$ 9.2%) to 48 h (-19.2 $\pm$ 11.9%) after the first exercise (Ex1), whereas it was significantly reduced only at POST (-14.6 $\pm$ 11.0%) after the second exercise (Ex2) (p < 0.001). RPE (Ex1: 12.3 $\pm$ 1.9; Ex2: 10.8 $\pm$ 2.0), HR (Ex1: 156 $\pm$ 23 bpm; Ex2: 145 $\pm$ 25 bpm), C w (Ex1: 4.5 $\pm$ 0.9 J$\times$m -1 $\times$kg -1 ; Ex2: 4.1 $\pm$ 0.7 J$\times$m -1 $\times$kg -1 ) and RF EMG activity (Ex1: 0.071 $\pm$ 0.028 mV; Ex2: 0.041 $\pm$ 0.014 mV) were significantly decreased during Ex2 compared to Ex1 (p < 0.01). RF $\mu$ was significantly greater in Ex2 (0.44 $\pm$ 0.18) compared to Ex1 (0.56 $\pm$ 0.27; p < 0.001). Conclusions The RF muscle displayed specific mechanical and nervous adaptations to repeated DW bouts as compared to VL. Moreover, the muscle adaptations conferred by the first bout of DW could have induced greater exercise efficiency, inducing lesser perceived exertion and cardio-metabolic demand when the same exercise was repeated two weeks later.

q-bio.TO↗

arXiv2023

Stabilization of approximate GHZ state with quasi-local couplings

We propose a reservoir design, composed of fixed dissipation operators acting each on few local subsystems, to stabilize an approximate GHZ state on n qubits. The main idea is to work out how a previously proposed sequence of two stabilization steps can be applied instead in appropriate (probabilistic) superposition. We examine alternatives to synchronize the superposition using local couplings only, thanks to a chain of "clock" ancillas or to additional levels on the data subsystems. The practical value of these alternatives depends on experimental constraints. They all feature a design tradeoff between approximate stabilization fidelity and protection against perturbations. These proposals illustrate how simple autonomous automata can be implemented in quantum reservoir engineering to replace sequential state preparation procedures. Encoding automaton actions via additional data levels only, appears particularly efficient in this context. Our analysis method, reducing the Lindblad master equation to a Markov chain on virtual output signals, may be of independent interest.

quant-ph↗

arXiv2023

Complex QA and language models hybrid architectures, Survey

This paper reviews the state-of-the-art of large language models (LLM) architectures and strategies for "complex" question-answering with a focus on hybrid architectures. LLM based chatbot services have allowed anyone to grasp the potential of LLM to solve many common problems, but soon discovered their limitations for complex questions. Addressing more specific, complex questions (e.g., "What is the best mix of power-generation methods to reduce climate change ?") often requires specialized architectures, domain knowledge, new skills, decomposition and multi-step resolution, deep reasoning, sensitive data protection, explainability, and human-in-the-loop processes. Therefore, we review: (1) necessary skills and tasks for handling complex questions and common LLM limits to overcome; (2) dataset, cost functions and evaluation metrics for measuring and improving (e.g. accuracy, explainability, fairness, robustness, groundedness, faithfulness, toxicity...); (3) family of solutions to overcome LLM limitations by (a) training and reinforcement (b) hybridization, (c) prompting, (d) agentic-architectures (agents, tools) and extended reasoning.

cs.CL↗

arXiv2022

Lebesgue Induction and Tonelli's Theorem in Coq

Lebesgue integration is a well-known mathematical tool, used for instance in probability theory, real analysis, and numerical mathematics. Thus its formalization in a proof assistant is to be designed to fit different goals and projects. Once Lebesgue integral is formally defined and the first lemmas are proved, the question of the convenience of the formalization naturally arises. To check it, a useful extension is the Tonelli theorem, stating that the (double) integral of a nonnegative measurable function of two variables can be computed by iterated integrals, and allowing to switch the order of integration. Therefore, we need to define and prove results on product spaces, hoping that they can easily derive from the existing ones on a single space. This article describes the formal definition and proof in Coq of product $\sigma$-algebras, product measures and their uniqueness, the construction of iterated integrals, up to the Tonelli theorem. We also advertise the \emph{Lebesgue induction principle} provided by an inductive type for {\nonnegative} measurable functions.

cs.LO↗

arXiv2021

A Coq Formalization of Lebesgue Integration of Nonnegative Functions

Integration, just as much as differentiation, is a fundamental calculus tool that is widely used in many scientific domains. Formalizing the mathematical concept of integration and the associated results in a formal proof assistant helps in providing the highest confidence on the correctness of numerical programs involving the use of integration, directly or indirectly. By its capability to extend the (Riemann) integral to a wide class of irregular functions, and to functions defined on more general spaces than the real line, the Lebesgue integral is perfectly suited for use in mathematical fields such as probability theory, numerical mathematics, and real analysis. In this article, we present the Coq formalization of $\sigma$-algebras, measures, simple functions, and integration of nonnegative measurable functions, up to the full formal proofs of the Beppo Levi (monotone convergence) theorem and Fatou's lemma. More than a plain formalization of the known literature, we present several design choices made to balance the harmony between mathematical readability and usability of Coq theorems. These results are a first milestone toward the formalization of $L^p$~spaces such as Banach spaces.

cs.LO↗

arXiv2021

Lebesgue integration. Detailed proofs to be formalized in Coq

To obtain the highest confidence on the correction of numerical simulation programs implementing the finite element method, one has to formalize the mathematical notions and results that allow to establish the soundness of the method. Sobolev spaces are the mathematical framework in which most weak formulations of partial derivative equations are stated, and where solutions are sought. These functional spaces are built on integration and measure theory. Hence, this chapter in functional analysis is a mandatory theoretical cornerstone for the definition of the finite element method. The purpose of this document is to provide the formal proof community with very detailed pen-and-paper proofs of the main results from integration and measure theory.

cs.LO↗

arXiv2020

Scaling up reservoir engineering for error-correcting codes

Error-correcting codes are usually envisioned to counter errors by operating unitary corrections depending on the projective measurement results of some syndrome observables. We here propose a way to use them in a more integrated way, where the error correction is applied continuously and autonomously by an engineered environment. We focus on a proposal for the repetition code that counters bit-flip errors, and how to scale up the network encoding a logical quantum bit, towards stronger information protection. The challenge has been to devise a network architecture which allows to autonomously correct higher-order errors, while remaining realistic towards experimental realization by avoiding all-to-all or all-to-one coupling.

quant-ph↗

arXiv2019

Effect of MTU length on child-adult difference in neuromuscular fatigue

Purpose The purpose of this study was to compare the development and etiology of neuromuscular fatigue of the knee extensor muscles (KE) at different muscle-tendon unit (MTU) lengths during repeated maximal voluntary isometric contractions (MVIC) between boys and men.Methods Twenty-two pre-pubertal boys (9-11 years) and 22 men (18-30 years) performed three KE fatigue protocols at short (SHORT), optimal (OPT) and long (LONG) MTU lengths, consisting of repeating 5-s MVIC interspersed with 5-s passive recovery periods until torque reached 60% of the initial MVIC torque. The etiology of neuromuscular fatigue was identified using non-invasive methods such as surface electromyography, near-infrared spectroscopy, magnetic nerve stimulation and twitch interpolation technique.Results The number of repetitions was significantly lower in men at OPT (14.8$\pm$3.2) and LONG (15.8$\pm$5.8) than boys (39.7$\pm$18.4 and 29.5 $\pm$10.2, respectively; p<0.001), while no difference was found at SHORT between both age groups (boys: 33.7$\pm$15.4, men: 40.9$\pm$14.2). At OPT and LONG boys showed a lower reduction in the single potentiated twitch (Qtwpot) and a greater decrease in the voluntary activation level (VA) than men. At SHORT, both populations displayed a moderate Qtwpot decrement and a significant VA reduction (p<0.001). The differences in maximal torque between boys and men were almost twice greater at OPT (223.9 N.m) than at SHORT (123.3 N.m) and LONG (136.5 N.m).Conclusion The differences in neuromuscular fatigue between children and adults are dependent on MTU length. Differences in maximal torque could underpin differences in neuromuscular fatigue between children and adults at OPT and SHORT. However, at LONG these differences do not seem to be explained by differences in maximal torque. The origins of this specific effect of MTU length remain to be determined.

q-bio.TO↗

arXiv2016

The Lax-Milgram Theorem. A detailed proof to be formalized in Coq

To obtain the highest confidence on the correction of numerical simulation programs implementing the finite element method, one has to formalize the mathematical notions and results that allow to establish the soundness of the method. The Lax-Milgram theorem may be seen as one of those theoretical cornerstones: under some completeness and coercivity assumptions, it states existence and uniqueness of the solution to the weak formulation of some boundary value problems. The purpose of this document is to provide the formal proof community with a very detailed pen-and-paper proof of the Lax-Milgram theorem.

cs.LO↗

arXiv2016

First-Order Indicators for the Estimation of Discrete Fractures in Porous Media

Faults and geological barriers can drastically affect the flow patterns in porous media. Such fractures can be modeled as interfaces that interact with the surrounding matrix. We propose a new technique for the estimation of the location and hydrogeological properties of a small number of large fractures in a porous medium from given distributed pressure or flow data. At each iteration, the algorithm builds a short list of candidates by comparing fracture indicators. These indicators quantify at the first order the decrease of a data misfit function; they are cheap to compute. Then, the best candidate is picked up by minimization of the objective function for each candidate. Optimally driven by the fit to the data, the approach has the great advantage of not requiring remeshing, nor shape derivation. The stability of the algorithm is shown on a series of numerical examples representative of typical situations.

math.NA↗