Author name cluster

Moritz Müller

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

5 papers

2 author rows

AAAI Conference 2026 System Paper

GPTKB v1.5: A Massive Knowledge Base for Exploring Factual LLM Knowledge

Yujia Hu
Tuan-Phong Nguyen
Shrestha Ghosh
Moritz Müller
Simon Razniewski

Language models are powerful artifacts, yet their factual knowledge is still poorly understood, and inaccessible to ad-hoc browsing and scalable statistical analysis. This demonstration introduces GPTKB v1.5, a densely interlinked 100-million-triple knowledge base (KB) built for $14,000 from GPT-4.1, using the GPTKB methodology for massive-recursive LLM knowledge materialization. This demo focuses on three use cases: (1) link-traversal-based LLM knowledge exploration, (2) SPARQL-based structured LLM knowledge querying, (3) comparative exploration of the strengths and weaknesses of LLM knowledge. Massive-recursive LLM knowledge materialization is a groundbreaking opportunity both for the systematic analysis of LLM knowledge, as well as for automated KB construction.

PDF Details DOI

STOC Conference 2023 Conference Paper

On the Consistency of Circuit Lower Bounds for Non-deterministic Time

Albert Atserias
Sam Buss
Moritz Müller

We prove the first unconditional consistency result for superpolynomial circuit lower bounds with a relatively strong theory of bounded arithmetic. Namely, we show that the theory ‍V 2 0 is consistent with the conjecture that ‍NEXP ‍⊈ ‍P/poly, i.e., some problem that is solvable in non-deterministic exponential time does not have polynomial size circuits. We suggest this is the best currently available evidence for the truth of the conjecture. Additionally, we establish a magnification result on the hardness of proving circuit lower bounds.

Details

FOCS Conference 2019 Conference Paper

Automating Resolution is NP-Hard

Albert Atserias
Moritz Müller

We show that the problem of finding a Resolution refutation that is at most polynomially longer than a shortest one is NP-hard. In the parlance of proof complexity, Resolution is not automatizable unless P = NP. Indeed, we show that it is NP-hard to distinguish between formulas that have Resolution refutations of polynomial length and those that do not have subexponential length refutations. This also implies that Resolution is not automatizable in subexponential time or quasi-polynomial time unless~NP is included in SUBEXP or QP, respectively.

Details

I&C Journal 2017 Journal Article

The treewidth of proofs

Moritz Müller
Stefan Szeider

So-called ordered variants of the classical notions of pathwidth and treewidth are introduced and proposed as proof theoretically meaningful complexity measures for the directed acyclic graphs underlying proofs. Ordered pathwidth is roughly the same as proof space and the ordered treewidth of a proof is meant to serve as a measure of how far it is from being treelike. Length-space lower bounds for k-DNF refutations are generalized to arbitrary infinity axioms and strengthened in that the space measure is relaxed to ordered treewidth.

Details DOI

MFCS Conference 2013 Conference Paper

Revisiting Space in Proof Complexity: Treewidth and Pathwidth

Moritz Müller
Stefan Szeider

Abstract So-called ordered variants of the classical notions of pathwidth and treewidth are introduced and proposed as proof theoretically meaningful complexity measures for the directed acyclic graphs underlying proofs. The ordered pathwidth of a proof is shown to be roughly the same as its formula space. Length-space lower bounds for R ( k )-refutations are generalized to arbitrary infinity axioms and strengthened in that the space measure is relaxed to ordered treewidth.

Details