-
GISR: Geometric Initialization and Silhouette-based Refinement for Single-View Robot Pose and Configuration Estimation
Authors:
Ivan Bilić,
Filip Marić,
Fabio Bonsignorio,
Ivan Petrović
Abstract:
For autonomous robotics applications, it is crucial that robots are able to accurately measure their potential state and perceive their environment, including other agents within it (e.g., cobots interacting with humans). The redundancy of these measurements is important, as it allows for planning and execution of recovery protocols in the event of sensor failure or external disturbances. Visual e…
▽ More
For autonomous robotics applications, it is crucial that robots are able to accurately measure their potential state and perceive their environment, including other agents within it (e.g., cobots interacting with humans). The redundancy of these measurements is important, as it allows for planning and execution of recovery protocols in the event of sensor failure or external disturbances. Visual estimation can provide this redundancy through the use of low-cost sensors and server as a standalone source of proprioception when no encoder-based sensing is available. Therefore, we estimate the configuration of the robot jointly with its pose, which provides a complete spatial understanding of the observed robot. We present GISR - a method for deep configuration and robot-to-camera pose estimation that prioritizes real-time execution. GISR is comprised of two modules: (i) a geometric initialization module, efficiently computing an approximate robot pose and configuration, and (ii) an iterative silhouette-based refinement module that refines the initial solution in only a few iterations. We evaluate our method on a publicly available dataset and show that GISR performs competitively with existing state-of-the-art approaches, while being significantly faster compared to existing methods of the same class. Our code is available at https://github.com/iwhitey/GISR-robot.
△ Less
Submitted 8 May, 2024;
originally announced May 2024.
-
Towards Automated Readable Proofs of Ruler and Compass Constructions
Authors:
Vesna Marinković,
Tijana Šukilović,
Filip Marić
Abstract:
Although there are several systems that successfully generate construction steps for ruler and compass construction problems, none of them provides readable synthetic correctness proofs for generated constructions. In the present work, we demonstrate how our triangle construction solver ArgoTriCS can cooperate with automated theorem provers for first order logic and coherent logic so that it gener…
▽ More
Although there are several systems that successfully generate construction steps for ruler and compass construction problems, none of them provides readable synthetic correctness proofs for generated constructions. In the present work, we demonstrate how our triangle construction solver ArgoTriCS can cooperate with automated theorem provers for first order logic and coherent logic so that it generates construction correctness proofs, that are both human-readable and formal (can be checked by interactive theorem provers such as Coq or Isabelle/HOL). These proofs currently rely on many high-level lemmas and our goal is to have them all formally shown from the basic axioms of geometry.
△ Less
Submitted 22 January, 2024;
originally announced January 2024.
-
Euclidean Equivariant Models for Generative Graphical Inverse Kinematics
Authors:
Oliver Limoyo,
Filip Marić,
Matthew Giamou,
Petra Alexson,
Ivan Petrović,
Jonathan Kelly
Abstract:
Quickly and reliably finding accurate inverse kinematics (IK) solutions remains a challenging problem for robotic manipulation. Existing numerical solvers typically produce a single solution only and rely on local search techniques to minimize a highly nonconvex objective function. Recently, learning-based approaches that approximate the entire feasible set of solutions have shown promise as a mea…
▽ More
Quickly and reliably finding accurate inverse kinematics (IK) solutions remains a challenging problem for robotic manipulation. Existing numerical solvers typically produce a single solution only and rely on local search techniques to minimize a highly nonconvex objective function. Recently, learning-based approaches that approximate the entire feasible set of solutions have shown promise as a means to generate multiple fast and accurate IK results in parallel. However, existing learning-based techniques have a significant drawback: each robot of interest requires a specialized model that must be trained from scratch. To address this shortcoming, we investigate a novel distance-geometric robot representation coupled with a graph structure that allows us to leverage the flexibility of graph neural networks (GNNs). We use this approach to train a generative graphical inverse kinematics solver (GGIK) that is able to produce a large number of diverse solutions in parallel while also generalizing well -- a single learned model can be used to produce IK solutions for a variety of different robots. The graphical formulation elegantly exposes the symmetry and Euclidean equivariance of the IK problem that stems from the spatial nature of robot manipulators. We exploit this symmetry by encoding it into the architecture of our learned model, yielding a flexible solver that is able to produce sets of IK solutions for multiple robots.
△ Less
Submitted 4 July, 2023;
originally announced July 2023.
-
CIDGIKc: Distance-Geometric Inverse Kinematics for Continuum Robots
Authors:
Hanna Jiamei Zhang,
Matthew Giamou,
Filip Marić,
Jonathan Kelly,
Jessica Burgner-Kahrs
Abstract:
The small size, high dexterity, and intrinsic compliance of continuum robots (CRs) make them well suited for constrained environments. Solving the inverse kinematics (IK), that is finding robot joint configurations that satisfy desired position or pose queries, is a fundamental challenge in motion planning, control, and calibration for any robot structure. For CRs, the need to avoid obstacles in t…
▽ More
The small size, high dexterity, and intrinsic compliance of continuum robots (CRs) make them well suited for constrained environments. Solving the inverse kinematics (IK), that is finding robot joint configurations that satisfy desired position or pose queries, is a fundamental challenge in motion planning, control, and calibration for any robot structure. For CRs, the need to avoid obstacles in tightly confined workspaces greatly complicates the search for feasible IK solutions. Without an accurate initialization or multiple re-starts, existing algorithms often fail to find a solution. We present CIDGIKc (Convex Iteration for Distance-Geometric Inverse Kinematics for Continuum Robots), an algorithm that solves these nonconvex feasibility problems with a sequence of semidefinite programs whose objectives are designed to encourage low-rank minimizers. CIDGIKc is enabled by a novel distance-geometric parameterization of constant curvature segment geometry for CRs with extensible segments. The resulting IK formulation involves only quadratic expressions and can efficiently incorporate a large number of collision avoidance constraints. Our experimental results demonstrate >98% solve success rates within complex, highly cluttered environments which existing algorithms cannot account for.
△ Less
Submitted 23 June, 2023;
originally announced June 2023.
-
A Distance-Geometric Method for Recovering Robot Joint Angles From an RGB Image
Authors:
Ivan Bilić,
Filip Marić,
Ivan Marković,
Ivan Petrović
Abstract:
Autonomous manipulation systems operating in domains where human intervention is difficult or impossible (e.g., underwater, extraterrestrial or hazardous environments) require a high degree of robustness to sensing and communication failures. Crucially, motion planning and control algorithms require a stream of accurate joint angle data provided by joint encoders, the failure of which may result i…
▽ More
Autonomous manipulation systems operating in domains where human intervention is difficult or impossible (e.g., underwater, extraterrestrial or hazardous environments) require a high degree of robustness to sensing and communication failures. Crucially, motion planning and control algorithms require a stream of accurate joint angle data provided by joint encoders, the failure of which may result in an unrecoverable loss of functionality. In this paper, we present a novel method for retrieving the joint angles of a robot manipulator using only a single RGB image of its current configuration, opening up an avenue for recovering system functionality when conventional proprioceptive sensing is unavailable. Our approach, based on a distance-geometric representation of the configuration space, exploits the knowledge of a robot's kinematic model with the goal of training a shallow neural network that performs a 2D-to-3D regression of distances associated with detected structural keypoints. It is shown that the resulting Euclidean distance matrix uniquely corresponds to the observed configuration, where joint angles can be recovered via multidimensional scaling and a simple inverse kinematics procedure. We evaluate the performance of our approach on real RGB images of a Franka Emika Panda manipulator, showing that the proposed method is efficient and exhibits solid generalization ability. Furthermore, we show that our method can be easily combined with a dense refinement technique to obtain superior results.
△ Less
Submitted 27 April, 2023; v1 submitted 5 January, 2023;
originally announced January 2023.
-
Generative Graphical Inverse Kinematics
Authors:
Oliver Limoyo,
Filip Marić,
Matthew Giamou,
Petra Alexson,
Ivan Petrović,
Jonathan Kelly
Abstract:
Quickly and reliably finding accurate inverse kinematics (IK) solutions remains a challenging problem for many robot manipulators. Existing numerical solvers are broadly applicable but typically only produce a single solution and rely on local search techniques to minimize nonconvex objective functions. More recent learning-based approaches that approximate the entire feasible set of solutions hav…
▽ More
Quickly and reliably finding accurate inverse kinematics (IK) solutions remains a challenging problem for many robot manipulators. Existing numerical solvers are broadly applicable but typically only produce a single solution and rely on local search techniques to minimize nonconvex objective functions. More recent learning-based approaches that approximate the entire feasible set of solutions have shown promise as a means to generate multiple fast and accurate IK results in parallel. However, existing learning-based techniques have a significant drawback: each robot of interest requires a specialized model that must be trained from scratch. To address this key shortcoming, we propose a novel distance-geometric robot representation coupled with a graph structure that allows us to leverage the sample efficiency of Euclidean equivariant functions and the generalizability of graph neural networks (GNNs). Our approach is generative graphical inverse kinematics (GGIK), the first learned IK solver able to accurately and efficiently produce a large number of diverse solutions in parallel while also displaying the ability to generalize -- a single learned model can be used to produce IK solutions for a variety of different robots. When compared to several other learned IK methods, GGIK provides more accurate solutions with the same amount of data. GGIK can generalize reasonably well to robot manipulators unseen during training. Additionally, GGIK can learn a constrained distribution that encodes joint limits and scales efficiently to larger robots and a high number of sampled solutions. Finally, GGIK can be used to complement local IK solvers by providing reliable initializations for a local optimization process.
△ Less
Submitted 24 March, 2024; v1 submitted 19 September, 2022;
originally announced September 2022.
-
On Automating Triangle Constructions in Absolute and Hyperbolic Geometry
Authors:
Vesna Marinković,
Tijana Šukilović,
Filip Marić
Abstract:
We describe first steps towards a system for automated triangle constructions in absolute and hyperbolic geometry. We discuss key differences between constructions in Euclidean, absolute and hyperbolic geometry, compile a list of primitive constructions and lemmas used for constructions in absolute and hyperbolic geometry, build an automated system for solving construction problems and test it on…
▽ More
We describe first steps towards a system for automated triangle constructions in absolute and hyperbolic geometry. We discuss key differences between constructions in Euclidean, absolute and hyperbolic geometry, compile a list of primitive constructions and lemmas used for constructions in absolute and hyperbolic geometry, build an automated system for solving construction problems and test it on a corpus of triangle-construction problems. We also provide an online compendium containing construction descriptions and illustrations.
△ Less
Submitted 3 January, 2022;
originally announced January 2022.
-
A proof system for graph (non)-isomorphism verification
Authors:
Milan Banković,
Ivan Drecun,
Filip Marić
Abstract:
In order to apply canonical labelling of graphs and isomorphism checking in interactive theorem provers, these checking algorithms must either be mechanically verified or their results must be verifiable by independent checkers. We analyze a state-of-the-art algorithm for canonical labelling of graphs (described by McKay and Piperno) and formulate it in terms of a formal proof system. We provide a…
▽ More
In order to apply canonical labelling of graphs and isomorphism checking in interactive theorem provers, these checking algorithms must either be mechanically verified or their results must be verifiable by independent checkers. We analyze a state-of-the-art algorithm for canonical labelling of graphs (described by McKay and Piperno) and formulate it in terms of a formal proof system. We provide an implementation that can export a proof that the obtained graph is the canonical form of a given graph. Such proofs are then verified by our independent checker and can be used to confirm that two given graphs are not isomorphic.
△ Less
Submitted 31 January, 2023; v1 submitted 28 December, 2021;
originally announced December 2021.
-
Convex Iteration for Distance-Geometric Inverse Kinematics
Authors:
Matthew Giamou,
Filip Marić,
David M. Rosen,
Valentin Peretroukhin,
Nicholas Roy,
Ivan Petrović,
Jonathan Kelly
Abstract:
Inverse kinematics (IK) is the problem of finding robot joint configurations that satisfy constraints on the position or pose of one or more end-effectors. For robots with redundant degrees of freedom, there is often an infinite, nonconvex set of solutions. The IK problem is further complicated when collision avoidance constraints are imposed by obstacles in the workspace. In general, closed-form…
▽ More
Inverse kinematics (IK) is the problem of finding robot joint configurations that satisfy constraints on the position or pose of one or more end-effectors. For robots with redundant degrees of freedom, there is often an infinite, nonconvex set of solutions. The IK problem is further complicated when collision avoidance constraints are imposed by obstacles in the workspace. In general, closed-form expressions yielding feasible configurations do not exist, motivating the use of numerical solution methods. However, these approaches rely on local optimization of nonconvex problems, often requiring an accurate initialization or numerous re-initializations to converge to a valid solution. In this work, we first formulate inverse kinematics with complex workspace constraints as a convex feasibility problem whose low-rank feasible points provide exact IK solutions. We then present \texttt{CIDGIK} (Convex Iteration for Distance-Geometric Inverse Kinematics), an algorithm that solves this feasibility problem with a sequence of semidefinite programs whose objectives are designed to encourage low-rank minimizers. Our problem formulation elegantly unifies the configuration space and workspace constraints of a robot: intrinsic robot geometry and obstacle avoidance are both expressed as simple linear matrix equations and inequalities. Our experimental results for a variety of popular manipulator models demonstrate faster and more accurate convergence than a conventional nonlinear optimization-based approach, especially in environments with many obstacles.
△ Less
Submitted 6 July, 2022; v1 submitted 7 September, 2021;
originally announced September 2021.
-
Riemannian Optimization for Distance-Geometric Inverse Kinematics
Authors:
Filip Marić,
Matthew Giamou,
Adam W. Hall,
Soroush Khoubyarian,
Ivan Petrović,
Jonathan Kelly
Abstract:
Solving the inverse kinematics problem is a fundamental challenge in motion planning, control, and calibration for articulated robots. Kinematic models for these robots are typically parametrized by joint angles, generating a complicated map** between the robot configuration and the end-effector pose. Alternatively, the kinematic model and task constraints can be represented using invariant dist…
▽ More
Solving the inverse kinematics problem is a fundamental challenge in motion planning, control, and calibration for articulated robots. Kinematic models for these robots are typically parametrized by joint angles, generating a complicated map** between the robot configuration and the end-effector pose. Alternatively, the kinematic model and task constraints can be represented using invariant distances between points attached to the robot. In this paper, we formalize the equivalence of distance-based inverse kinematics and the distance geometry problem for a large class of articulated robots and task constraints. Unlike previous approaches, we use the connection between distance geometry and low-rank matrix completion to find inverse kinematics solutions by completing a partial Euclidean distance matrix through local optimization. Furthermore, we parametrize the space of Euclidean distance matrices with the Riemannian manifold of fixed-rank Gram matrices, allowing us to leverage a variety of mature Riemannian optimization methods. Finally, we show that bound smoothing can be used to generate informed initializations without significant computational overhead, improving convergence. We demonstrate that our inverse kinematics solver achieves higher success rates than traditional techniques, and substantially outperforms them on problems that involve many workspace constraints.
△ Less
Submitted 10 December, 2023; v1 submitted 31 August, 2021;
originally announced August 2021.
-
A Riemannian Metric for Geometry-Aware Singularity Avoidance by Articulated Robots
Authors:
Filip Marić,
Luka Petrović,
Marko Guberina,
Jonathan Kelly,
Ivan Petrović
Abstract:
Articulated robots such as manipulators increasingly must operate in uncertain and dynamic environments where interaction (with human coworkers, for example) is necessary. In these situations, the capacity to quickly adapt to unexpected changes in operational space constraints is essential. At certain points in a manipulator's configuration space, termed singularities, the robot loses one or more…
▽ More
Articulated robots such as manipulators increasingly must operate in uncertain and dynamic environments where interaction (with human coworkers, for example) is necessary. In these situations, the capacity to quickly adapt to unexpected changes in operational space constraints is essential. At certain points in a manipulator's configuration space, termed singularities, the robot loses one or more degrees of freedom (DoF) and is unable to move in specific operational space directions. The inability to move in arbitrary directions in operational space compromises adaptivity and, potentially, safety. We introduce a geometry-aware singularity index, defined using a Riemannian metric on the manifold of symmetric positive definite matrices, to provide a measure of proximity to singular configurations. We demonstrate that our index avoids some of the failure modes and difficulties inherent to other common indices. Further, we show that this index can be differentiated easily, making it compatible with local optimization approaches used for operational space control. Our experimental results establish that, for reaching and path following tasks, optimization based on our index outperforms a common manipulability maximization technique and ensures singularity-robust motions.
△ Less
Submitted 12 July, 2022; v1 submitted 9 March, 2021;
originally announced March 2021.
-
Inverse Kinematics as Low-Rank Euclidean Distance Matrix Completion
Authors:
Filip Marić,
Matthew Giamou,
Ivan Petrović,
Jonathan Kelly
Abstract:
The majority of inverse kinematics (IK) algorithms search for solutions in a configuration space defined by joint angles. However, the kinematics of many robots can also be described in terms of distances between rigidly-attached points, which collectively form a Euclidean distance matrix. This alternative geometric description of the kinematics reveals an elegant equivalence between IK and the pr…
▽ More
The majority of inverse kinematics (IK) algorithms search for solutions in a configuration space defined by joint angles. However, the kinematics of many robots can also be described in terms of distances between rigidly-attached points, which collectively form a Euclidean distance matrix. This alternative geometric description of the kinematics reveals an elegant equivalence between IK and the problem of low-rank matrix completion. We use this connection to implement a novel Riemannian optimization-based solution to IK for various articulated robots with symmetric joint angle constraints.
△ Less
Submitted 5 July, 2022; v1 submitted 9 November, 2020;
originally announced November 2020.
-
Formalizing IMO Problems and Solutions in Isabelle/HOL
Authors:
Filip Marić,
Sana Stojanović-{\Dj}urđević
Abstract:
The International Mathematical Olympiad (IMO) is perhaps the most celebrated mental competition in the world and as such is among the greatest grand challenges for Artificial Intelligence (AI). The IMO Grand Challenge, recently formulated, requires to build an AI that can win a gold medal in the competition. We present some initial steps that could help to tackle this goal by creating a public rep…
▽ More
The International Mathematical Olympiad (IMO) is perhaps the most celebrated mental competition in the world and as such is among the greatest grand challenges for Artificial Intelligence (AI). The IMO Grand Challenge, recently formulated, requires to build an AI that can win a gold medal in the competition. We present some initial steps that could help to tackle this goal by creating a public repository of mechanically checked solutions of IMO Problems in the interactive theorem prover Isabelle/HOL. This repository is actively maintained by students of the Faculty of Mathematics, University of Belgrade, Serbia within the course "Introduction to Interactive Theorem Proving".
△ Less
Submitted 29 October, 2020;
originally announced October 2020.
-
Heteroscedastic Uncertainty for Robust Generative Latent Dynamics
Authors:
Oliver Limoyo,
Bryan Chan,
Filip Marić,
Brandon Wagstaff,
Rupam Mahmood,
Jonathan Kelly
Abstract:
Learning or identifying dynamics from a sequence of high-dimensional observations is a difficult challenge in many domains, including reinforcement learning and control. The problem has recently been studied from a generative perspective through latent dynamics: high-dimensional observations are embedded into a lower-dimensional space in which the dynamics can be learned. Despite some successes, l…
▽ More
Learning or identifying dynamics from a sequence of high-dimensional observations is a difficult challenge in many domains, including reinforcement learning and control. The problem has recently been studied from a generative perspective through latent dynamics: high-dimensional observations are embedded into a lower-dimensional space in which the dynamics can be learned. Despite some successes, latent dynamics models have not yet been applied to real-world robotic systems where learned representations must be robust to a variety of perceptual confounds and noise sources not seen during training. In this paper, we present a method to jointly learn a latent state representation and the associated dynamics that is amenable for long-term planning and closed-loop control under perceptually difficult conditions. As our main contribution, we describe how our representation is able to capture a notion of heteroscedastic or input-specific uncertainty at test time by detecting novel or out-of-distribution (OOD) inputs. We present results from prediction and control experiments on two image-based tasks: a simulated pendulum balancing task and a real-world robotic manipulator reaching task. We demonstrate that our model produces significantly more accurate predictions and exhibits improved control performance, compared to a model that assumes homoscedastic uncertainty only, in the presence of varying degrees of input degradation.
△ Less
Submitted 11 July, 2022; v1 submitted 18 August, 2020;
originally announced August 2020.
-
Fighting Failures with FIRE: Failure Identification to Reduce Expert Burden in Intervention-Based Learning
Authors:
Trevor Ablett,
Filip Marić,
Jonathan Kelly
Abstract:
Supervised imitation learning, also known as behavioral cloning, suffers from distribution drift leading to failures during policy execution. One approach to mitigate this issue is to allow an expert to correct the agent's actions during task execution, based on the expert's determination that the agent has reached a `point of no return.' The agent's policy is then retrained using this new correct…
▽ More
Supervised imitation learning, also known as behavioral cloning, suffers from distribution drift leading to failures during policy execution. One approach to mitigate this issue is to allow an expert to correct the agent's actions during task execution, based on the expert's determination that the agent has reached a `point of no return.' The agent's policy is then retrained using this new corrective data. This approach alone can enable high-performance agents to be learned, but at a substantial cost: the expert must vigilantly observe execution until the policy reaches a specified level of success, and even at that point, there is no guarantee that the policy will always succeed. To address these limitations, we present FIRE (Failure Identification to Reduce Expert Burden in intervention-based learning), a system that can predict when a running policy will fail, halt its execution, and request a correction from the expert. Unlike existing approaches that learn only from expert data, our approach learns from both expert and non-expert data, akin to adversarial learning. We demonstrate experimentally for a series of challenging manipulation tasks that our method is able to recognize state-action pairs that lead to failures. This permits seamless integration into an intervention-based learning system, where we show an order-of-magnitude gain in sample efficiency compared with a state-of-the-art inverse reinforcement learning method and dramatically improved performance over an equivalent amount of data learned with behavioral cloning.
△ Less
Submitted 8 December, 2023; v1 submitted 1 July, 2020;
originally announced July 2020.
-
Inverse Kinematics for Serial Kinematic Chains via Sum of Squares Optimization
Authors:
Filip Maric,
Matthew Giamou,
Soroush Khoubyarian,
Ivan Petrovic,
Jonathan Kelly
Abstract:
Inverse kinematics is a fundamental problem for articulated robots: fast and accurate algorithms are needed for translating task-related workspace constraints and goals into feasible joint configurations. In general, inverse kinematics for serial kinematic chains is a difficult nonlinear problem, for which closed form solutions cannot be easily obtained. Therefore, computationally efficient numeri…
▽ More
Inverse kinematics is a fundamental problem for articulated robots: fast and accurate algorithms are needed for translating task-related workspace constraints and goals into feasible joint configurations. In general, inverse kinematics for serial kinematic chains is a difficult nonlinear problem, for which closed form solutions cannot be easily obtained. Therefore, computationally efficient numerical methods that can be adapted to a general class of manipulators are of great importance. % to motion planning and workspace generation tasks. In this paper, we use convex optimization techniques to solve the inverse kinematics problem with joint limit constraints for highly redundant serial kinematic chains with spherical joints in two and three dimensions. This is accomplished through a novel formulation of inverse kinematics as a nearest point problem, and with a fast sum of squares solver that exploits the sparsity of kinematic constraints for serial manipulators. Our method has the advantages of post-hoc certification of global optimality and a runtime that scales polynomialy with the number of degrees of freedom. Additionally, we prove that our convex relaxation leads to a globally optimal solution when certain conditions are met, and demonstrate empirically that these conditions are common and represent many practical instances. Finally, we provide an open source implementation of our algorithm.
△ Less
Submitted 29 October, 2020; v1 submitted 20 September, 2019;
originally announced September 2019.
-
Fast Manipulability Maximization Using Continuous-Time Trajectory Optimization
Authors:
Filip Marić,
Oliver Limoyo,
Luka Petrović,
Trevor Ablett,
Ivan Petrović,
Jonathan Kelly
Abstract:
A significant challenge in manipulation motion planning is to ensure agility in the face of unpredictable changes during task execution. This requires the identification and possible modification of suitable joint-space trajectories, since the joint velocities required to achieve a specific endeffector motion vary with manipulator configuration. For a given manipulator configuration, the joint spa…
▽ More
A significant challenge in manipulation motion planning is to ensure agility in the face of unpredictable changes during task execution. This requires the identification and possible modification of suitable joint-space trajectories, since the joint velocities required to achieve a specific endeffector motion vary with manipulator configuration. For a given manipulator configuration, the joint space-to-task space velocity map** is characterized by a quantity known as the manipulability index. In contrast to previous control-based approaches, we examine the maximization of manipulability during planning as a way of achieving adaptable and safe joint space-to-task space motion map**s in various scenarios. By representing the manipulator trajectory as a continuous-time Gaussian process (GP), we are able to leverage recent advances in trajectory optimization to maximize the manipulability index during trajectory generation. Moreover, the sparsity of our chosen representation reduces the typically large computational cost associated with maximizing manipulability when additional constraints exist. Results from simulation studies and experiments with a real manipulator demonstrate increases in manipulability, while maintaining smooth trajectories with more dexterous (and therefore more agile) arm configurations.
△ Less
Submitted 1 May, 2020; v1 submitted 8 August, 2019;
originally announced August 2019.
-
Sparse Bounded Degree Sum of Squares Optimization for Certifiably Globally Optimal Rotation Averaging
Authors:
Matthew Giamou,
Filip Maric,
Valentin Peretroukhin,
Jonathan Kelly
Abstract:
Estimating unknown rotations from noisy measurements is an important step in SfM and other 3D vision tasks. Typically, local optimization methods susceptible to returning suboptimal local minima are used to solve the rotation averaging problem. A new wave of approaches that leverage convex relaxations have provided the first formal guarantees of global optimality for state estimation techniques in…
▽ More
Estimating unknown rotations from noisy measurements is an important step in SfM and other 3D vision tasks. Typically, local optimization methods susceptible to returning suboptimal local minima are used to solve the rotation averaging problem. A new wave of approaches that leverage convex relaxations have provided the first formal guarantees of global optimality for state estimation techniques involving SO(3). However, most of these guarantees are only applicable when the measurement error introduced by noise is within a certain bound that depends on the problem instance's structure. In this paper, we cast rotation averaging as a polynomial optimization problem over unit quaternions to produce the first rotation averaging method that is formally guaranteed to provide a certifiably globally optimal solution for \textit{any} problem instance. This is achieved by formulating and solving a sparse convex sum of squares (SOS) relaxation of the problem. We provide an open source implementation of our algorithm and experiments, demonstrating the benefits of our globally optimal approach.
△ Less
Submitted 13 June, 2019; v1 submitted 2 April, 2019;
originally announced April 2019.
-
Fully Automatic, Verified Classification of all Frankl-Complete (FC(6)) Set Families
Authors:
Filip Marić,
Bojan Vučković,
Miodrag Živković
Abstract:
The Frankl's conjecture, formulated in 1979. and still open, states that in every family of sets closed for unions there is an element contained in at least half of the sets. A family Fc is called Frankl-complete (or FC-family) if in every union-closed family F containing Fc, one of the elements of union Fc occurs in at least half of the elements of F (so F satisfies the Frankl's condition). FC-fa…
▽ More
The Frankl's conjecture, formulated in 1979. and still open, states that in every family of sets closed for unions there is an element contained in at least half of the sets. A family Fc is called Frankl-complete (or FC-family) if in every union-closed family F containing Fc, one of the elements of union Fc occurs in at least half of the elements of F (so F satisfies the Frankl's condition). FC-families play an important role in attacking the Frankl's conjecture, since they enable significant search space pruning. We extend previous work by giving a total characterization of all FC-families over a 6-element universe, by defining and enumerating all minimal FC and maximal nonFC-families. We use a fully automated, computer assisted approach, formally verified within the proof-assistant Isabelle/HOL.
△ Less
Submitted 23 February, 2019;
originally announced February 2019.
-
Manipulability Maximization Using Continuous-Time Gaussian Processes
Authors:
Filip Marić,
Oliver Limoyo,
Luka Petrović,
Ivan Petrović,
Jonathan Kelly
Abstract:
A significant challenge in motion planning is to avoid being in or near \emph{singular configurations} (\textit{singularities}), that is, joint configurations that result in the loss of the ability to move in certain directions in task space. A robotic system's capacity for motion is reduced even in regions that are in close proximity to (i.e., neighbouring) a singularity. In this work we examine…
▽ More
A significant challenge in motion planning is to avoid being in or near \emph{singular configurations} (\textit{singularities}), that is, joint configurations that result in the loss of the ability to move in certain directions in task space. A robotic system's capacity for motion is reduced even in regions that are in close proximity to (i.e., neighbouring) a singularity. In this work we examine singularity avoidance in a motion planning context, finding trajectories which minimize proximity to singular regions, subject to constraints. We define a manipulability-based likelihood associated with singularity avoidance over a continuous trajectory representation, which we then maximize using a \textit{maximum a posteriori} (MAP) estimator. Viewing the MAP problem as inference on a factor graph, we use gradient information from interpolated states to maximize the trajectory's overall manipulability. Both qualitative and quantitative analyses of experimental data show increases in manipulability that result in smooth trajectories with visibly more dexterous arm configurations.
△ Less
Submitted 11 September, 2018; v1 submitted 26 March, 2018;
originally announced March 2018.
-
Self-Calibration of Mobile Manipulator Kinematic and Sensor Extrinsic Parameters Through Contact-Based Interaction
Authors:
Oliver Limoyo,
Trevor Ablett,
Filip Marić,
Luke Volpatti,
Jonathan Kelly
Abstract:
We present a novel approach for mobile manipulator self-calibration using contact information. Our method, based on point cloud registration, is applied to estimate the extrinsic transform between a fixed vision sensor mounted on a mobile base and an end effector. Beyond sensor calibration, we demonstrate that the method can be extended to include manipulator kinematic model parameters, which invo…
▽ More
We present a novel approach for mobile manipulator self-calibration using contact information. Our method, based on point cloud registration, is applied to estimate the extrinsic transform between a fixed vision sensor mounted on a mobile base and an end effector. Beyond sensor calibration, we demonstrate that the method can be extended to include manipulator kinematic model parameters, which involves a non-rigid registration process. Our procedure uses on-board sensing exclusively and does not rely on any external measurement devices, fiducial markers, or calibration rigs. Further, it is fully automatic in the general case. We experimentally validate the proposed method on a custom mobile manipulator platform, and demonstrate centimetre-level post-calibration accuracy in positioning of the end effector using visual guidance only. We also discuss the stability properties of the registration algorithm, in order to determine the conditions under which calibration is possible.
△ Less
Submitted 22 October, 2018; v1 submitted 16 March, 2018;
originally announced March 2018.
-
Computer-Assisted Proving of Combinatorial Conjectures Over Finite Domains: A Case Study of a Chess Conjecture
Authors:
Predrag Janičić,
Filip Marić,
Marko Maliković
Abstract:
There are several approaches for using computers in deriving mathematical proofs. For their illustration, we provide an in-depth study of using computer support for proving one complex combinatorial conjecture -- correctness of a strategy for the chess KRK endgame. The final, machine verifiable, result presented in this paper is that there is a winning strategy for white in the KRK endgame general…
▽ More
There are several approaches for using computers in deriving mathematical proofs. For their illustration, we provide an in-depth study of using computer support for proving one complex combinatorial conjecture -- correctness of a strategy for the chess KRK endgame. The final, machine verifiable, result presented in this paper is that there is a winning strategy for white in the KRK endgame generalized to $n \times n$ board (for natural $n$ greater than $3$). We demonstrate that different approaches for computer-based theorem proving work best together and in synergy and that the technology currently available is powerful enough for providing significant help to humans deriving complex proofs.
△ Less
Submitted 27 March, 2019; v1 submitted 23 January, 2018;
originally announced January 2018.
-
Short Portfolio Training for CSP Solving
Authors:
Mirko Stojadinović,
Mladen Nikolić,
Filip Marić
Abstract:
Many different approaches for solving Constraint Satisfaction Problems (CSPs) and related Constraint Optimization Problems (COPs) exist. However, there is no single solver (nor approach) that performs well on all classes of problems and many portfolio approaches for selecting a suitable solver based on simple syntactic features of the input CSP instance have been developed. In this paper we first…
▽ More
Many different approaches for solving Constraint Satisfaction Problems (CSPs) and related Constraint Optimization Problems (COPs) exist. However, there is no single solver (nor approach) that performs well on all classes of problems and many portfolio approaches for selecting a suitable solver based on simple syntactic features of the input CSP instance have been developed. In this paper we first present a simple portfolio method for CSP based on k-nearest neighbors method. Then, we propose a new way of using portfolio systems --- training them shortly in the exploitation time, specifically for the set of instances to be solved and using them on that set. Thorough evaluation has been performed and has shown that the approach yields good results. We evaluated several machine learning techniques for our portfolio. Due to its simplicity and efficiency, the selected k-nearest neighbors method is especially suited for our short training approach and it also yields the best results among the tested methods. We also confirm that our approach yields good results on SAT domain.
△ Less
Submitted 8 May, 2015;
originally announced May 2015.
-
Formalizing Frankl's Conjecture: FC-families
Authors:
Filip Marić,
Miodrag Živković,
Bojan Vučković
Abstract:
The Frankl's conjecture, formulated in 1979. and still open, states that in every family of sets closed for unions there is an element contained in at least half of the sets. FC-families are families for which it is proved that every union-closed family containing them satisfies the Frankl's condition (e.g., in every union-closed family that contains a one-element set {a}, the element a is contain…
▽ More
The Frankl's conjecture, formulated in 1979. and still open, states that in every family of sets closed for unions there is an element contained in at least half of the sets. FC-families are families for which it is proved that every union-closed family containing them satisfies the Frankl's condition (e.g., in every union-closed family that contains a one-element set {a}, the element a is contained in at least half of the sets, so families of the form {a} are the simplest FC-families). FC-families play an important role in attacking the Frankl's conjecture, since they enable significant search space pruning. We present a formalization of the computer assisted approach for proving that a family is an FC-family. Proof-by-computation paradigm is used and the proof assistant Isabelle/HOL is used both to check mathematical content, and to perform (verified) combinatorial searches on which the proofs rely. FC-families known in the literature are confirmed, and a new FC-family is discovered.
△ Less
Submitted 16 July, 2012;
originally announced July 2012.
-
Formalization and Implementation of Algebraic Methods in Geometry
Authors:
Filip Marić,
Ivan Petrović,
Danijela Petrović,
Predrag Janičić
Abstract:
We describe our ongoing project of formalization of algebraic methods for geometry theorem proving (Wu's method and the Groebner bases method), their implementation and integration in educational tools. The project includes formal verification of the algebraic methods within Isabelle/HOL proof assistant and development of a new, open-source Java implementation of the algebraic methods. The project…
▽ More
We describe our ongoing project of formalization of algebraic methods for geometry theorem proving (Wu's method and the Groebner bases method), their implementation and integration in educational tools. The project includes formal verification of the algebraic methods within Isabelle/HOL proof assistant and development of a new, open-source Java implementation of the algebraic methods. The project should fill-in some gaps still existing in this area (e.g., the lack of formal links between algebraic methods and synthetic geometry and the lack of self-contained implementations of algebraic methods suitable for integration with dynamic geometry tools) and should enable new applications of theorem proving in education.
△ Less
Submitted 22 February, 2012;
originally announced February 2012.
-
Formalization of Abstract State Transition Systems for SAT
Authors:
Filip Maric,
Predrag Janicic
Abstract:
We present a formalization of modern SAT solvers and their properties in a form of abstract state transition systems. SAT solving procedures are described as transition relations over states that represent the values of the solver's global variables. Several different SAT solvers are formalized, including both the classical DPLL procedure and its state-of-the-art successors. The formalization is…
▽ More
We present a formalization of modern SAT solvers and their properties in a form of abstract state transition systems. SAT solving procedures are described as transition relations over states that represent the values of the solver's global variables. Several different SAT solvers are formalized, including both the classical DPLL procedure and its state-of-the-art successors. The formalization is made within the Isabelle/HOL system and the total correctness (soundness, termination, completeness) is shown for each presented system (with respect to a simple notion of satisfiability that can be manually checked). The systems are defined in a general way and cover procedures used in a wide range of modern SAT solvers. Our formalization builds up on the previous work on state transition systems for SAT, but it gives machine-verifiable proofs, somewhat more general specifications, and weaker assumptions that ensure the key correctness properties. The presented proofs of formal correctness of the transition systems can be used as a key building block in proving correctness of SAT solvers by using other verification approaches.
△ Less
Submitted 27 September, 2011; v1 submitted 22 August, 2011;
originally announced August 2011.
-
Simple Algorithm Portfolio for SAT
Authors:
Mladen Nikolic,
Filip Maric,
Predrag Janicic
Abstract:
The importance of algorithm portfolio techniques for SAT has long been noted, and a number of very successful systems have been devised, including the most successful one --- SATzilla. However, all these systems are quite complex (to understand, reimplement, or modify). In this paper we propose a new algorithm portfolio for SAT that is extremely simple, but in the same time so efficient that it ou…
▽ More
The importance of algorithm portfolio techniques for SAT has long been noted, and a number of very successful systems have been devised, including the most successful one --- SATzilla. However, all these systems are quite complex (to understand, reimplement, or modify). In this paper we propose a new algorithm portfolio for SAT that is extremely simple, but in the same time so efficient that it outperforms SATzilla. For a new SAT instance to be solved, our portfolio finds its k-nearest neighbors from the training set and invokes a solver that performs the best at those instances. The main distinguishing feature of our algorithm portfolio is the locality of the selection procedure --- the selection of a SAT solver is based only on few instances similar to the input one.
△ Less
Submitted 13 December, 2011; v1 submitted 1 July, 2011;
originally announced July 2011.
