arXiv subjects

Manuel Eberl

Publications and source records attributed to Manuel Eberl.

4 recordsLinked to original sources

arXiv2026

The Impossibility of Strategyproof Rank Aggregation

In rank aggregation, the goal is to combine multiple input rankings into a single output ranking. In this paper, we analyze rank aggregation methods, so-called social welfare functions (SWFs), with respect to strategyproofness, which requires that no agent can misreport his ranking to obtain an output ranking that is closer to his true ranking in terms of the Kemeny distance. As our main result, we show that no anonymous SWF satisfies unanimity and strategyproofness when there are at least four alternatives. This result is proven by SAT solving, a computer-aided theorem proving technique, and verified by Isabelle, a highly trustworthy interactive proof assistant. Further, we prove by hand that strategyproofness is incompatible with majority consistency, a variant of Condorcet-consistency for SWFs. Lastly, we show that all SWFs in two natural classes have a large incentive ratio and are thus highly manipulable.

cs.GT↗

arXiv2022

Strategyproofness and Proportionality in Party-Approval Multiwinner Elections

In party-approval multiwinner elections the goal is to allocate the seats of a fixed-size committee to parties based on the approval ballots of the voters over the parties. In particular, each voter can approve multiple parties and each party can be assigned multiple seats. Two central requirements in this setting are proportional representation and strategyproofness. Intuitively, proportional representation requires that every sufficiently large group of voters with similar preferences is represented in the committee. Strategyproofness demands that no voter can benefit by misreporting her true preferences. We show that these two axioms are incompatible for anonymous party-approval multiwinner voting rules, thus proving a far-reaching impossibility theorem. The proof of this result is obtained by formulating the problem in propositional logic and then letting a SAT solver show that the formula is unsatisfiable. Additionally, we demonstrate how to circumvent this impossibility by considering a weakening of strategy\-proofness which requires that only voters who do not approve any elected party cannot manipulate. While most common voting rules fail even this weak notion of strategyproofness, we characterize Chamberlin--Courant approval voting within the class of Thiele rules based on this strategyproofness notion.

cs.GT↗

arXiv2017

Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving

Two important requirements when aggregating the preferences of multiple agents are that the outcome should be economically efficient and the aggregation mechanism should not be manipulable. In this paper, we provide a computer-aided proof of a sweeping impossibility using these two conditions for randomized aggregation mechanisms. More precisely, we show that every efficient aggregation mechanism can be manipulated for all expected utility representations of the agents' preferences. This settles an open problem and strengthens a number of existing theorems, including statements that were shown within the special domain of assignment. Our proof is obtained by formulating the claim as a satisfiability problem over predicates from real-valued arithmetic, which is then checked using an SMT (satisfiability modulo theories) solver. In order to verify the correctness of the result, a minimal unsatisfiable set of constraints returned by the SMT solver was translated back into a proof in higher-order logic, which was automatically verified by an interactive theorem prover. To the best of our knowledge, this is the first application of SMT solvers in computational social choice.

cs.GT↗

arXiv2017

A Verified Compiler for Probability Density Functions

Bhat et al. developed an inductive compiler that computes density functions for probability spaces described by programs in a simple probabilistic functional language. In this work, we implement such a compiler for a modified version of this language within the theorem prover Isabelle and give a formal proof of its soundness w.r.t. the semantics of the source and target language. Together with Isabelle's code generation for inductive predicates, this yields a fully verified, executable density compiler. The proof is done in two steps, using a standard refinement approach: first, an abstract compiler working with abstract functions modelled directly in the theorem prover's logic is defined and proven sound. Then, this compiler is refined to a concrete version that returns a target-language expression.

cs.PL↗