Writing study: DeepProofLog: Efficient Proving in Deep Stochastic Logic Programs
← AAAI 2026 oral writing corpus
Ying Jiao, Rodrigo Castellano Ontiveros, Luc De Raedt, Marco Gori, Francesco Giannini, Michelangelo Diligenti, Giuseppe Marra · Official AAAI 2026 oral record
Figure, table and section ledger
Editorial contribution type: Efficiency, inference & systems (primary).
Layout extraction, not a required paper template. Counts are distinct caption labels; a multi-panel figure counts once. Section spans are estimated from heading positions, including floats and whitespace. Method and limitations.
- Canonical PDF
- 9 physical pages
- Before references / appendix
- ≈ 7.22 page-equivalents
- Main figures / tables
- 2 / 2
- Attached appendix figures / tables
- 0 / 0
- Attached appendix span
- No boundary detected; not assumed zero
Extraction notes: No attached appendix boundary detected. Zero means no recognized caption, not independently verified absence.
Source-bound correction: Checked 2026-10-25. This source uses numbered main headings. Physical p.4 raster confirms Section 4 wraps onto a second line; the full label is restored at the first line's column-aware bbox position. Captions are Figures 1–2 and Tables 1–2. Main-PDF appendix pointers do not establish inspection of the separate supporting text.
Section-by-section lengths and source pages
The title/abstract/front matter precede the first numbered heading. A span ends at the next detected top-level heading, not at the last sentence; end-page whitespace is included. References and statements are listed separately. These are not measurements of text-only or artwork area.
| Top-level heading | Starts on PDF page | Estimated span | Share of entire PDF |
|---|---|---|---|
| 1 Introduction | 1 | ≈ 1.36 pp. | 15.11% |
| 2 Preliminaries | 2 | ≈ 1.04 pp. | 11.56% |
| 3 DeepProofLog | 3 | ≈ 0.61 pp. | 6.78% |
| 4 Markov Decision Processes for DeepProofLog | 4 | ≈ 0.83 pp. | 9.22% |
| 5 Learning in DeepProofLog | 5 | ≈ 0.41 pp. | 4.56% |
| 6 Experiments | 5 | ≈ 1.72 pp. | 19.11% |
| 7 Related Work | 7 | ≈ 0.48 pp. | 5.33% |
| 8 Conclusions | 7 | ≈ 0.25 pp. | 2.78% |
| Acknowledgments | 8 | ≈ 0.19 pp. | 2.11% |
| References | 8 | ≈ 1.78 pp. | 19.78% |
All detected figure and table locations
Attached appendix
No recognized caption labels.
Argument and organization
- 1 Introduction; 2 Preliminaries
Separates proof-generation cost from probabilistic inference cost and contrasts possible-world semantics with distributions over derivations before defining SLD resolution and MDPs.
- 3 DeepProofLog; 4 Markov Decision Processes for DeepProofLog; 5 Learning in DeepProofLog
Introduces goal-conditioned transition probabilities, maps proof steps to MDP components with a worked example, then derives the learning connection and splits exact dynamic programming from approximate policy gradients.
- 6 Experiments; 7 Related Work; 8 Conclusions
Tests perception-plus-reasoning scalability and knowledge-graph completion separately, displays actual proof trees, then revisits the closest systems and the remaining leftmost-atom restriction.
Problem, claim and contribution
The introduction changes the object being modeled: a distribution over proof derivations rather than possible worlds. It also distinguishes the cost of discovering proofs from the cost of probabilistic inference over them. This makes the scalability claim depend on a clear semantic and computational choice instead of an unspecified faster neural module.
Introduction, physical pp.1-2; stochastic resolution definitions, p.3 · Main paper
Argument and section order
The formal mapping is staged: define the goal representation and transition probabilities, instantiate states/actions/transitions/rewards, illustrate a positive and negative query, and only then introduce dynamic programming and policy gradients. The propositions state expressiveness and an objective correspondence; they are not interchangeable with empirical performance claims.
Sections 3-5 and Propositions 1-2, pp.3-5 · Main paper
Figures, captions and visual explanation
Figure 1 compares goal-level, scalar-clause and term-level parameterization in adjacent panels, making the changed conditioning visible before the formal definitions. Figure 2 shows concrete multi-step proof trees with named predicates and terminal markers. These examples communicate representational differences and inspectable outputs without relying on a generic stack of network boxes.
Figure 1, physical p.2; Figure 2, p.7; rendered pages inspected · Main paper
Tables, comparisons and evidence
Table 1 separates exact and approximate methods, pairs accuracy with minutes and labels a 24-hour timeout. It preserves the policy-gradient variant's zero accuracy at large sequence lengths despite completed runs. Table 2 retains non-winning knowledge-graph results; its protocol specifies 200 sampled negative corruptions and a RotatE prior for the neurosymbolic methods.
Section 6.1, p.5; Tables 1-2 and Section 6.2, p.6 · Main paper
Appendix and reproducibility
Proofs and derivations are routed to Appendix A, an action-space implementation detail to B.2, and task-specific logic programs, settings and metrics to C.1-C.2. The essential semantics, reward construction and exact-versus-approximate split remain in the main text. The linked extended document was not inspected, so these are verified pointers rather than claims about the appendix's completeness.
Sections 3-5, pp.4-5; Sections 6.1-6.2, pp.5-6; extended-version link, p.1 · Main paper
Clarity and writing conventions
The conclusion explicitly retains the leftmost-atom restriction and presents more flexible selection as future work. The experiment text also acknowledges a suboptimal learned policy at larger MNIST lengths. This is useful bounded wording: a tractable run, an inspectable proof and high task accuracy are three different claims, not synonyms for general successful reasoning.
Section 6.1 continuation, p.6; Sections 7-8, p.7 · Main paper
What to reuse—and what not to infer
Transferable lesson: When a formal reformulation enables a new system, teach the mapping with one worked symbolic example, state its consequences, and separate exact from approximate implementations in both prose and tables. Keep timeouts, completed failures and non-winning baselines visible.
Boundary: The appendix proofs and code were not inspected. Theoretical expressiveness and objective correspondence do not guarantee that the learned policy finds a useful solution in every large search space. Knowledge-graph results use sampled negative candidates and an inherited embedding prior; they should not be relabeled as unrestricted all-entity rankings or stand-alone logical discovery.
Apply this lesson using the argument and evidence worksheet.
Inspection record and sources
- Checked
- 2026-10-25
- Reading status
- Writing-focused manuscript scan + selected visuals inspected
- Main text
- Writing-focused text scan of physical PDF pp.1-7, covering semantics, definitions, the formal MDP mapping, exact/approximate inference, experiments, comparison with prior systems and limitations. Physical pp.2, 6 and 7 were rendered and visually inspected; the acknowledgments/reference boundary on p.8 was checked. This was not a proof audit or implementation/benchmark reproduction.
- Appendix / supplement
- Main-text pointers identify Appendix A.1-A.3 for proofs/derivations, B.2 for early abandonment, C.1 for MNIST logic programs and settings, and C.2 for knowledge-graph details. These sections are not attached to the nine-page proceedings PDF. The linked extended version and code were not retrieved or inspected; only their main-paper pointers were checked.
- Visually inspected PDF pages
- 2, 6, 7
This is a writing-focused scan of the manuscript and the stated supplementary scope: framing, organization, visual explanation, evidence presentation and wording. It is not a line-by-line proof audit, reproduction of results or exhaustive scientific review.