Query-driven PAC-Learning for Reasoning

Brendan Juba

arxiv: 1906.10118 · v1 · pith:V5GOJ63Rnew · submitted 2019-06-24 · 💻 cs.AI

Query-driven PAC-Learning for Reasoning

Brendan Juba This is my paper

Pith reviewed 2026-05-25 17:11 UTC · model grok-4.3

classification 💻 cs.AI

keywords PAC learningproof searchbackward chainingresolutionrule learningquery-driven reasoninglogical inference

0 comments

The pith

Any backward proof search algorithm that is sufficiently oblivious to its knowledge base can be modified to learn rules supporting a proof of a given query under PAC semantics.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper considers learning logical rules from data that suffice to prove a specific query, using Valiant's PAC semantics. It shows that standard backward proof search procedures can be adapted so that they learn the needed rules from data at the same time they search for a proof. This integration matters for a reader because it removes the need for a separate learning stage before reasoning begins. The approach applies directly to common proof systems including chaining and resolution. A sympathetic reader sees a way to make rule-based reasoning systems responsive to observed data without changing their core search strategy.

Core claim

We show how any backward proof search algorithm that is sufficiently oblivious to the contents of its knowledge base can be modified to learn such rules while it searches for a proof using those rules. We note that this gives such algorithms for standard logics such as chaining and resolution.

What carries the argument

The modification of an oblivious backward proof search algorithm that lets it learn query-supporting rules from data during the search itself.

If this is right

Standard chaining procedures become PAC learners for rules that prove a given query.
Standard resolution procedures become PAC learners for rules that prove a given query.
Rule learning occurs inside the proof search rather than in a prior separate phase.
The learned rules are guaranteed to support a proof of the query under the PAC semantics.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same modification could apply to any other proof system whose search routine meets the obliviousness condition.
Query-driven learning may reduce the number of rules that need to be considered by focusing only on those relevant to the current query.
Empirical tests could measure whether the PAC error bounds translate into reliable proof success rates on held-out data sets.

Load-bearing premise

The backward proof search algorithm must be sufficiently oblivious to the contents of its knowledge base.

What would settle it

A concrete counter-example in which a standard backward chaining procedure, after the proposed modification, produces rules whose PAC error on unseen data exceeds the bound required to prove the target query.

Figures

Figures reproduced from arXiv: 1906.10118 by Brendan Juba.

read the original abstract

We consider the problem of learning rules from a data set that support a proof of a given query, under Valiant's PAC-Semantics. We show how any backward proof search algorithm that is sufficiently oblivious to the contents of its knowledge base can be modified to learn such rules while it searches for a proof using those rules. We note that this gives such algorithms for standard logics such as chaining and resolution.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper shows how to modify backward proof search algorithms to learn PAC-supporting rules on the fly for a query, but the key 'sufficiently oblivious' condition is left informal and limits how far the claim can be checked.

read the letter

The core claim is that any backward proof search that is sufficiently oblivious to its knowledge base can be altered to learn rules from data while it searches for a proof of a given query, all under Valiant's PAC semantics, and that this covers chaining and resolution. That is the one thing worth knowing: it tries to fold rule learning directly into the search process rather than treating learning and proving as separate stages. The modification is presented as preserving correctness under the external PAC guarantee. What the paper does is sketch a general recipe for this integration and note its applicability to two standard proof procedures. That is a clean, scoped idea if the details hold. The soft spot is exactly the one the stress-test flags. 'Sufficiently oblivious' is stated without a formal definition, characterization, or set of sufficient conditions in the abstract, and the claim that the modification works for the cited logics rests on it. Without that, it is difficult to verify whether the result applies beyond the cases the author has in mind or whether the obliviousness requirement rules out many practical search algorithms. The abstract gives no derivation or algorithm pseudocode, so the strength of the argument cannot be assessed from what is visible. If the full paper supplies a precise condition plus a proof that the modified search still finds proofs when they exist under the PAC model, the result becomes more usable. As written at the high level, the work is narrow and the central property needs pinning down. This is for researchers working at the intersection of PAC learning and automated reasoning who want to see learning folded into proof search. A reader already familiar with backward chaining or resolution might extract the high-level idea and try to instantiate it, but the paper is unlikely to change practice until the oblivious condition is made operational. It deserves a serious referee because the direction is worth checking formally even if the current write-up requires expansion on the key assumption.

Referee Report

1 major / 0 minor

Summary. The paper claims that under Valiant's PAC semantics, any backward proof search algorithm that is 'sufficiently oblivious' to its knowledge base can be modified to learn rules supporting a proof of a given query while performing the search; it asserts that this yields algorithms for standard logics including chaining and resolution.

Significance. If the central claim holds with a precise characterization of 'sufficiently oblivious,' the result would supply a general mechanism for integrating PAC-style rule learning into existing proof procedures without separate training phases. This could strengthen query-driven reasoning systems in AI by making learning a byproduct of search, with direct applicability to well-studied inference rules.

major comments (1)

[Abstract] Abstract (and presumably §3 or the main technical section): the claim that 'any backward proof search algorithm that is sufficiently oblivious' can be modified while preserving correctness under PAC semantics is load-bearing, yet no formal definition, necessary and sufficient condition, or characterization of 'sufficiently oblivious' is supplied. Without this, one cannot verify whether the modification is sound for chaining or resolution, nor determine the class of algorithms covered.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the detailed review and for identifying the need for a precise characterization of 'sufficiently oblivious.' We agree this is essential for verifying the central claim and will revise the manuscript accordingly.

read point-by-point responses

Referee: [Abstract] Abstract (and presumably §3 or the main technical section): the claim that 'any backward proof search algorithm that is sufficiently oblivious' can be modified while preserving correctness under PAC semantics is load-bearing, yet no formal definition, necessary and sufficient condition, or characterization of 'sufficiently oblivious' is supplied. Without this, one cannot verify whether the modification is sound for chaining or resolution, nor determine the class of algorithms covered.

Authors: We acknowledge that the current manuscript does not supply a formal definition or characterization of 'sufficiently oblivious.' In the revised version we will add, in the main technical section, a precise definition specifying the conditions on a backward proof search algorithm (e.g., independence from KB contents in rule selection and subgoal ordering) that are necessary and sufficient for the PAC-preserving modification to be sound. This will explicitly cover the cases of chaining and resolution and delineate the broader class of algorithms to which the result applies. revision: yes

Circularity Check

0 steps flagged

No circularity; general theoretical claim under external PAC semantics

full rationale

The central claim is a general statement that any backward proof search algorithm satisfying an external condition ('sufficiently oblivious') can be modified to learn rules during search while preserving correctness under Valiant's PAC semantics. No equations, fitted parameters, or self-citations are invoked to derive the result; the claim does not reduce to its inputs by construction. The property is presented as an assumption on the input algorithm class, not defined in terms of the output. This matches the default expectation of a non-circular paper.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on standard assumptions from Valiant's PAC semantics and general properties of backward proof search; no free parameters, new entities, or ad-hoc axioms are introduced in the abstract.

axioms (1)

domain assumption Valiant's PAC-Semantics framework applies to learning rules that support proofs
The entire result is framed under PAC semantics as stated in the abstract.

pith-pipeline@v0.9.0 · 5568 in / 1099 out tokens · 35307 ms · 2026-05-25T17:11:53.243609+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

23 extracted references · 23 canonical work pages

[1]

A computing procedure for quantiﬁcation theory

[Davis and Putnam, 1960] Martin Davis and Hilary Putnam. A computing procedure for quantiﬁcation theory. JACM, 7(3):201–215,

work page 1960
[2]

Loveland

[Davis et al., 1962] Martin Davis, George Logemann, and Donald W. Loveland. A machine program for theorem- proving. Communications of the ACM , 5(7):394–397,

work page 1962
[3]

The ﬁrst Winograd Schema Challenge at IJCAI-16

[Davis et al., 2017] Ernest Davis, Leora Morgenstern, and Charles L Ortiz. The ﬁrst Winograd Schema Challenge at IJCAI-16. AI Magazine, 38(3):97–98,

work page 2017
[4]

Learning decision trees from random ex- amples

[Ehrenfeucht and Haussler, 1989] Andrzej Ehrenfeucht and David Haussler. Learning decision trees from random ex- amples. Inf. Comp., 82(3):231–246,

work page 1989
[5]

Space bounds for resolution

[Esteban and Tor´an, 2001] Juan Luis Esteban and Jacobo Tor´an. Space bounds for resolution. Inf. Comp. , 171(1):84–97,

work page 2001
[6]

[Halpern, 1990] Joseph Y . Halpern. An analysis of ﬁrst-order logics of probability. Artiﬁcial Intelligence, 46:311–350,

work page 1990
[7]

Tackling the Winograd Schema Challenge through ma- chine logical inferences

[Isaak and Michael, 2016] Nicos Isaak and Loizos Michael. Tackling the Winograd Schema Challenge through ma- chine logical inferences. In David Pearce and Helena Soﬁa Pinto, editors, STAIRS, volume 284 of Frontiers in Ar- tiﬁcial Intelligence and Applications , pages 75–86. IOS Press,

work page 2016
[8]

Principled sampling for anomaly detection

[Juba et al., 2015] Brendan Juba, Christopher Musco, Fan Long, Stelios Sidiroglou, and Martin Rinard. Principled sampling for anomaly detection. In Proc. NDSS,

work page 2015
[9]

Implicit learning of common sense for reasoning

[Juba, 2013] Brendan Juba. Implicit learning of common sense for reasoning. In Proc. 23rd IJCAI, pages 939–946,

work page 2013
[10]

Learning to reason

[Khardon and Roth, 1997] Roni Khardon and Dan Roth. Learning to reason. J. ACM, 44(5):697–725,

work page 1997
[11]

Investigating a gen- eral hierarchy of polynomially decidable classes of CNF’s based on short tree-like resolution proofs

[Kullmann, 1999] Oliver Kullmann. Investigating a gen- eral hierarchy of polynomially decidable classes of CNF’s based on short tree-like resolution proofs. Technical Re- port TR99-041, ECCC,

work page 1999
[12]

[Lenat, 1995] Douglas B. Lenat. CYC: a large-scale invest- ment in knowledge infrastructure. CACM, 38(11):33–38,

work page 1995
[13]

Sound input ﬁlter generation for integer overﬂow errors

[Long et al., 2014] Fan Long, Stelios Sidiroglou, Deokhwan Kim, and Martin Rinard. Sound input ﬁlter generation for integer overﬂow errors. In Proc. 41st POPL,

work page 2014
[14]

[Michael and Valiant, 2008] Loizos Michael and Leslie G. Valiant. A ﬁrst experimental demonstration of massive knowledge infusion. In Proc. 11th KR , pages 378–389,

work page 2008
[15]

Partial observability and learnability

[Michael, 2010] Loizos Michael. Partial observability and learnability. Artiﬁcial Intelligence , 174(11):639–669,

work page 2010
[16]

Machine invention of ﬁrst-order predi- cates by inverting resolution

[Muggleton and Buntine, 1988] Stephen Muggleton and Wray Buntine. Machine invention of ﬁrst-order predi- cates by inverting resolution. In Proc. 5th ICML , pages 339–352,

work page 1988
[17]

Inductive logic programming: Theory and methods

[Muggleton and De Raedt, 1994] Stephen Muggleton and Luc De Raedt. Inductive logic programming: Theory and methods. J. Logic Programming, 19:629–679,

work page 1994
[18]

Inductive logic pro- gramming

[Muggleton, 1991] Stephen Muggleton. Inductive logic pro- gramming. New generation computing , 8(4):295–318,

work page 1991
[19]

Probabilistic logic

[Nilsson, 1986] Nils J Nilsson. Probabilistic logic. Artiﬁcial intelligence, 28(1):71–87,

work page 1986
[20]

[Rubin, 1976] Donald B. Rubin. Inference and missing data. Biometrika, 63(3):581–592,

work page 1976
[21]

[Valiant, 1984] Leslie G. Valiant. A theory of the learnable. Communications of the ACM, 18(11):1134–1142,

work page 1984
[22]

[Valiant, 2000] Leslie G. Valiant. Robust logics. Artiﬁcial Intelligence, 117:231–253,

work page 2000
[23]

[Valiant, 2006] Leslie G. Valiant. Knowledge infusion. In Proc. AAAI-06, pages 1546–1551, 2006

work page 2006

[1] [1]

A computing procedure for quantiﬁcation theory

[Davis and Putnam, 1960] Martin Davis and Hilary Putnam. A computing procedure for quantiﬁcation theory. JACM, 7(3):201–215,

work page 1960

[2] [2]

Loveland

[Davis et al., 1962] Martin Davis, George Logemann, and Donald W. Loveland. A machine program for theorem- proving. Communications of the ACM , 5(7):394–397,

work page 1962

[3] [3]

The ﬁrst Winograd Schema Challenge at IJCAI-16

[Davis et al., 2017] Ernest Davis, Leora Morgenstern, and Charles L Ortiz. The ﬁrst Winograd Schema Challenge at IJCAI-16. AI Magazine, 38(3):97–98,

work page 2017

[4] [4]

Learning decision trees from random ex- amples

[Ehrenfeucht and Haussler, 1989] Andrzej Ehrenfeucht and David Haussler. Learning decision trees from random ex- amples. Inf. Comp., 82(3):231–246,

work page 1989

[5] [5]

Space bounds for resolution

[Esteban and Tor´an, 2001] Juan Luis Esteban and Jacobo Tor´an. Space bounds for resolution. Inf. Comp. , 171(1):84–97,

work page 2001

[6] [6]

[Halpern, 1990] Joseph Y . Halpern. An analysis of ﬁrst-order logics of probability. Artiﬁcial Intelligence, 46:311–350,

work page 1990

[7] [7]

Tackling the Winograd Schema Challenge through ma- chine logical inferences

[Isaak and Michael, 2016] Nicos Isaak and Loizos Michael. Tackling the Winograd Schema Challenge through ma- chine logical inferences. In David Pearce and Helena Soﬁa Pinto, editors, STAIRS, volume 284 of Frontiers in Ar- tiﬁcial Intelligence and Applications , pages 75–86. IOS Press,

work page 2016

[8] [8]

Principled sampling for anomaly detection

[Juba et al., 2015] Brendan Juba, Christopher Musco, Fan Long, Stelios Sidiroglou, and Martin Rinard. Principled sampling for anomaly detection. In Proc. NDSS,

work page 2015

[9] [9]

Implicit learning of common sense for reasoning

[Juba, 2013] Brendan Juba. Implicit learning of common sense for reasoning. In Proc. 23rd IJCAI, pages 939–946,

work page 2013

[10] [10]

Learning to reason

[Khardon and Roth, 1997] Roni Khardon and Dan Roth. Learning to reason. J. ACM, 44(5):697–725,

work page 1997

[11] [11]

Investigating a gen- eral hierarchy of polynomially decidable classes of CNF’s based on short tree-like resolution proofs

[Kullmann, 1999] Oliver Kullmann. Investigating a gen- eral hierarchy of polynomially decidable classes of CNF’s based on short tree-like resolution proofs. Technical Re- port TR99-041, ECCC,

work page 1999

[12] [12]

[Lenat, 1995] Douglas B. Lenat. CYC: a large-scale invest- ment in knowledge infrastructure. CACM, 38(11):33–38,

work page 1995

[13] [13]

Sound input ﬁlter generation for integer overﬂow errors

[Long et al., 2014] Fan Long, Stelios Sidiroglou, Deokhwan Kim, and Martin Rinard. Sound input ﬁlter generation for integer overﬂow errors. In Proc. 41st POPL,

work page 2014

[14] [14]

[Michael and Valiant, 2008] Loizos Michael and Leslie G. Valiant. A ﬁrst experimental demonstration of massive knowledge infusion. In Proc. 11th KR , pages 378–389,

work page 2008

[15] [15]

Partial observability and learnability

[Michael, 2010] Loizos Michael. Partial observability and learnability. Artiﬁcial Intelligence , 174(11):639–669,

work page 2010

[16] [16]

Machine invention of ﬁrst-order predi- cates by inverting resolution

[Muggleton and Buntine, 1988] Stephen Muggleton and Wray Buntine. Machine invention of ﬁrst-order predi- cates by inverting resolution. In Proc. 5th ICML , pages 339–352,

work page 1988

[17] [17]

Inductive logic programming: Theory and methods

[Muggleton and De Raedt, 1994] Stephen Muggleton and Luc De Raedt. Inductive logic programming: Theory and methods. J. Logic Programming, 19:629–679,

work page 1994

[18] [18]

Inductive logic pro- gramming

[Muggleton, 1991] Stephen Muggleton. Inductive logic pro- gramming. New generation computing , 8(4):295–318,

work page 1991

[19] [19]

Probabilistic logic

[Nilsson, 1986] Nils J Nilsson. Probabilistic logic. Artiﬁcial intelligence, 28(1):71–87,

work page 1986

[20] [20]

[Rubin, 1976] Donald B. Rubin. Inference and missing data. Biometrika, 63(3):581–592,

work page 1976

[21] [21]

[Valiant, 1984] Leslie G. Valiant. A theory of the learnable. Communications of the ACM, 18(11):1134–1142,

work page 1984

[22] [22]

[Valiant, 2000] Leslie G. Valiant. Robust logics. Artiﬁcial Intelligence, 117:231–253,

work page 2000

[23] [23]

[Valiant, 2006] Leslie G. Valiant. Knowledge infusion. In Proc. AAAI-06, pages 1546–1551, 2006

work page 2006